show that is f^2 is contractive, we can take the (unique) fixpoint of f

Also add "Local" to some Default Proof Using to keep them more contained

theories/algebra/agree.v

@@ -47,7 +47,7 @@ Qed.
 Section list_theory.
   Context `(R: relation A) `{Equivalence A R}.
   Collection Hyps := Type H.
-  Set Default Proof Using "Hyps".
+  Local Set Default Proof Using "Hyps".
 
   Global Instance: PreOrder (list_setincl R).
   Proof.
@@ -192,7 +192,7 @@ Section list_theory.
   Section fmap.
     Context `(R' : relation B) (f : A → B) {Hf: Proper (R ==> R') f}.
     Collection Hyps := Type Hf.
-    Set Default Proof Using "Hyps".
+    Local Set Default Proof Using "Hyps".
     
     Global Instance list_setincl_fmap :
       Proper (list_setincl R ==> list_setincl R') (fmap f).
@@ -219,7 +219,7 @@ Section list_theory.
 End list_theory.
 
 Section agree.
-Set Default Proof Using "Type".
+Local Set Default Proof Using "Type".
 Context {A : ofeT}.
 
 Definition agree_list (x : agree A) := agree_car x :: agree_with x.

theories/algebra/cmra.v

@@ -430,7 +430,7 @@ Qed.
 
 (** ** Total core *)
 Section total_core.
-  Set Default Proof Using "Type*".
+  Local Set Default Proof Using "Type*".
   Context `{CMRATotal A}.
 
   Lemma cmra_core_l x : core x ⋅ x ≡ x.
@@ -555,6 +555,7 @@ Hint Immediate cmra_unit_total.
 
 (** * Properties about CMRAs with Leibniz equality *)
 Section cmra_leibniz.
+  Local Set Default Proof Using "Type*".
   Context {A : cmraT} `{!LeibnizEquiv A}.
   Implicit Types x y : A.
 
@@ -601,6 +602,7 @@ Section cmra_leibniz.
 End cmra_leibniz.
 
 Section ucmra_leibniz.
+  Local Set Default Proof Using "Type*".
   Context {A : ucmraT} `{!LeibnizEquiv A}.
   Implicit Types x y z : A.
 
@@ -629,7 +631,7 @@ Section cmra_total.
     ✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
     ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2).
   Lemma cmra_total_mixin : CMRAMixin A.
-  Proof.
+  Proof using Type*.
     split; auto.
     - intros n x y ? Hcx%core_ne Hx; move: Hcx. rewrite /core /= Hx /=.
       case (total y)=> [cy ->]; eauto.
@@ -654,6 +656,7 @@ Proof.
 Qed.
 
 Section cmra_monotone.
+  Local Set Default Proof Using "Type*".
   Context {A B : cmraT} (f : A → B) `{!CMRAMonotone f}.
   Global Instance cmra_monotone_proper : Proper ((≡) ==> (≡)) f := ne_proper _.
   Lemma cmra_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
@@ -796,6 +799,7 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
 }.
 
 Section discrete.
+  Local Set Default Proof Using "Type*".
   Context `{Equiv A, PCore A, Op A, Valid A, @Equivalence A (≡)}.
   Context (ra_mix : RAMixin A).
   Existing Instances discrete_dist.
@@ -819,6 +823,7 @@ Global Instance discrete_cmra_discrete `{Equiv A, PCore A, Op A, Valid A,
 Proof. split. apply _. done. Qed.
 
 Section ra_total.
+  Local Set Default Proof Using "Type*".
   Context A `{Equiv A, PCore A, Op A, Valid A}.
   Context (total : ∀ x, is_Some (pcore x)).
   Context (op_proper : ∀ (x : A), Proper ((≡) ==> (≡)) (op x)).

theories/algebra/gmap.v

@@ -333,7 +333,7 @@ Proof.
 Qed.
 
 Section freshness.
-  Set Default Proof Using "Type*".
+  Local Set Default Proof Using "Type*".
   Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
   Lemma alloc_updateP_strong (Q : gmap K A → Prop) (I : gset K) m x :
     ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.

theories/algebra/gset.v

@@ -155,7 +155,7 @@ Section gset_disj.
   Proof. eauto using gset_disj_alloc_empty_updateP_strong. Qed.
 
   Section fresh_updates.
-    Set Default Proof Using "Type*".
+    Local Set Default Proof Using "Type*".
     Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
 
     Lemma gset_disj_alloc_updateP (Q : gset_disj K → Prop) X :

theories/algebra/ofe.v

@@ -166,7 +166,7 @@ Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
 Proof. by intros n y1 y2. Qed.
 
 Section contractive.
-  Set Default Proof Using "Type*".
+  Local Set Default Proof Using "Type*".
   Context {A B : ofeT} (f : A → B) `{!Contractive f}.
   Implicit Types x y : A.
 
@@ -261,6 +261,45 @@ Section fixpoint.
   Qed.
 End fixpoint.
 
+(** Fixpoint of f when f^2 is contractive. **)
+(* TODO: Generalize 2 to m. *)
+Definition fixpoint2 `{Cofe A, Inhabited A} (f : A → A)
+  `{!Contractive (Nat.iter 2 f)} := fixpoint (Nat.iter 2 f).
+
+Section fixpoint2.
+  Local Set Default Proof Using "Type*".
+  Context `{Cofe A, Inhabited A} (f : A → A) `{!Contractive (Nat.iter 2 f)}.
+  (* TODO: Can we get rid of this assumption, derive it from contractivity? *)
+  Context `{!∀ n, Proper (dist n ==> dist n) f}.
+
+  Lemma fixpoint2_unfold : fixpoint2 f ≡ f (fixpoint2 f).
+  Proof.
+    apply equiv_dist=>n.
+    rewrite /fixpoint2 fixpoint_eq /fixpoint_def (conv_compl n (fixpoint_chain _)) //.
+    induction n as [|n IH]; simpl.
+    - eapply contractive_0 with (f0 := Nat.iter 2 f). done.
+    - eapply contractive_S with (f0 := Nat.iter 2 f); first done. eauto.
+  Qed.
+
+  Lemma fixpoint2_unique (x : A) : x ≡ f x → x ≡ fixpoint2 f.
+  Proof.
+    intros Hf. apply fixpoint_unique, equiv_dist=>n. eapply equiv_dist in Hf.
+    rewrite 2!{1}Hf. done.
+  Qed.
+
+  Section fixpoint2_ne.
+    Context (g : A → A) `{!Contractive (Nat.iter 2 g), !∀ n, Proper (dist n ==> dist n) g}.
+
+    Lemma fixpoint2_ne n : (∀ z, f z ≡{n}≡ g z) → fixpoint2 f ≡{n}≡ fixpoint2 g.
+    Proof.
+      rewrite /fixpoint2=>Hne /=. apply fixpoint_ne=>? /=. rewrite !Hne. done.
+    Qed.
+
+    Lemma fixpoint2_proper : (∀ z, f z ≡ g z) → fixpoint2 f ≡ fixpoint2 g.
+    Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint2_ne. Qed.
+  End fixpoint2_ne.
+End fixpoint2.
+
 (** Mutual fixpoints *)
 Section fixpointAB.
   Local Unset Default Proof Using.
@@ -744,7 +783,7 @@ Section discrete_cofe.
 
   Instance discrete_dist : Dist A := λ n x y, x ≡ y.
   Definition discrete_ofe_mixin : OfeMixin A.
-  Proof.
+  Proof using Type*.
     split.
     - intros x y; split; [done|intros Hn; apply (Hn 0)].
     - done.

theories/algebra/updates.v

@@ -86,7 +86,7 @@ Qed.
 
 (** ** Frame preserving updates for total CMRAs *)
 Section total_updates.
-  Set Default Proof Using "Type*".
+  Local Set Default Proof Using "Type*".
   Context `{CMRATotal A}.
 
   Lemma cmra_total_updateP x (P : A → Prop) :

theories/heap_lang/lib/barrier/specification.v

@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Section spec.
-Set Default Proof Using "Type*".
+Local Set Default Proof Using "Type*".
 Context `{!heapG Σ, !barrierG Σ}.
 
 Lemma barrier_spec (N : namespace) :

theories/heap_lang/lib/par.v

@@ -14,7 +14,7 @@ Definition par : val :=
 Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
 
 Section proof.
-Set Default Proof Using "Type*".
+Local Set Default Proof Using "Type*".
 Context `{!heapG Σ, !spawnG Σ}.
 
 (* Notice that this allows us to strip a later *after* the two Ψ have been

theories/tests/barrier_client.v

@@ -14,7 +14,7 @@ Definition client : expr :=
     (worker 12 "b" "y" ||| worker 17 "b" "y").
 
 Section client.
-  Set Default Proof Using "Type*".
+  Local Set Default Proof Using "Type*".
   Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
 
   Definition N := nroot .@ "barrier".

theories/tests/joining_existentials.v

@@ -24,7 +24,7 @@ Definition client eM eW1 eW2 : expr :=
   (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
 
 Section proof.
-Set Default Proof Using "Type*".
+Local Set Default Proof Using "Type*".
 Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
 Context (N : namespace).
 Local Notation X := (F (iProp Σ)).

theories/tests/one_shot.v

@@ -30,7 +30,7 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
 Proof. solve_inG. Qed.
 
 Section proof.
-Set Default Proof Using "Type*".
+Local Set Default Proof Using "Type*".
 Context `{!heapG Σ, !one_shotG Σ}.
 
 Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=