Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • iris/iris
  • jeehoon.kang/iris-coq
  • amintimany/iris-coq
  • dfrumin/iris-coq
  • Villetaneuse/iris
  • gares/iris
  • shiatsumat/iris
  • Blaisorblade/iris
  • jihgfee/iris-coq
  • mrhaandi/iris
  • tlsomers/iris
  • Quarkbeast/iris-coq
  • janno/iris
  • amaurremi/iris-coq
  • proux/iris
  • tchajed/iris
  • herbelin/iris-coq
  • msammler/iris-coq
  • maximedenes/iris-coq
  • bpeters/iris
  • haidang/iris
  • lepigre/iris
  • lczch/iris
  • simonspies/iris
  • gpirlea/iris
  • dkhalanskiyjb/iris
  • gmalecha/iris
  • germanD/iris
  • aa755/iris
  • jules/iris
  • abeln/iris
  • simonfv/iris
  • atrieu/iris
  • arthuraa/iris
  • simonh/iris
  • jung/iris
  • mattam82/iris
  • Armael/iris
  • adamAndMath/iris
  • gmevel/iris
  • snyke7/iris
  • johannes/iris
  • NiklasM/iris
  • simonspies/iris-parametric-index
  • svancollem/iris
  • proux1/iris
  • wmansky/iris
  • LukeXuan/iris
  • ivanbakel/iris
  • SkySkimmer/iris
  • tjhance/iris
  • yiyunliu/iris
  • Lee-Janggun/iris
  • thomas-lamiaux/iris
  • dongjae/iris
  • dnezam/iris
  • Tragicus/iris
  • clef-men/iris
  • ffengyu/iris
59 results
Show changes
Commits on Source (5)
...@@ -39,28 +39,16 @@ Section ofe. ...@@ -39,28 +39,16 @@ Section ofe.
Local Definition below (a : A) (x : mra R) := b, b x R a b. Local Definition below (a : A) (x : mra R) := b, b x R a b.
Local Lemma below_app a x y : below a (x ++ y) below a x below a y. Local Lemma below_app a x y : below a (x ++ y) below a x below a y.
Proof. Proof. set_solver. Qed.
split.
- intros (b & [|]%elem_of_app & ?); [left|right]; exists b; eauto.
- intros [(b & ? & ?)|(b & ? & ?)]; exists b; rewrite elem_of_app; eauto.
Qed.
Local Lemma below_principal a b : below a (principal R b) R a b. Local Lemma below_principal a b : below a (principal R b) R a b.
Proof. Proof. set_solver. Qed.
split.
- intros (c & ->%elem_of_list_singleton & ?); done.
- intros Hab; exists b; split; first apply elem_of_list_singleton; done.
Qed.
Local Instance mra_equiv : Equiv (mra R) := Local Instance mra_equiv : Equiv (mra R) :=
λ x y, a, below a x below a y. λ x y, a, below a x below a y.
Local Instance mra_equiv_equiv : Equivalence mra_equiv. Local Instance mra_equiv_equiv : Equivalence mra_equiv.
Proof. Proof. unfold mra_equiv; split; intros ?; naive_solver. Qed.
split; [by firstorder|by firstorder|].
intros ??? Heq1 Heq2 ?; split; intros ?;
[apply Heq2; apply Heq1|apply Heq1; apply Heq2]; done.
Qed.
Canonical Structure mraO := discreteO (mra R). Canonical Structure mraO := discreteO (mra R).
End ofe. End ofe.
...@@ -83,12 +71,12 @@ Section cmra. ...@@ -83,12 +71,12 @@ Section cmra.
apply discrete_cmra_mixin; first apply _. apply discrete_cmra_mixin; first apply _.
apply ra_total_mixin. apply ra_total_mixin.
- eauto. - eauto.
- intros ??? Heq a; specialize (Heq a); rewrite !below_app; firstorder. - intros ??? Heq a; by rewrite !below_app (Heq a).
- intros ?; done. - intros ?; done.
- done. - done.
- intros ????; rewrite !below_app; firstorder. - intros ????; rewrite !below_app; by intuition.
- intros ???; rewrite !below_app; firstorder. - intros ???; rewrite !below_app; by intuition.
- rewrite /core /pcore /=; intros ??; rewrite below_app; firstorder. - rewrite /core /pcore /=; intros ??; rewrite below_app; by intuition.
- done. - done.
- intros ? ? [? ?]; eexists _; done. - intros ? ? [? ?]; eexists _; done.
- done. - done.
...@@ -119,53 +107,41 @@ Section cmra. ...@@ -119,53 +107,41 @@ Section cmra.
intros [z ->]; rewrite assoc mra_idemp; done. intros [z ->]; rewrite assoc mra_idemp; done.
Qed. Qed.
Lemma principal_R_opN_base `{!Transitive R} n x y : Lemma principal_R_op_base `{!Transitive R} x y :
( b, b y c, c x R b c) y x {n} x. ( b, b y c, c x R b c) y x x.
Proof. Proof.
intros HR; split; rewrite /op /mra_op below_app; [|by firstorder]. intros HR. split; rewrite /op /mra_op below_app; [|by intuition].
intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done]. intros [(c & (d & Hd1 & Hd2)%HR & Hc2)|]; [|done].
exists d; split; [|transitivity c]; done. exists d; split; [|transitivity c]; done.
Qed. Qed.
Lemma principal_R_opN `{!Transitive R} n a b :
R a b principal R a principal R b {n} principal R b.
Proof.
intros; apply principal_R_opN_base; intros c; rewrite /principal.
setoid_rewrite elem_of_list_singleton => ->; eauto.
Qed.
Lemma principal_R_op `{!Transitive R} a b : Lemma principal_R_op `{!Transitive R} a b :
R a b principal R a principal R b principal R b. R a b principal R a principal R b principal R b.
Proof. by intros ? ?; apply (principal_R_opN 0). Qed.
Lemma principal_op_RN n a b x :
R a a principal R a x {n} principal R b R a b.
Proof. Proof.
intros Ha HR. intros; apply principal_R_op_base; intros c; rewrite /principal.
destruct (HR a) as [[z [HR1%elem_of_list_singleton HR2]] _]; set_solver.
last by subst; eauto.
rewrite /op /mra_op /principal below_app below_principal; auto.
Qed. Qed.
Lemma principal_op_R' a b x : Lemma principal_op_R' a b x :
R a a principal R a x principal R b R a b. R a a principal R a x principal R b R a b.
Proof. intros ? ?; eapply (principal_op_RN 0); eauto. Qed. Proof. move=> Ha /(_ a) HR. set_solver. Qed.
Lemma principal_op_R `{!Reflexive R} a b x : Lemma principal_op_R `{!Reflexive R} a b x :
principal R a x principal R b R a b. principal R a x principal R b R a b.
Proof. intros; eapply principal_op_R'; eauto. Qed. Proof. by apply principal_op_R'. Qed.
Lemma principal_includedN `{!PreOrder R} n a b : Lemma principal_included `{!PreOrder R} a b :
principal R a {n} principal R b R a b. principal R a principal R b R a b.
Proof. Proof.
split. split.
- intros [z Hz]; eapply principal_op_RN; first done. by rewrite Hz. - move=> [z Hz]. by eapply principal_op_R.
- intros ?; exists (principal R b); rewrite principal_R_opN; eauto. - intros ?; exists (principal R b). by rewrite principal_R_op.
Qed. Qed.
Lemma principal_included `{!PreOrder R} a b : (* Useful? *)
principal R a principal R b R a b. Lemma principal_includedN `{!PreOrder R} n a b :
Proof. apply (principal_includedN 0). Qed. principal R a {n} principal R b R a b.
Proof. by rewrite -principal_included -cmra_discrete_included_iff. Qed.
Lemma mra_local_update_grow `{!Transitive R} a x b: Lemma mra_local_update_grow `{!Transitive R} a x b:
R a b R a b
...@@ -175,15 +151,8 @@ Section cmra. ...@@ -175,15 +151,8 @@ Section cmra.
apply local_update_unital_discrete. apply local_update_unital_discrete.
intros z _ Habz. intros z _ Habz.
split; first done. split; first done.
intros w; split. intros w. specialize (Habz w).
- intros (y & ->%elem_of_list_singleton & Hy2). set_solver.
exists b; split; first constructor; done.
- intros (y & [->|Hy1]%elem_of_cons & Hy2).
+ exists b; split; first constructor; done.
+ exists b; split; first constructor.
specialize (Habz w) as [_ [c [->%elem_of_list_singleton Hc2]]].
{ exists y; split; first (by apply elem_of_app; right); eauto. }
etrans; eauto.
Qed. Qed.
Lemma mra_local_update_get_frag `{!PreOrder R} a b: Lemma mra_local_update_get_frag `{!PreOrder R} a b:
...@@ -202,45 +171,58 @@ End cmra. ...@@ -202,45 +171,58 @@ End cmra.
Global Arguments mraR {_} _. Global Arguments mraR {_} _.
Global Arguments mraUR {_} _. Global Arguments mraUR {_} _.
(**
If [R] is a partial order, relative to a setoid [S] on the carrier [A],
then [principal R] is proper and injective.
(* Might be useful if the type of elements is an OFE. *) The following theory generalizes over an arbitrary setoid [S] and necessary properties,
Section mra_over_ofe. but is overly general, so we encapsulate the instances in an opt-in module.
Context {A : ofe} {R : relation A}. *)
Module mra_over_rel.
Section mra_over_rel.
Context {A : Type} {R : relation A}.
Implicit Types a b : A. Implicit Types a b : A.
Implicit Types x y : mra R. Implicit Types x y : mra R.
Implicit Type (S : relation A).
Global Instance principal_ne #[export] Instance principal_rel_proper S
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} : `{!Proper (S ==> S ==> iff) R} `{!Reflexive S} :
NonExpansive (principal R). Proper (S ==> ()) (principal R).
Proof. intros n a1 a2 Ha; split; rewrite !below_principal !Ha; done. Qed. Proof. intros a1 a2 Ha; split; rewrite ->!below_principal, !Ha; done. Qed.
Global Instance principal_proper
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
Proper (() ==> ()) (principal R) := ne_proper _.
Lemma principal_inj_related a b : Lemma principal_inj_related a b :
principal R a principal R b R a a R a b. principal R a principal R b R a a R a b.
Proof. Proof. move=> /(_ a). set_solver. Qed.
intros Hab ?.
destruct (Hab a) as [[? [?%elem_of_list_singleton ?]] _];
last by subst; auto.
exists a; rewrite /principal elem_of_list_singleton; done.
Qed.
Lemma principal_inj_general a b : Lemma principal_inj_general S a b :
principal R a principal R b principal R a principal R b
R a a R b b (R a b R b a a b) a b. R a a R b b (R a b R b a S a b) S a b.
Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed. Proof. intros ??? Has; apply Has; apply principal_inj_related; auto. Qed.
Global Instance principal_inj_instance `{!Reflexive R} `{!AntiSymm () R} : #[export] Instance principal_inj {S} `{!Reflexive R} `{!AntiSymm S R} :
Inj () () (principal R). Inj S () (principal R).
Proof. intros ???; apply principal_inj_general; auto. Qed. Proof. intros ???. apply principal_inj_general => //. apply: anti_symm. Qed.
End mra_over_rel.
End mra_over_rel.
Global Instance principal_injN `{!Reflexive R} {Has : AntiSymm () R} n : (* Specialize [mra_over_rel] to equality. Only [principal_inj] seems generally useful. *)
Inj (dist n) (dist n) (principal R). Global Instance principal_inj `{R : relation A} `{!Reflexive R} `{!AntiSymm (=) R} :
Proof. Inj (=) () (principal R) := mra_over_rel.principal_inj.
intros x y Hxy%discrete_iff; last apply _.
eapply equiv_dist; revert Hxy; apply inj; apply _. (* Might be useful if the type of elements is an OFE. *)
Qed. Section mra_over_ofe.
Context {A : ofe} {R : relation A}.
Implicit Types a b : A.
Implicit Types x y : mra R.
Import mra_over_rel.
Global Instance principal_proper
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
Proper (() ==> ()) (principal R) := ne_proper _.
(* TODO: Useful? Clients should rather call equiv_dist. *)
Lemma principal_injN `{!Reflexive R} {Has : AntiSymm () R} n :
Inj (dist n) () (principal R).
Proof. intros x y Hxy%(inj _). by apply equiv_dist. Qed.
End mra_over_ofe. End mra_over_ofe.
Require Import iris.unstable.algebra.monotone.
Section test_mra_over_eq.
Context {A : Type} {R : relation A}.
Context `{!Reflexive R} {Has : AntiSymm (=) R}.
Implicit Types a b : A.
Implicit Types x y : mra R.
Lemma test1 a b : principal R a principal R b a = b.
Proof.
by intros ?%(inj _).
Qed.
End test_mra_over_eq.
Section test_mra_over_ofe.
Context {A : ofe} {R : relation A}.
Implicit Types a b : A.
Implicit Types x y : mra R.
Import mra_over_rel.
Context `{!Reflexive R} {Has : AntiSymm () R}.
Lemma test a b : principal R a principal R b a b.
Proof.
by intros ?%(inj _).
Qed.
Lemma principal_ne
`{!∀ n, Proper ((dist n) ==> (dist n) ==> iff) R} :
NonExpansive (principal R).
Proof. apply _. Abort.
Lemma principal_inj_instance :
Inj () () (principal R).
Proof. apply _. Abort.
(* Also questionable. *)
Instance principal_injN' n :
Inj (dist n) (dist n) (principal R).
Proof. apply principal_injN. Abort.
End test_mra_over_ofe.