Commit bb0f3924 authored by Robbert Krebbers's avatar Robbert Krebbers

`equiv` is no longer type class opaque.

parent 6d7699bd
Pipeline #16212 passed with stage
in 6 minutes and 15 seconds
...@@ -874,22 +874,6 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := { ...@@ -874,22 +874,6 @@ Record RAMixin A `{Equiv A, PCore A, Op A, Valid A} := {
ra_valid_op_l x y : (x y) x 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. Section discrete.
Local Set Default Proof Using "Type*". Local Set Default Proof Using "Type*".
Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A ()). Context `{Equiv A, PCore A, Op A, Valid A} (Heq : @Equivalence A ()).
......
...@@ -40,12 +40,10 @@ Instance dec_agree_pcore : PCore (dec_agree A) := Some. ...@@ -40,12 +40,10 @@ Instance dec_agree_pcore : PCore (dec_agree A) := Some.
Definition dec_agree_ra_mixin : RAMixin (dec_agree A). Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof. 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).
- intros [?|] [?|]; by repeat (simplify_eq/= || case_match). - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
- rewrite /pcore /dec_agree_pcore=> -? [?|] [->]; - intros [?|]; by repeat (simplify_eq/= || case_match).
by repeat (simplify_eq/= || case_match).
- rewrite /pcore /dec_agree_pcore. naive_solver.
- by intros [?|] [?|] ?. - by intros [?|] [?|] ?.
Qed. Qed.
......
...@@ -28,7 +28,7 @@ Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed. ...@@ -28,7 +28,7 @@ Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
Definition frac_ra_mixin : RAMixin frac. Definition frac_ra_mixin : RAMixin frac.
Proof. 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. 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. rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
Qed. Qed.
......
...@@ -24,7 +24,7 @@ Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc. ...@@ -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. Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
Definition ufrac_ra_mixin : RAMixin ufrac. 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. Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR. Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
......
...@@ -47,8 +47,7 @@ Proof. ...@@ -47,8 +47,7 @@ Proof.
- iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ). - iIntros (wp1 wp2) "#H"; iIntros ([[E e1] Φ]); iRevert (E e1 Φ).
iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)). iApply twp_pre_mono. iIntros "!#" (E e Φ). iApply ("H" $! (E,e,Φ)).
- intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2] - intros wp Hwp n [[E1 e1] Φ1] [[E2 e2] Φ2]
[[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?]; [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=.
simplify_eq/=.
rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne. rewrite /uncurry3 /twp_pre. do 24 (f_equiv || done). by apply pair_ne.
Qed. Qed.
...@@ -80,8 +79,7 @@ Proof. ...@@ -80,8 +79,7 @@ Proof.
prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) iProp Σ). prodC (prodC (leibnizC coPset) (exprC Λ)) (val Λ -c> iProp Σ) iProp Σ).
assert (NonExpansive Ψ'). assert (NonExpansive Ψ').
{ intros n [[E1 e1] Φ1] [[E2 e2] Φ2] { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
[[?%(discrete_iff _ _)%leibniz_equiv ?%(discrete_iff _ _)%leibniz_equiv] ?]; [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
simplify_eq/=. by apply HΨ. }
iApply (least_fixpoint_strong_ind _ Ψ' with "[] H"). iApply (least_fixpoint_strong_ind _ Ψ' with "[] H").
iIntros "!#" ([[??] ?]) "H". by iApply "IH". iIntros "!#" ([[??] ?]) "H". by iApply "IH".
Qed. Qed.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment