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 (1)
......@@ -464,6 +464,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := {
ra_op_minus x y : x y x y x y
}.
(*
Section discrete.
Context {A : cofeT} `{∀ x : A, Timeless x}.
Context {v : Valid A} `{Unit A, Op A, Minus A} (ra : RA A).
......@@ -480,7 +481,7 @@ Section discrete.
apply (timeless _), dist_le with n; auto with lia.
Qed.
Definition discreteRA : cmraT :=
CMRAT (cofe_mixin A) discrete_cmra_mixin discrete_extend_mixin.
CMRAT (let 'CofeT _ _ _ _ m := A in m) discrete_cmra_mixin discrete_extend_mixin.
Lemma discrete_updateP (x : discreteRA) (P : A → Prop) :
(∀ z, ✓ (x ⋅ z) → ∃ y, P y ∧ ✓ (y ⋅ z)) → x ~~>: P.
Proof. intros Hvalid n z; apply Hvalid. Qed.
......@@ -505,6 +506,7 @@ Section unit.
Global Instance unit_cmra_identity : CMRAIdentity unitRA.
Proof. by split; intros []. Qed.
End unit.
*)
(** ** Product *)
Section prod.
......
......@@ -62,32 +62,33 @@ Class Contractive `{Dist A, Dist B} (f : A -> B) :=
(** Bundeled version *)
Structure cofeT := CofeT {
cofe_car :> Type;
cofe_equiv : Equiv cofe_car;
cofe_dist : Dist cofe_car;
cofe_compl : Compl cofe_car;
cofe_mixin : CofeMixin cofe_car
_ : Equiv cofe_car;
_ : Dist cofe_car;
_ : Compl cofe_car;
_ : CofeMixin cofe_car
}.
Arguments CofeT {_ _ _ _} _.
Add Printing Constructor cofeT.
Existing Instances cofe_equiv cofe_dist cofe_compl.
Instance cofe_equiv (A : cofeT) : Equiv A := let 'CofeT _ e _ _ _ := A in e.
Instance cofe_dist (A : cofeT) : Dist A := let 'CofeT _ _ d _ _ := A in d.
Instance cofe_compl (A : cofeT) : Compl A := let 'CofeT _ _ _ c _ := A in c.
Arguments cofe_car : simpl never.
Arguments cofe_equiv : simpl never.
Arguments cofe_dist : simpl never.
Arguments cofe_compl : simpl never.
Arguments cofe_mixin : simpl never.
(** Lifting properties from the mixin *)
Section cofe_mixin.
Context {A : cofeT}.
Implicit Types x y : A.
Lemma equiv_dist x y : x y n, x {n} y.
Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
Proof. by destruct A as [???? []]. Qed.
Global Instance dist_equivalence n : Equivalence (@dist A _ n).
Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
Proof. by destruct A as [???? []]. Qed.
Lemma dist_S n x y : x {S n} y x {n} y.
Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
Proof. destruct A as [???? []]; auto. Qed.
Lemma conv_compl n (c : chain A) : compl c {n} c (S n).
Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
Proof. destruct A as [???? []]; auto. Qed.
End cofe_mixin.
(** General properties *)
......
......@@ -18,7 +18,49 @@ Proof.
split.
- intros m1 m2; split.
+ by intros Hm n k; apply equiv_dist.
+ intros Hm k; apply equiv_dist; intros n; apply Hm.
+ intros Hm k.
(**
Goal is
@equiv (option (cofe_car A)) (@option_equiv (cofe_car A) (cofe_equiv A))
(@lookup K (cofe_car A) (@gmap K H H0 (cofe_car A)) (@gmap_lookup K H H0 (cofe_car A)) k m1)
(@lookup K (cofe_car A) (@gmap K H H0 (cofe_car A)) (@gmap_lookup K H H0 (cofe_car A)) k m2)
*)
(** LHS of equiv_dist is:
@equiv (cofe_car B) (cofe_equiv B) x y
for some [B : cofeT].
*)
Fail apply equiv_dist.
(* Works: apply @equiv_dist. *)
(* Note that equiv_dist is an iff, so [apply:] needs some help. But it works.
apply: (fun {A} x y => proj2 (@equiv_dist A x y)).
*)
(* I do not think it is just about the type of the projection of the [equiv]
operational typeclass being in the way. The following also fails. *)
change (option (cofe_car A)) with (cofe_car (optionC A)).
Fail apply equiv_dist.
change (@option_equiv (cofe_car A) (cofe_equiv A)) with
(@cofe_equiv (optionC A)).
(* Only now it works *)
apply equiv_dist.
intros n; apply Hm.
- intros n; split.
+ by intros m k.
+ by intros m1 m2 ? k.
......
......@@ -876,12 +876,14 @@ Lemma later_equivI {A : cofeT} (x y : later A) :
(x y)%I ( (later_car x later_car y) : uPred M)%I.
Proof. done. Qed.
(*
(* Discrete *)
(* For equality, there already is timeless_eq *)
Lemma discrete_validI {A : cofeT} `{∀ x : A, Timeless x}
`{Op A, Valid A, Unit A, Minus A} (ra : RA A) (x : discreteRA ra) :
(✓ x)%I ≡ (■ ✓ x : uPred M)%I.
Proof. done. Qed.
*)
(* Timeless *)
Lemma timelessP_spec P : TimelessP P n x, {n} x P 0 x P n x.
......