Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

CHANGELOG.md

@@ -12,11 +12,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
   is proven in the logic.
-* [#] Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
+* Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.
   (The old `cofeT` is provided by `algebra.deprecated`.)
-* [#] Implement a new agreement construction.  Unlike the old one, this one
+* Implement a new agreement construction.  Unlike the old one, this one
   preserves discreteness.
 * Renaming and moving things around: uPred and the rest of the base logic are
   in `base_logic`, while `program_logic` is for everything involving the

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.
@@ -213,6 +233,85 @@ Section fixpoint.
   Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
 End fixpoint.
 
+(** Mutual fixpoints *)
+Section fixpoint2.
+  Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
+  Context (fA : A → B → A).
+  Context (fB : A → B → B).
+  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
+  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
+
+  Local Definition fixpoint_AB (x : A) : B := fixpoint (fB x).
+  Local Instance fixpoint_AB_contractive : Contractive fixpoint_AB.
+  Proof.
+    intros n x x' Hx; rewrite /fixpoint_AB.
+    apply fixpoint_ne=> y. by f_contractive.
+  Qed.
+
+  Local Definition fixpoint_AA (x : A) : A := fA x (fixpoint_AB x).
+  Local Instance fixpoint_AA_contractive : Contractive fixpoint_AA.
+  Proof. solve_contractive. Qed.
+
+  Definition fixpoint_A : A := fixpoint fixpoint_AA.
+  Definition fixpoint_B : B := fixpoint_AB fixpoint_A.
+
+  Lemma fixpoint_A_unfold : fA fixpoint_A fixpoint_B ≡ fixpoint_A.
+  Proof. by rewrite {2}/fixpoint_A (fixpoint_unfold _). Qed.
+  Lemma fixpoint_B_unfold : fB fixpoint_A fixpoint_B ≡ fixpoint_B.
+  Proof. by rewrite {2}/fixpoint_B /fixpoint_AB (fixpoint_unfold _). Qed.
+
+  Instance: Proper ((≡) ==> (≡) ==> (≡)) fA.
+  Proof.
+    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
+  Qed.
+  Instance: Proper ((≡) ==> (≡) ==> (≡)) fB.
+  Proof.
+    apply ne_proper_2=> n x x' ? y y' ?. f_contractive; auto using dist_S.
+  Qed.
+
+  Lemma fixpoint_A_unique p q : fA p q ≡ p → fB p q ≡ q → p ≡ fixpoint_A.
+  Proof.
+    intros HfA HfB. rewrite -HfA. apply fixpoint_unique. rewrite /fixpoint_AA.
+    f_equiv=> //. apply fixpoint_unique. by rewrite HfA HfB.
+  Qed.
+  Lemma fixpoint_B_unique p q : fA p q ≡ p → fB p q ≡ q → q ≡ fixpoint_B.
+  Proof. intros. apply fixpoint_unique. by rewrite -fixpoint_A_unique. Qed.
+End fixpoint2.
+
+Section fixpoint2_ne.
+  Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}.
+  Context (fA fA' : A → B → A).
+  Context (fB fB' : A → B → B).
+  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA}.
+  Context `{∀ n, Proper (dist_later n ==> dist n ==> dist n) fA'}.
+  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB}.
+  Context `{∀ n, Proper (dist_later n ==> dist_later n ==> dist n) fB'}.
+
+  Lemma fixpoint_A_ne n :
+    (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
+    fixpoint_A fA fB ≡{n}≡ fixpoint_A fA' fB'.
+  Proof.
+    intros HfA HfB. apply fixpoint_ne=> z.
+    rewrite /fixpoint_AA /fixpoint_AB HfA. f_equiv. by apply fixpoint_ne.
+  Qed.
+  Lemma fixpoint_B_ne n :
+    (∀ x y, fA x y ≡{n}≡ fA' x y) → (∀ x y, fB x y ≡{n}≡ fB' x y) →
+    fixpoint_B fA fB ≡{n}≡ fixpoint_B fA' fB'.
+  Proof.
+    intros HfA HfB. apply fixpoint_ne=> z. rewrite HfB. f_contractive.
+    apply fixpoint_A_ne; auto using dist_S.
+  Qed.
+
+  Lemma fixpoint_A_proper :
+    (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
+    fixpoint_A fA fB ≡ fixpoint_A fA' fB'.
+  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_A_ne. Qed.
+  Lemma fixpoint_B_proper :
+    (∀ x y, fA x y ≡ fA' x y) → (∀ x y, fB x y ≡ fB' x y) →
+    fixpoint_B fA fB ≡ fixpoint_B fA' fB'.
+  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
+End fixpoint2_ne.
+
 (** Function space *)
 (* We make [ofe_fun] a definition so that we can register it as a canonical
 structure. *)
@@ -513,7 +612,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 +705,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 +714,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 +843,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,15 +867,21 @@ 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 later_car_compose_ne {B : ofeT} (f : A → B) :
-    (Contractive f) → ∀ n, Proper (dist n ==> dist n) (f ∘ later_car).
+  Instance later_car_anti_contractive n :
+    Proper (dist n ==> dist_later n) later_car.
+  Proof. move=> [x] [y] /= Hxy. done. Qed.
+
+  Lemma contractive_alt {B : ofeT} (f : A → B) :
+    Contractive f ↔ ∃ g : later A → B,
+      (∀ n, Proper (dist n ==> dist n) g) ∧ (∀ x, f x ≡ g (Next x)).
   Proof.
-    move=> Hcont n [x] [y] /= Hxy. apply Hcont. intros m Hmn.
-    destruct n; first by (exfalso; omega). eapply dist_le', Hxy. omega.
+    split.
+    - intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.
+    - intros (g&Hg&Hf) n x y Hxy. rewrite !Hf. by apply Hg.
   Qed.
 End later.
 
@@ -819,8 +925,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/derived.v

@@ -290,10 +290,8 @@ Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qe
 Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
   {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
-  rewrite -later_equivI. intros Heq.
-  change ((P ⊢ (Ψ ∘ later_car) (Next a)) → P ⊢ (Ψ ∘ later_car) (Next b)).
-  apply internal_eq_rewrite; last done.
-  exact: later_car_compose_ne.
+  move: HΨ=> /contractiveI HΨ Heq ?.
+  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
 Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).

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

@@ -45,7 +45,7 @@ Section fractional.
     Fractional Φ → Fractional Ψ → Fractional (λ q, Φ q ∗ Ψ q)%I.
   Proof.
     intros ?? q q'. rewrite !fractional -!assoc. f_equiv.
-    rewrite !assoc. f_equiv; last done. by rewrite comm.
+    rewrite !assoc. f_equiv. by rewrite comm.
   Qed.
 
   Global Instance fractional_big_sepL {A} l Ψ :
@@ -98,7 +98,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 →
@@ -140,12 +139,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 _.
@@ -581,6 +581,15 @@ Lemma option_validI {A : cmraT} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
 Proof. unseal. by destruct mx. Qed.
 
+(* Contractive functions *)
+Lemma contractiveI {A B : ofeT} (f : A → B) :
+  Contractive f ↔ (∀ a b, ▷ (a ≡ b) ⊢ f a ≡ f b).
+Proof.
+  split; unseal; intros Hf.
+  - intros a b; split=> n x _; apply Hf.
+  - intros i a b; eapply Hf, ucmra_unit_validN.
+Qed.
+
 (* Functions *)
 Lemma cofe_funC_equivI {A B} (f g : A -c> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof. by unseal. Qed.

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 *)

docs/constructions.tex

@@ -141,35 +141,28 @@ $K \fpfn (-)$ is a locally non-expansive functor from $\CMRAs$ to $\CMRAs$.
 
 Given some OFE $\cofe$, we define the CMRA $\agm(\cofe)$ as follows:
 \begin{align*}
-  \agm(\cofe) \eqdef{}& \set{(c, V) \in (\nat \to \cofe) \times \SProp}/\ {\sim} \\[-0.2em]
-  \textnormal{where }& \melt \sim \meltB \eqdef{} \melt.V = \meltB.V \land 
-    \All n. n \in \melt.V \Ra \melt.c(n) \nequiv{n} \meltB.c(n)  \\
+  \agm(\cofe) \eqdef{}& \setComp{\melt \in \finpset\cofe}{c \neq \emptyset} /\ {\sim} \\[-0.2em]
+  \melt \nequiv{n} \meltB \eqdef{}& (\All x \in \melt. \Exists y \in \meltB. x \nequiv{n} y) \land (\All y \in \meltB. \Exists x \in \melt. x \nequiv{n} y) \\
+  \textnormal{where }& \melt \sim \meltB \eqdef{} \All n. \melt \nequiv{n} \meltB  \\
+~\\
 %    \All n \in {\melt.V}.\, \melt.x \nequiv{n} \meltB.x \\
-  \melt \nequiv{n} \meltB \eqdef{}& (\All m \leq n. m \in \melt.V \Lra m \in \meltB.V) \land (\All m \leq n. m \in \melt.V \Ra \melt.c(m) \nequiv{m} \meltB.c(m)) \\
-  \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ n \in \melt.V \land \All m \leq n. \melt.c(n) \nequiv{m} \melt.c(m) } \\
+  \mval_n \eqdef{}& \setComp{\melt \in \agm(\cofe)}{ \All x, y \in \melt. x \nequiv{n} y } \\
   \mcore\melt \eqdef{}& \melt \\
-  \melt \mtimes \meltB \eqdef{}& \left(\melt.c, \setComp{n}{n \in \melt.V \land n \in \meltB.V \land \melt \nequiv{n} \meltB }\right)
+  \melt \mtimes \meltB \eqdef{}& \melt \cup \meltB
 \end{align*}
 %Note that the carrier $\agm(\cofe)$ is a \emph{record} consisting of the two fields $c$ and $V$.
 
 $\agm(-)$ is a locally non-expansive functor from $\OFEs$ to $\CMRAs$.
 
-You can think of the $c$ as a \emph{chain} of elements of $\cofe$ that has to converge only for $n \in V$ steps.
-The reason we store a chain, rather than a single element, is that $\agm(\cofe)$ needs to be a COFE itself, so we need to be able to give a limit for every chain of $\agm(\cofe)$.
-However, given such a chain, we cannot constructively define its limit: Clearly, the $V$ of the limit is the limit of the $V$ of the chain.
-But what to pick for the actual data, for the element of $\cofe$?
-Only if $V = \nat$ we have a chain of $\cofe$ that we can take a limit of; if the $V$ is smaller, the chain ``cancels'', \ie stops converging as we reach indices $n \notin V$.
-To mitigate this, we apply the usual construction to close a set; we go from elements of $\cofe$ to chains of $\cofe$.
-
-We define an injection $\aginj$ into $\agm(\cofe)$ as follows:
-\[ \aginj(x) \eqdef \record{\mathrm c \eqdef \Lam \any. x, \mathrm V \eqdef \nat} \]
+We define a non-expansive injection $\aginj$ into $\agm(\cofe)$ as follows:
+\[ \aginj(x) \eqdef \set{x} \]
 There are no interesting frame-preserving updates for $\agm(\cofe)$, but we can show the following:
 \begin{mathpar}
   \axiomH{ag-val}{\aginj(x) \in \mval_n}
 
   \axiomH{ag-dup}{\aginj(x) = \aginj(x)\mtimes\aginj(x)}
   
-  \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Ra x \nequiv{n} y}
+  \axiomH{ag-agree}{\aginj(x) \mtimes \aginj(y) \in \mval_n \Lra x \nequiv{n} y}
 \end{mathpar}
 
 

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).