New definition of contractive.

Using this new definition we can express being contractive using a
Proper. This has the following advantages:

- It makes it easier to state that a function with multiple arguments
  is contractive (in all or some arguments).
- A solve_contractive tactic can be implemented by extending the
  solve_proper tactic.

algebra/ofe.v

@@ -83,6 +83,11 @@ Record chain (A : ofeT) := {
 Arguments chain_car {_} _ _.
 Arguments chain_cauchy {_} _ _ _ _.
 
+Program Definition chain_map {A B : ofeT} (f : A → B)
+    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
+  {| chain_car n := f (c n) |}.
+Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+
 Notation Compl A := (chain A%type → A).
 Class Cofe (A : ofeT) := {
   compl : Compl A;
@@ -140,8 +145,14 @@ Section cofe.
 End cofe.
 
 (** Contractive functions *)
-Class Contractive {A B : ofeT} (f : A → B) :=
-  contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
+Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop :=
+  match n with 0 => True | S n => x ≡{n}≡ y end.
+Arguments dist_later _ !_ _ _ /.
+
+Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n).
+Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
+
+Notation Contractive f := (∀ n, Proper (dist_later n ==> dist n) f).
 
 Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
 Proof. by intros n y1 y2. Qed.
@@ -151,9 +162,9 @@ Section contractive.
   Implicit Types x y : A.
 
   Lemma contractive_0 x y : f x ≡{0}≡ f y.
-  Proof. eauto using contractive with omega. Qed.
+  Proof. by apply (_ : Contractive f). Qed.
   Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y.
-  Proof. eauto using contractive, dist_le with omega. Qed.
+  Proof. intros. by apply (_ : Contractive f). Qed.
 
   Global Instance contractive_ne n : Proper (dist n ==> dist n) f | 100.
   Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
@@ -161,18 +172,27 @@ Section contractive.
   Proof. apply (ne_proper _). Qed.
 End contractive.
 
-(** Mapping a chain *)
-Program Definition chain_map {A B : ofeT} (f : A → B)
-    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
-  {| chain_car n := f (c n) |}.
-Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
+Ltac f_contractive :=
+  match goal with
+  | |- ?f _ ≡{_}≡ ?f _ => apply (_ : Proper (dist_later _ ==> _) f)
+  | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (dist_later _ ==> _ ==> _) f)
+  | |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
+  end;
+  try match goal with
+  | |- dist_later ?n ?x ?y => destruct n as [|n]; [done|change (x ≡{n}≡ y)]
+  end;
+  try reflexivity.
+
+Ltac solve_contractive :=
+  preprocess_solve_proper;
+  solve [repeat (first [f_contractive|f_equiv]; try eassumption)].
 
 (** Fixpoint *)
 Program Definition fixpoint_chain {A : ofeT} `{Inhabited A} (f : A → A)
   `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
 Next Obligation.
   intros A ? f ? n.
-  induction n as [|n IH]; intros [|i] ?; simpl in *; try reflexivity || omega.
+  induction n as [|n IH]=> -[|i] //= ?; try omega.
   - apply (contractive_0 f).
   - apply (contractive_S f), IH; auto with omega.
 Qed.
@@ -513,7 +533,7 @@ Instance ofe_morCF_contractive F1 F2 :
   cFunctorContractive (ofe_morCF F1 F2).
 Proof.
   intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply ofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
+  apply ofe_morC_map_ne; apply cFunctor_contractive; destruct n, Hfg; by split.
 Qed.
 
 (** Sum *)
@@ -606,6 +626,7 @@ Qed.
 (** Discrete cofe *)
 Section discrete_cofe.
   Context `{Equiv A, @Equivalence A (≡)}.
+
   Instance discrete_dist : Dist A := λ n x y, x ≡ y.
   Definition discrete_ofe_mixin : OfeMixin A.
   Proof.
@@ -614,7 +635,7 @@ Section discrete_cofe.
     - done.
     - done.
   Qed.
-  
+
   Global Program Instance discrete_cofe : Cofe (OfeT A discrete_ofe_mixin) :=
     { compl c := c 0 }.
   Next Obligation.
@@ -743,17 +764,17 @@ Section later.
   Context {A : ofeT}.
   Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
   Instance later_dist : Dist (later A) := λ n x y,
-    match n with 0 => True | S n => later_car x ≡{n}≡ later_car y end.
+    dist_later n (later_car x) (later_car y).
   Definition later_ofe_mixin : OfeMixin (later A).
   Proof.
     split.
     - intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
       split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
-    - intros [|n]; [by split|split]; unfold dist, later_dist.
+    - split; rewrite /dist /later_dist.
       + by intros [x].
       + by intros [x] [y].
       + by intros [x] [y] [z] ??; trans y.
-    - intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
+    - intros [|n] [x] [y] ?; [done|]; rewrite /dist /later_dist; by apply dist_S.
   Qed.
   Canonical Structure laterC : ofeT := OfeT (later A) later_ofe_mixin.
 
@@ -767,9 +788,13 @@ Section later.
   Qed.
 
   Global Instance Next_contractive : Contractive (@Next A).
-  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
+  Proof. by intros [|n] x y. Qed.
   Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
+
+  Lemma contractive_alt {B : ofeT} (f : A → B) :
+    Contractive f ↔ (∀ n x y, Next x ≡{n}≡ Next y → f x ≡{n}≡ f y).
+  Proof. done. Qed.
 End later.
 
 Arguments laterC : clear implicits.
@@ -812,8 +837,8 @@ Qed.
 
 Instance laterCF_contractive F : cFunctorContractive (laterCF F).
 Proof.
-  intros A1 A2 B1 B2 n fg fg' Hfg.
-  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
+  intros A1 A2 B1 B2 n fg fg' Hfg. apply laterC_map_contractive.
+  destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
 Qed.
 
 (** Notation for writing functors *)

algebra/sts.v

@@ -78,7 +78,7 @@ Qed.
 Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
 Proof.
   intros S1 S2 HS T1 T2 HT. rewrite /up_set.
-  f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
+  f_equiv=> // s1 s2 Hs. by apply up_preserving.
 Qed.
 Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof.

base_logic/lib/boxes.v

@@ -47,17 +47,17 @@ Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop
 Proof. solve_proper. Qed.
 Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
 Proof. solve_proper. Qed.
+
 Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
 Proof. solve_proper. Qed.
-Global Instance box_contractive f : Contractive (box N f).
-Proof.
-  intros n P1 P2 HP1P2. apply exist_ne. intros Φ. f_equiv; last done.
-  apply contractive. intros n' ?. by rewrite HP1P2.
-Qed.
-
 Global Instance slice_persistent γ P : PersistentP (slice N γ P).
 Proof. apply _. Qed.
 
+Global Instance box_contractive f : Contractive (box N f).
+Proof. solve_contractive. Qed.
+Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
+Proof. apply (contractive_ne _). Qed.
+
 Lemma box_own_auth_agree γ b1 b2 :
   box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
 Proof.

base_logic/lib/fractional.v

@@ -55,7 +55,6 @@ Section fractional.
   Proof. done. Qed.
 
   (** Proof mode instances *)
-
   Global Instance from_sep_fractional_fwd P P1 P2 Φ q1 q2 :
     AsFractional P Φ (q1 + q2) → Fractional Φ →
     AsFractional P1 Φ q1 → AsFractional P2 Φ q2 →
@@ -97,12 +96,11 @@ Section fractional.
     AsFractional R Φ r → AsFractional PP' Φ (p + p') → Fractional Φ →
     Frame R (Φ p') Q → MakeSep (Φ p) Q PQ → Frame R PP' PQ.
   Proof.
-    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm. done.
+    rewrite /Frame=>->->-><-<-. rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
   Global Instance frame_fractional_half P Q R Φ p:
     AsFractional R Φ (p/2) → AsFractional P Φ p → Fractional Φ →
     AsFractional Q Φ (p/2)%Qp →
     Frame R P Q.
   Proof. by rewrite /Frame -{2}(Qp_div_2 p)=>->->->->. Qed.
-
 End fractional.

base_logic/lib/wsat.v

@@ -44,11 +44,10 @@ Context `{invG Σ}.
 Implicit Types P : iProp Σ.
 
 (* Invariants *)
+Instance invariant_unfold_contractive : Contractive (@invariant_unfold Σ).
+Proof. solve_contractive. Qed.
 Global Instance ownI_contractive i : Contractive (@ownI Σ _ i).
-Proof.
-  intros n P Q HPQ. rewrite /ownI /invariant_unfold. do 4 f_equiv.
-  apply Next_contractive=> j ?; by rewrite (HPQ j).
-Qed.
+Proof. solve_contractive. Qed.
 Global Instance ownI_persistent i P : PersistentP (ownI i P).
 Proof. rewrite /ownI. apply _. Qed.
 

base_logic/primitive.v

@@ -284,8 +284,8 @@ Proof.
 Qed.
 Global Instance later_contractive : Contractive (@uPred_later M).
 Proof.
-  intros n P Q HPQ; unseal; split=> -[|n'] x ??; simpl; [done|].
-  apply (HPQ n'); eauto using cmra_validN_S.
+  unseal; intros [|n] P Q HPQ; split=> -[|n'] x ?? //=; try omega.
+  apply HPQ; eauto using cmra_validN_S.
 Qed.
 Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
@@ -583,12 +583,11 @@ Proof. unseal. by destruct mx. Qed.
 
 (* Contractive functions *)
 Lemma contractiveI {A B : ofeT} (f : A → B) :
-  Contractive f ↔ (∀ x y, ▷ (x ≡ y) ⊢ f x ≡ f y).
+  Contractive f ↔ (∀ a b, ▷ (a ≡ b) ⊢ f a ≡ f b).
 Proof.
   split; unseal; intros Hf.
-  - intros x y; split=> -[|n] z _ /=; eauto using contractive_0, contractive_S.
-  - intros [|i] x y Hxy; apply (uPred_in_entails _ _ (Hf x y) _ ∅);
-      simpl; eauto using ucmra_unit_validN.
+  - intros a b; split=> n x _; apply Hf.
+  - intros i a b; eapply Hf, ucmra_unit_validN.
 Qed.
 
 (* Functions *)

base_logic/upred.v

@@ -118,8 +118,8 @@ Qed.
 Instance uPredCF_contractive F :
   urFunctorContractive F → cFunctorContractive (uPredCF F).
 Proof.
-  intros ? A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
+  intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredC_map_ne, urFunctor_contractive.
+  destruct n; split; by apply HPQ.
 Qed.
 
 (** logical entailement *)

prelude/gmultiset.v

@@ -185,8 +185,8 @@ Proof.
     rewrite !map_to_list_insert, !bind_cons
       by (by rewrite ?lookup_union_with, ?lookup_delete, ?HX).
     rewrite (assoc_L _), <-(comm (++) (f (_,n'))), <-!(assoc_L _), <-IH.
-    rewrite (assoc_L _); f_equiv; [rewrite (comm _); simpl|done].
-    by rewrite replicate_plus, Permutation_middle.
+    rewrite (assoc_L _). f_equiv.
+    rewrite (comm _); simpl. by rewrite replicate_plus, Permutation_middle.
   - rewrite <-insert_union_with_l, !map_to_list_insert, !bind_cons
       by (by rewrite ?lookup_union_with, ?HX, ?HY).
     by rewrite <-(assoc_L (++)), <-IH.

prelude/tactics.v

@@ -273,6 +273,7 @@ favor the second because the relation (dist) stays the same. *)
 Ltac f_equiv :=
   match goal with
   | _ => reflexivity
+  | |- pointwise_relation _ _ _ _ => intros ?
   (* We support matches on both sides, *if* they concern the same variable, or
      variables in some relation. *)
   | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
@@ -301,26 +302,12 @@ Ltac f_equiv :=
    (* In case the function symbol differs, but the arguments are the same,
       maybe we have a pointwise_relation in our context. *)
   | H : pointwise_relation _ ?R ?f ?g |- ?R (?f ?x) (?g ?x) => apply H
-  end.
-
-(** auto_proper solves goals of the form "f _ = f _", for any relation and any
-    number of arguments, by repeatedly applying f_equiv and handling trivial cases.
-    If it cannot solve an equality, it will leave that to the user. *)
-Ltac auto_equiv :=
-  (* Deal with "pointwise_relation" *)
-  repeat lazymatch goal with
-  | |- pointwise_relation _ _ _ _ => intros ?
   end;
-  (* Normalize away equalities. *)
-  simplify_eq;
-  (* repeatedly apply congruence lemmas and use the equalities in the hypotheses. *)
-  try (f_equiv; fast_done || auto_equiv).
-
-(** solve_proper solves goals of the form "Proper (R1 ==> R2)", for any
-    number of relations. All the actual work is done by auto_equiv;
-    solve_proper just introduces the assumptions and unfolds the first
-    head symbol. *)
-Ltac solve_proper :=
+  try reflexivity.
+
+(* The tactic [preprocess_solve_proper] unfolds the first head symbol, so that
+we proceed by repeatedly using [f_equiv]. *)
+Ltac preprocess_solve_proper :=
   (* Introduce everything *)
   intros;
   repeat lazymatch goal with
@@ -340,7 +327,14 @@ Ltac solve_proper :=
   | |- ?R (?f _ _) (?f _ _) => unfold f
   | |- ?R (?f _) (?f _) => unfold f
   end;
-  solve [ auto_equiv ].
+  simplify_eq.
+
+(** The tactic [solve_proper] solves goals of the form "Proper (R1 ==> R2)", for
+any number of relations. The actual work is done by repeatedly applying
+[f_equiv]. *)
+Ltac solve_proper :=
+  preprocess_solve_proper;
+  solve [repeat (f_equiv; try eassumption)].
 
 (** The tactic [intros_revert tac] introduces all foralls/arrows, performs tac,
 and then reverts them. *)

program_logic/weakestpre.v

@@ -37,11 +37,7 @@ Definition wp_pre `{irisG Λ Σ}
 Local Instance wp_pre_contractive `{irisG Λ Σ} : Contractive wp_pre.
 Proof.
   rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
-  apply or_ne, and_ne, forall_ne; auto=> σ1; apply wand_ne; auto.
-  apply fupd_ne, sep_ne, later_contractive; auto=> i ?.
-  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> efs.
-  apply wand_ne, fupd_ne, sep_ne, sep_ne; auto; first by apply Hwp.
-  apply big_opL_ne=> ? ef. by apply Hwp.
+  repeat (f_contractive || f_equiv); apply Hwp.
 Qed.
 
 Definition wp_def `{irisG Λ Σ} :
@@ -138,12 +134,12 @@ Global Instance wp_ne E e n :
   Proper (pointwise_relation _ (dist n) ==> dist n) (@wp Λ Σ _ E e).
 Proof.
   revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
-  rewrite !wp_unfold /wp_pre. apply or_ne, and_ne; auto; first solve_proper.
-  apply forall_ne=> σ1.
-  apply wand_ne, fupd_ne, sep_ne, later_contractive; auto=> i ?.
-  apply forall_ne=> e2; apply forall_ne=> σ2; apply forall_ne=> ef.
-  apply wand_ne, fupd_ne, sep_ne, sep_ne; auto.
-  apply IH; [done|]=> v. eapply dist_le; eauto with omega.
+  rewrite !wp_unfold /wp_pre.
+  (* FIXME: figure out a way to properly automate this proof *)
+  (* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
+  is very slow here *)
+  do 18 (f_contractive || f_equiv). apply IH; first lia.
+  intros v. eapply dist_le; eauto with omega.
 Qed.
 Global Instance wp_proper E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ _ E e).

[Ralf Jung]

@robbertkrebbers what do you think about having a similar notation for non-expansiveness?

I once tried this a while ago and noticed this is not just a cosmetic change; it reorders some quantifiers because it enforces the step-index to be last. IIRC you had good reasons to put it first in many places. On the other hand, Nonexpansive f is much clearer, and for contractiveness, this seems to work out fine.

[Robbert]

I don't I have had any other reasons other than consistency.

If we go for this, we probably also want a notation Nonexpansive2 for non-expansiveness of binary operators (of which we have quite a lot).

[Ralf Jung]

All right, I will put this on my low-priority TODO list then.