diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index cff69e8da34b3b7c82c5b7d7b2ae3e7cdc9bebbf..d4418c515e2d989ff513ce006dfa32448a8228e1 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -874,22 +874,6 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := { ra_valid_op_l x y : ✓ (x ⋅ y) → ✓ x }. -Section leibniz. - Local Set Default Proof Using "Type*". - Context A `{Equiv A, PCore A, Op A, Valid A}. - Context `{!Equivalence (≡@{A}), !LeibnizEquiv A}. - Context (op_assoc : Assoc (=@{A}) (⋅)). - Context (op_comm : Comm (=@{A}) (⋅)). - Context (pcore_l : ∀ (x : A) cx, pcore x = Some cx → cx ⋅ x = x). - Context (ra_pcore_idemp : ∀ (x : A) cx, pcore x = Some cx → pcore cx = Some cx). - Context (ra_pcore_mono : ∀ (x y : A) cx, - x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy). - Context (ra_valid_op_l : ∀ x y : A, ✓ (x ⋅ y) → ✓ x). - - Definition ra_leibniz_mixin : RAMixin A. - Proof. split; repeat intro; fold_leibniz; naive_solver. Qed. -End leibniz. - Section discrete. Local Set Default Proof Using "Type*". Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A (≡)). diff --git a/theories/algebra/deprecated.v b/theories/algebra/deprecated.v index 245cb63fdc28704d51a063247fecd8f14b1e5db0..2c8165cf10bff603132c3f7e054bee0c1129537d 100644 --- a/theories/algebra/deprecated.v +++ b/theories/algebra/deprecated.v @@ -40,12 +40,10 @@ Instance dec_agree_pcore : PCore (dec_agree A) := Some. Definition dec_agree_ra_mixin : RAMixin (dec_agree A). Proof. - apply ra_leibniz_mixin; try (apply _ || done). + apply ra_total_mixin; apply _ || eauto. - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match). - intros [?|] [?|]; by repeat (simplify_eq/= || case_match). - - rewrite /pcore /dec_agree_pcore=> -? [?|] [->]; - by repeat (simplify_eq/= || case_match). - - rewrite /pcore /dec_agree_pcore. naive_solver. + - intros [?|]; by repeat (simplify_eq/= || case_match). - by intros [?|] [?|] ?. Qed. diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v index 003a4fe23c70da4fea180ef4692c4b99477d5a58..f5f84eb01cf3f4fb43fcde9ef143018548e7da74 100644 --- a/theories/algebra/frac.v +++ b/theories/algebra/frac.v @@ -28,7 +28,7 @@ Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed. Definition frac_ra_mixin : RAMixin frac. Proof. - apply ra_leibniz_mixin; try (apply _ || done). + split; try apply _; try done. unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done. rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. Qed. diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v index 75ec408d376ca2a6672e10a6b1ccfaf759060a9c..297258cf9373392ff07398dce5e2973bdbcaa4ba 100644 --- a/theories/algebra/ufrac.v +++ b/theories/algebra/ufrac.v @@ -24,7 +24,7 @@ Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc. Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed. Definition ufrac_ra_mixin : RAMixin ufrac. -Proof. apply ra_leibniz_mixin; try (apply _ || done). Qed. +Proof. split; try (apply _ || done). Qed. Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin. Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR. diff --git a/theories/program_logic/total_weakestpre.v b/theories/program_logic/total_weakestpre.v index f9c150142695b179f724fdc06137d5077768c269..3b964c1fe6e944f5b6d3e6692ca42aa7e55db2fc 100644 --- a/theories/program_logic/total_weakestpre.v +++ b/theories/program_logic/total_weakestpre.v @@ -47,8 +47,7 @@ Proof. - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ). iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" \$! (E,e,Φ)). - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2] - [[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?]; - simplify_eq/=. + [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne. Qed. @@ -80,8 +79,7 @@ Proof. prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) → iProp Σ). assert (NonExpansive Ψ'). { intros n [[E1 e1] Φ1] [[E2 e2] Φ2] - [[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?]; - simplify_eq/=. by apply HΨ. } + [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. } iApply (least_fixpoint_strong_ind _ Ψ' with "[] H"). iIntros "!#" ([[??] ?]) "H". by iApply "IH". Qed.