diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v index 2527765eb8654eeda68ca410abedc84be56dd762..bb2396e0e9394b5d55a2676cc9614edbbcd54ae3 100644 --- a/theories/algebra/cofe_solver.v +++ b/theories/algebra/cofe_solver.v @@ -1,6 +1,5 @@ From iris.algebra Require Export ofe. -(* FIXME: This file needs a 'Proof Using' hint, but the default we use - everywhere makes for lots of extra ssumptions. *) +Set Default Proof Using "Type". Record solution (F : cFunctor) := Solution { solution_car :> ofeT; @@ -22,7 +21,7 @@ Notation map := (cFunctor_map F). Fixpoint A (k : nat) : ofeT := match k with 0 => unitC | S k => F (A k) end. Local Instance: ∀ k, Cofe (A k). -Proof. induction 0; apply _. Defined. +Proof using Fcofe. induction 0; apply _. Defined. Fixpoint f (k : nat) : A k -n> A (S k) := match k with 0 => CofeMor (λ _, inhabitant) | S k => map (g k,f k) end with g (k : nat) : A (S k) -n> A k := @@ -34,12 +33,12 @@ Arguments f : simpl never. Arguments g : simpl never. Lemma gf {k} (x : A k) : g k (f k x) ≡ x. -Proof. +Proof using Fcontr. induction k as [|k IH]; simpl in *; [by destruct x|]. rewrite -cFunctor_compose -{2}[x]cFunctor_id. by apply (contractive_proper map). Qed. Lemma fg {k} (x : A (S (S k))) : f (S k) (g (S k) x) ≡{k}≡ x. -Proof. +Proof using Fcontr. induction k as [|k IH]; simpl. - rewrite f_S g_S -{2}[x]cFunctor_id -cFunctor_compose. apply (contractive_0 map). @@ -88,11 +87,11 @@ Fixpoint ff {k} (i : nat) : A k -n> A (i + k) := Fixpoint gg {k} (i : nat) : A (i + k) -n> A k := match i with 0 => cid | S i => gg i ◎ g (i + k) end. Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x. -Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed. +Proof using Fcontr. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)) IH]. Qed. Lemma f_tower k (X : tower) : f (S k) (X (S k)) ≡{k}≡ X (S (S k)). -Proof. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed. +Proof using Fcontr. intros. by rewrite -(fg (X (S (S k)))) -(g_tower X). Qed. Lemma ff_tower k i (X : tower) : ff i (X (S k)) ≡{k}≡ X (i + S k). -Proof. +Proof using Fcontr. intros; induction i as [|i IH]; simpl; [done|]. by rewrite IH Nat.add_succ_r (dist_le _ _ _ _ (f_tower _ X)); last omega. Qed. @@ -138,7 +137,7 @@ Definition embed_coerce {k} (i : nat) : A k -n> A i := end. Lemma g_embed_coerce {k i} (x : A k) : g i (embed_coerce (S i) x) ≡ embed_coerce i x. -Proof. +Proof using Fcontr. unfold embed_coerce; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl. - symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl. - exfalso; lia. @@ -206,7 +205,7 @@ Instance fold_ne : Proper (dist n ==> dist n) fold. Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed. Theorem result : solution F. -Proof. +Proof using All. apply (Solution F T _ (CofeMor unfold) (CofeMor fold)). - move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=. rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)). diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index e140399cae69cb991ec7a2c607f9d5213376f582..c2272a18c9048014ffaca1042b7fe48cb859a1ed 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -358,34 +358,34 @@ Section freshness. Lemma alloc_updateP' m x : ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None. Proof. eauto using alloc_updateP. Qed. - - Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i : - ✓ u → LeftId (≡) u (⋅) → - u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q. - Proof. - intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg. - destruct (Hx n (gf !! i)) as (y&?&Hy). - { move:(Hg i). rewrite !left_id. - case: (gf !! i)=>[x|]; rewrite /= ?left_id //. - intros; by apply cmra_valid_validN. } - exists {[ i := y ]}; split; first by auto. - intros i'; destruct (decide (i' = i)) as [->|]. - - rewrite lookup_op lookup_singleton. - move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //. - - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. - Qed. - Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i : - ✓ u → LeftId (≡) u (⋅) → - u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. - Proof. eauto using alloc_unit_singleton_updateP. Qed. - Lemma alloc_unit_singleton_update (u : A) i (y : A) : - ✓ u → LeftId (≡) u (⋅) → u ~~> y → (∅:gmap K A) ~~> {[ i := y ]}. - Proof. - rewrite !cmra_update_updateP; - eauto using alloc_unit_singleton_updateP with subst. - Qed. End freshness. +Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i : + ✓ u → LeftId (≡) u (⋅) → + u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q. +Proof. + intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg. + destruct (Hx n (gf !! i)) as (y&?&Hy). + { move:(Hg i). rewrite !left_id. + case: (gf !! i)=>[x|]; rewrite /= ?left_id //. + intros; by apply cmra_valid_validN. } + exists {[ i := y ]}; split; first by auto. + intros i'; destruct (decide (i' = i)) as [->|]. + - rewrite lookup_op lookup_singleton. + move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //. + - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id. +Qed. +Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i : + ✓ u → LeftId (≡) u (⋅) → + u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y. +Proof. eauto using alloc_unit_singleton_updateP. Qed. +Lemma alloc_unit_singleton_update (u : A) i (y : A) : + ✓ u → LeftId (≡) u (⋅) → u ~~> y → (∅:gmap K A) ~~> {[ i := y ]}. +Proof. + rewrite !cmra_update_updateP; + eauto using alloc_unit_singleton_updateP with subst. +Qed. + Lemma alloc_local_update m1 m2 i x : m1 !! i = None → ✓ x → (m1,m2) ~l~> (<[i:=x]>m1, <[i:=x]>m2). Proof. diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v index 9744e1355841672da6a8a9ba7585f20f517c8e9b..479e74c2f0a9a610ab71555b15c0ddf542117058 100644 --- a/theories/algebra/iprod.v +++ b/theories/algebra/iprod.v @@ -43,8 +43,6 @@ Section iprod_cofe. Qed. (** Properties of iprod_insert. *) - Context `{EqDecision A}. - Global Instance iprod_insert_ne n x : Proper (dist n ==> dist n ==> dist n) (iprod_insert x). Proof. diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v index 6e201a88958c3de7515bccc66b8a17e5e4aa261a..fbec685edc45a40d108dea675f49ee07743ef575 100644 --- a/theories/algebra/ofe.v +++ b/theories/algebra/ofe.v @@ -255,6 +255,8 @@ End fixpoint. (** Mutual fixpoints *) Section fixpoint2. + Local Unset Default Proof Using. + Context `{Cofe A, Cofe B, !Inhabited A, !Inhabited B}. Context (fA : A → B → A). Context (fB : A → B → B). diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v index dc7a42fe10dc1bd6d862fd80b09e579e3437e1f3..35d63746e13d986dec87fe5cc27a3016f50d95c2 100644 --- a/theories/algebra/updates.v +++ b/theories/algebra/updates.v @@ -107,7 +107,7 @@ Section total_updates. rewrite cmra_total_updateP; setoid_rewrite <-cmra_discrete_valid_iff. naive_solver eauto using 0. Qed. - Lemma cmra_discrete_update `{CMRADiscrete A} (x y : A) : + Lemma cmra_discrete_update (x y : A) : x ~~> y ↔ ∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z). Proof. rewrite cmra_total_update; setoid_rewrite <-cmra_discrete_valid_iff. diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v index e66b620f8e1a24b86f2b6382b01bfd87185f9187..a87844443106f691ee8f1f71b00b5355d099ac78 100644 --- a/theories/base_logic/lib/sts.v +++ b/theories/base_logic/lib/sts.v @@ -16,7 +16,7 @@ Instance subG_stsΣ Σ sts : Proof. intros ?%subG_inG ?. by split. Qed. Section definitions. - Context `{invG Σ, stsG Σ sts} (γ : gname). + Context `{stsG Σ sts} (γ : gname). Definition sts_ownS (S : sts.states sts) (T : sts.tokens sts) : iProp Σ := own γ (sts_frag S T). @@ -24,7 +24,7 @@ Section definitions. own γ (sts_frag_up s T). Definition sts_inv (φ : sts.state sts → iProp Σ) : iProp Σ := (∃ s, own γ (sts_auth s ∅) ∗ φ s)%I. - Definition sts_ctx (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ := + Definition sts_ctx `{!invG Σ} (N : namespace) (φ: sts.state sts → iProp Σ) : iProp Σ := inv N (sts_inv φ). Global Instance sts_inv_ne n : @@ -37,13 +37,13 @@ Section definitions. Proof. solve_proper. Qed. Global Instance sts_own_proper s : Proper ((≡) ==> (⊣⊢)) (sts_own s). Proof. solve_proper. Qed. - Global Instance sts_ctx_ne n N : + Global Instance sts_ctx_ne `{!invG Σ} n N : Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx N). Proof. solve_proper. Qed. - Global Instance sts_ctx_proper N : + Global Instance sts_ctx_proper `{!invG Σ} N : Proper (pointwise_relation _ (≡) ==> (⊣⊢)) (sts_ctx N). Proof. solve_proper. Qed. - Global Instance sts_ctx_persistent N φ : PersistentP (sts_ctx N φ). + Global Instance sts_ctx_persistent `{!invG Σ} N φ : PersistentP (sts_ctx N φ). Proof. apply _. Qed. Global Instance sts_own_peristent s : PersistentP (sts_own s ∅). Proof. apply _. Qed. diff --git a/theories/prelude/countable.v b/theories/prelude/countable.v index aa8ae1b3cdc5082645de6124f874dd5548c99841..37f0d922da96e6670680327884c1050bf830c177 100644 --- a/theories/prelude/countable.v +++ b/theories/prelude/countable.v @@ -32,7 +32,7 @@ Qed. (** * Choice principles *) Section choice. - Context `{Countable A} (P : A → Prop) `{∀ x, Decision (P x)}. + Context `{Countable A} (P : A → Prop). Inductive choose_step: relation positive := | choose_step_None {p} : decode p = None → choose_step (Psucc p) p @@ -50,6 +50,9 @@ Section choice. constructor. intros j. inversion 1 as [? Hd|? y Hd]; subst; auto with lia. Qed. + + Context `{∀ x, Decision (P x)}. + Fixpoint choose_go {i} (acc : Acc choose_step i) : A := match Some_dec (decode i) with | inleft (x↾Hx) => diff --git a/theories/prelude/fin_maps.v b/theories/prelude/fin_maps.v index aba8c7479b8660a6d51efafd1569992767c89e42..2dc9df1bdd7027644c4418a104c3b74b3550a227 100644 --- a/theories/prelude/fin_maps.v +++ b/theories/prelude/fin_maps.v @@ -118,7 +118,13 @@ Context `{FinMap K M}. (** ** Setoids *) Section setoid. - Context `{Equiv A} `{!Equivalence ((≡) : relation A)}. + Context `{Equiv A}. + + Lemma map_equiv_lookup_l (m1 m2 : M A) i x : + m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y. + Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed. + + Context `{!Equivalence ((≡) : relation A)}. Global Instance map_equivalence : Equivalence ((≡) : relation (M A)). Proof. split. @@ -173,9 +179,6 @@ Section setoid. split; [intros Hm; apply map_eq; intros i|by intros ->]. by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty. Qed. - Lemma map_equiv_lookup_l (m1 m2 : M A) i x : - m1 ≡ m2 → m1 !! i = Some x → ∃ y, m2 !! i = Some y ∧ x ≡ y. - Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed. Global Instance map_fmap_proper `{Equiv B} (f : A → B) : Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap (M:=M) f). Proof. diff --git a/theories/prelude/finite.v b/theories/prelude/finite.v index 7109bf3a7dceef7308a830dccee6c3f8876f6864..9c51d7cbf7442d4a67ce05b818f57dc27841544f 100644 --- a/theories/prelude/finite.v +++ b/theories/prelude/finite.v @@ -171,13 +171,15 @@ Proof. apply finite_bijective. eauto. Qed. (** Decidability of quantification over finite types *) Section forall_exists. - Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)}. + Context `{Finite A} (P : A → Prop). Lemma Forall_finite : Forall P (enum A) ↔ (∀ x, P x). Proof. rewrite Forall_forall. intuition auto using elem_of_enum. Qed. Lemma Exists_finite : Exists P (enum A) ↔ (∃ x, P x). Proof. rewrite Exists_exists. naive_solver eauto using elem_of_enum. Qed. + Context `{∀ x, Decision (P x)}. + Global Instance forall_dec: Decision (∀ x, P x). Proof. refine (cast_if (decide (Forall P (enum A)))); diff --git a/theories/prelude/list.v b/theories/prelude/list.v index 7228aa6f1be4ad9dc90cbddaed7581188d0d139b..0384de643b1bd73e92092aa35dd5dde2a0f615fa 100644 --- a/theories/prelude/list.v +++ b/theories/prelude/list.v @@ -735,6 +735,28 @@ End no_dup_dec. (** ** Set operations on lists *) Section list_set. + Lemma elem_of_list_intersection_with f l k x : + x ∈ list_intersection_with f l k ↔ ∃ x1 x2, + x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x. + Proof. + split. + - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|]. + intros Hx. setoid_rewrite elem_of_cons. + cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x) + ∨ x ∈ list_intersection_with f l k); [naive_solver|]. + clear IH. revert Hx. generalize (list_intersection_with f l k). + induction k; simpl; [by auto|]. + case_match; setoid_rewrite elem_of_cons; naive_solver. + - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl. + + generalize (list_intersection_with f l k). + induction Hx2; simpl; [by rewrite Hx; left |]. + case_match; simpl; try setoid_rewrite elem_of_cons; auto. + + generalize (IH Hx). clear Hx IH Hx2. + generalize (list_intersection_with f l k). + induction k; simpl; intros; [done|]. + case_match; simpl; rewrite ?elem_of_cons; auto. + Qed. + Context `{!EqDecision A}. Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k. Proof. @@ -773,27 +795,6 @@ Section list_set. - constructor. rewrite elem_of_list_intersection; intuition. done. - done. Qed. - Lemma elem_of_list_intersection_with f l k x : - x ∈ list_intersection_with f l k ↔ ∃ x1 x2, - x1 ∈ l ∧ x2 ∈ k ∧ f x1 x2 = Some x. - Proof. - split. - - induction l as [|x1 l IH]; simpl; [by rewrite elem_of_nil|]. - intros Hx. setoid_rewrite elem_of_cons. - cut ((∃ x2, x2 ∈ k ∧ f x1 x2 = Some x) - ∨ x ∈ list_intersection_with f l k); [naive_solver|]. - clear IH. revert Hx. generalize (list_intersection_with f l k). - induction k; simpl; [by auto|]. - case_match; setoid_rewrite elem_of_cons; naive_solver. - - intros (x1&x2&Hx1&Hx2&Hx). induction Hx1 as [x1|x1 ? l ? IH]; simpl. - + generalize (list_intersection_with f l k). - induction Hx2; simpl; [by rewrite Hx; left |]. - case_match; simpl; try setoid_rewrite elem_of_cons; auto. - + generalize (IH Hx). clear Hx IH Hx2. - generalize (list_intersection_with f l k). - induction k; simpl; intros; [done|]. - case_match; simpl; rewrite ?elem_of_cons; auto. - Qed. End list_set. (** ** Properties of the [filter] function *) @@ -2171,7 +2172,7 @@ Section Forall_Exists. Lemma Forall_replicate n x : P x → Forall P (replicate n x). Proof. induction n; simpl; constructor; auto. Qed. Lemma Forall_replicate_eq n (x : A) : Forall (x =) (replicate n x). - Proof. induction n; simpl; constructor; auto. Qed. + Proof using -(P). induction n; simpl; constructor; auto. Qed. Lemma Forall_take n l : Forall P l → Forall P (take n l). Proof. intros Hl. revert n. induction Hl; intros [|?]; simpl; auto. Qed. Lemma Forall_drop n l : Forall P l → Forall P (drop n l). @@ -2741,7 +2742,7 @@ End Forall3. (** Setoids *) Section setoid. - Context `{Equiv A} `{!Equivalence ((≡) : relation A)}. + Context `{Equiv A}. Implicit Types l k : list A. Lemma equiv_Forall2 l k : l ≡ k ↔ Forall2 (≡) l k. @@ -2752,6 +2753,8 @@ Section setoid. by setoid_rewrite equiv_option_Forall2. Qed. + Context {Hequiv: Equivalence ((≡) : relation A)}. + Global Instance list_equivalence : Equivalence ((≡) : relation (list A)). Proof. split. @@ -2763,42 +2766,42 @@ Section setoid. Proof. induction 1; f_equal; fold_leibniz; auto. Qed. Global Instance cons_proper : Proper ((≡) ==> (≡) ==> (≡)) (@cons A). - Proof. by constructor. Qed. + Proof using -(Hequiv). by constructor. Qed. Global Instance app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@app A). - Proof. induction 1; intros ???; simpl; try constructor; auto. Qed. + Proof using -(Hequiv). induction 1; intros ???; simpl; try constructor; auto. Qed. Global Instance length_proper : Proper ((≡) ==> (=)) (@length A). - Proof. induction 1; f_equal/=; auto. Qed. + Proof using -(Hequiv). induction 1; f_equal/=; auto. Qed. Global Instance tail_proper : Proper ((≡) ==> (≡)) (@tail A). Proof. by destruct 1. Qed. Global Instance take_proper n : Proper ((≡) ==> (≡)) (@take A n). - Proof. induction n; destruct 1; constructor; auto. Qed. + Proof using -(Hequiv). induction n; destruct 1; constructor; auto. Qed. Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n). - Proof. induction n; destruct 1; simpl; try constructor; auto. Qed. + Proof using -(Hequiv). induction n; destruct 1; simpl; try constructor; auto. Qed. Global Instance list_lookup_proper i : Proper ((≡) ==> (≡)) (lookup (M:=list A) i). Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed. Global Instance list_alter_proper f i : Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i). - Proof. intros. induction i; destruct 1; constructor; eauto. Qed. + Proof using -(Hequiv). intros. induction i; destruct 1; constructor; eauto. Qed. Global Instance list_insert_proper i : Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i). - Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed. + Proof using -(Hequiv). intros ???; induction i; destruct 1; constructor; eauto. Qed. Global Instance list_inserts_proper i : Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i). - Proof. + Proof using -(Hequiv). intros k1 k2 Hk; revert i. induction Hk; intros ????; simpl; try f_equiv; naive_solver. Qed. Global Instance list_delete_proper i : Proper ((≡) ==> (≡)) (delete (M:=list A) i). - Proof. induction i; destruct 1; try constructor; eauto. Qed. + Proof using -(Hequiv). induction i; destruct 1; try constructor; eauto. Qed. Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A). Proof. destruct 1; by constructor. Qed. Global Instance list_filter_proper P `{∀ x, Decision (P x)} : Proper ((≡) ==> iff) P → Proper ((≡) ==> (≡)) (filter (B:=list A) P). - Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed. + Proof using -(Hequiv). intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed. Global Instance replicate_proper n : Proper ((≡) ==> (≡)) (@replicate A n). - Proof. induction n; constructor; auto. Qed. + Proof using -(Hequiv). induction n; constructor; auto. Qed. Global Instance reverse_proper : Proper ((≡) ==> (≡)) (@reverse A). Proof. induction 1; rewrite ?reverse_cons; repeat (done || f_equiv). Qed. Global Instance last_proper : Proper ((≡) ==> (≡)) (@last A). diff --git a/theories/prelude/option.v b/theories/prelude/option.v index 242ad4f5f96ae13ba630351b8564c2abee9ed0a5..4988d7ba153a97404575363615f363ea328a69f5 100644 --- a/theories/prelude/option.v +++ b/theories/prelude/option.v @@ -115,18 +115,18 @@ End Forall2. Instance option_equiv `{Equiv A} : Equiv (option A) := option_Forall2 (≡). Section setoids. - Context `{Equiv A} `{!Equivalence ((≡) : relation A)}. + Context `{Equiv A} {Hequiv: Equivalence ((≡) : relation A)}. Implicit Types mx my : option A. Lemma equiv_option_Forall2 mx my : mx ≡ my ↔ option_Forall2 (≡) mx my. - Proof. done. Qed. + Proof using -(Hequiv). done. Qed. Global Instance option_equivalence : Equivalence ((≡) : relation (option A)). Proof. apply _. Qed. Global Instance Some_proper : Proper ((≡) ==> (≡)) (@Some A). - Proof. by constructor. Qed. + Proof using -(Hequiv). by constructor. Qed. Global Instance Some_equiv_inj : Inj (≡) (≡) (@Some A). - Proof. by inversion_clear 1. Qed. + Proof using -(Hequiv). by inversion_clear 1. Qed. Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A). Proof. intros x y; destruct 1; fold_leibniz; congruence. Qed. @@ -134,17 +134,17 @@ Section setoids. Proof. split; [by inversion_clear 1|by intros ->]. Qed. Lemma equiv_Some_inv_l mx my x : mx ≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡ y. - Proof. destruct 1; naive_solver. Qed. + Proof using -(Hequiv). destruct 1; naive_solver. Qed. Lemma equiv_Some_inv_r mx my y : mx ≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡ y. - Proof. destruct 1; naive_solver. Qed. + Proof using -(Hequiv). destruct 1; naive_solver. Qed. Lemma equiv_Some_inv_l' my x : Some x ≡ my → ∃ x', Some x' = my ∧ x ≡ x'. - Proof. intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed. + Proof using -(Hequiv). intros ?%(equiv_Some_inv_l _ _ x); naive_solver. Qed. Lemma equiv_Some_inv_r' mx y : mx ≡ Some y → ∃ y', mx = Some y' ∧ y ≡ y'. Proof. intros ?%(equiv_Some_inv_r _ _ y); naive_solver. Qed. Global Instance is_Some_proper : Proper ((≡) ==> iff) (@is_Some A). - Proof. inversion_clear 1; split; eauto. Qed. + Proof using -(Hequiv). inversion_clear 1; split; eauto. Qed. Global Instance from_option_proper {B} (R : relation B) (f : A → B) : Proper ((≡) ==> R) f → Proper (R ==> (≡) ==> R) (from_option f). Proof. destruct 3; simpl; auto. Qed.