Commit 6a0e1c76 authored by Robbert Krebbers's avatar Robbert Krebbers

Merge commit '86304d73' into gen_proofmode

parents 702ad20d 86304d73
......@@ -14,7 +14,7 @@ theories/algebra/dra.v
theories/algebra/cofe_solver.v
theories/algebra/agree.v
theories/algebra/excl.v
theories/algebra/iprod.v
theories/algebra/functions.v
theories/algebra/frac.v
theories/algebra/csum.v
theories/algebra/list.v
......
From iris.algebra Require Export ofe monoid.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Class PCore (A : Type) := pcore : A option A.
......@@ -1462,3 +1463,103 @@ Instance optionURF_contractive F :
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, rFunctor_contractive.
Qed.
(* Dependently-typed functions over a finite domain *)
Section ofe_fun_cmra.
Context `{Hfin : Finite A} {B : A ucmraT}.
Implicit Types f g : ofe_fun B.
Instance ofe_fun_op : Op (ofe_fun B) := λ f g x, f x g x.
Instance ofe_fun_pcore : PCore (ofe_fun B) := λ f, Some (λ x, core (f x)).
Instance ofe_fun_valid : Valid (ofe_fun B) := λ f, x, f x.
Instance ofe_fun_validN : ValidN (ofe_fun B) := λ n f, x, {n} f x.
Definition ofe_fun_lookup_op f g x : (f g) x = f x g x := eq_refl.
Definition ofe_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
Lemma ofe_fun_included_spec (f g : ofe_fun B) : f g x, f x g x.
Proof using Hfin.
split; [by intros [h Hh] x; exists (h x); rewrite /op /ofe_fun_op (Hh x)|].
intros [h ?]%finite_choice. by exists h.
Qed.
Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B).
Proof using Hfin.
apply cmra_total_mixin.
- eauto.
- by intros n f1 f2 f3 Hf x; rewrite ofe_fun_lookup_op (Hf x).
- by intros n f1 f2 Hf x; rewrite ofe_fun_lookup_core (Hf x).
- by intros n f1 f2 Hf ? x; rewrite -(Hf x).
- intros g; split.
+ intros Hg n i; apply cmra_valid_validN, Hg.
+ intros Hg i; apply cmra_valid_validN=> n; apply Hg.
- intros n f Hf x; apply cmra_validN_S, Hf.
- by intros f1 f2 f3 x; rewrite ofe_fun_lookup_op assoc.
- by intros f1 f2 x; rewrite ofe_fun_lookup_op comm.
- by intros f x; rewrite ofe_fun_lookup_op ofe_fun_lookup_core cmra_core_l.
- by intros f x; rewrite ofe_fun_lookup_core cmra_core_idemp.
- intros f1 f2; rewrite !ofe_fun_included_spec=> Hf x.
by rewrite ofe_fun_lookup_core; apply cmra_core_mono, Hf.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
destruct (finite_choice (λ x (yy : B x * B x),
f x yy.1 yy.2 yy.1 {n} f1 x yy.2 {n} f2 x)) as [gg Hgg].
{ intros x. specialize (Hf12 x).
destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
exists (y1,y2); eauto. }
exists (λ x, (gg x).1), (λ x, (gg x).2). split_and!=> -?; naive_solver.
Qed.
Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
Instance ofe_fun_unit : Unit (ofe_fun B) := λ x, ε.
Definition ofe_fun_lookup_empty x : ε x = ε := eq_refl.
Lemma ofe_fun_ucmra_mixin : UcmraMixin (ofe_fun B).
Proof.
split.
- intros x; apply ucmra_unit_valid.
- by intros f x; rewrite ofe_fun_lookup_op left_id.
- constructor=> x. apply core_id_core, _.
Qed.
Canonical Structure ofe_funUR := UcmraT (ofe_fun B) ofe_fun_ucmra_mixin.
Global Instance ofe_fun_unit_discrete :
( i, Discrete (ε : B i)) Discrete (ε : ofe_fun B).
Proof. intros ? f Hf x. by apply: discrete. Qed.
End ofe_fun_cmra.
Arguments ofe_funR {_ _ _} _.
Arguments ofe_funUR {_ _ _} _.
Instance ofe_fun_map_cmra_morphism
`{Finite A} {B1 B2 : A ucmraT} (f : x, B1 x B2 x) :
( x, CmraMorphism (f x)) CmraMorphism (ofe_fun_map f).
Proof.
split; first apply _.
- intros n g Hg x; rewrite /ofe_fun_map; apply (cmra_morphism_validN (f _)), Hg.
- intros. apply Some_proper=>i. apply (cmra_morphism_core (f i)).
- intros g1 g2 i. by rewrite /ofe_fun_map ofe_fun_lookup_op cmra_morphism_op.
Qed.
Program Definition ofe_funURF `{Finite C} (F : C urFunctor) : urFunctor := {|
urFunctor_car A B := ofe_funUR (λ c, urFunctor_car (F c) A B);
urFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
|}.
Next Obligation.
intros C ?? F A1 A2 B1 B2 n ?? g.
by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
Qed.
Next Obligation.
intros C ?? F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
apply ofe_fun_map_ext=> y; apply urFunctor_id.
Qed.
Next Obligation.
intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose.
apply ofe_fun_map_ext=>y; apply urFunctor_compose.
Qed.
Instance ofe_funURF_contractive `{Finite C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (ofe_funURF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
by apply ofe_funC_map_ne=>c; apply urFunctor_contractive.
Qed.
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
From stdpp Require Import finite.
Set Default Proof Using "Type".
Definition ofe_fun_insert `{EqDecision A} {B : A ofeT}
(x : A) (y : B x) (f : ofe_fun B) : ofe_fun B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Instance: Params (@ofe_fun_insert) 5.
Definition ofe_fun_singleton `{Finite A} {B : A ucmraT}
(x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
Instance: Params (@ofe_fun_singleton) 5.
Section ofe.
Context `{Heqdec : EqDecision A} {B : A ofeT}.
Implicit Types x : A.
Implicit Types f g : ofe_fun B.
(** Properties of ofe_fun_insert. *)
Global Instance ofe_fun_insert_ne x :
NonExpansive2 (ofe_fun_insert (B:=B) x).
Proof.
intros n y1 y2 ? f1 f2 ? x'; rewrite /ofe_fun_insert.
by destruct (decide _) as [[]|].
Qed.
Global Instance ofe_fun_insert_proper x :
Proper (() ==> () ==> ()) (ofe_fun_insert x) := ne_proper_2 _.
Lemma ofe_fun_lookup_insert f x y : (ofe_fun_insert x y f) x = y.
Proof.
rewrite /ofe_fun_insert; destruct (decide _) as [Hx|]; last done.
by rewrite (proof_irrel Hx eq_refl).
Qed.
Lemma ofe_fun_lookup_insert_ne f x x' y :
x x' (ofe_fun_insert x y f) x' = f x'.
Proof. by rewrite /ofe_fun_insert; destruct (decide _). Qed.
Global Instance ofe_fun_insert_discrete f x y :
Discrete f Discrete y Discrete (ofe_fun_insert x y f).
Proof.
intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
- rewrite ofe_fun_lookup_insert.
apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert.
- rewrite ofe_fun_lookup_insert_ne //.
apply: discrete. by rewrite -(Heq x') ofe_fun_lookup_insert_ne.
Qed.
End ofe.
Section cmra.
Context `{Finite A} {B : A ucmraT}.
Implicit Types x : A.
Implicit Types f g : ofe_fun B.
Global Instance ofe_fun_singleton_ne x :
NonExpansive (ofe_fun_singleton x : B x _).
Proof. intros n y1 y2 ?; apply ofe_fun_insert_ne. done. by apply equiv_dist. Qed.
Global Instance ofe_fun_singleton_proper x :
Proper (() ==> ()) (ofe_fun_singleton x) := ne_proper _.
Lemma ofe_fun_lookup_singleton x (y : B x) : (ofe_fun_singleton x y) x = y.
Proof. by rewrite /ofe_fun_singleton ofe_fun_lookup_insert. Qed.
Lemma ofe_fun_lookup_singleton_ne x x' (y : B x) :
x x' (ofe_fun_singleton x y) x' = ε.
Proof. intros; by rewrite /ofe_fun_singleton ofe_fun_lookup_insert_ne. Qed.
Global Instance ofe_fun_singleton_discrete x (y : B x) :
( i, Discrete (ε : B i)) Discrete y Discrete (ofe_fun_singleton x y).
Proof. apply _. Qed.
Lemma ofe_fun_singleton_validN n x (y : B x) : {n} ofe_fun_singleton x y {n} y.
Proof.
split; [by move=>/(_ x); rewrite ofe_fun_lookup_singleton|].
move=>Hx x'; destruct (decide (x = x')) as [->|];
rewrite ?ofe_fun_lookup_singleton ?ofe_fun_lookup_singleton_ne //.
by apply ucmra_unit_validN.
Qed.
Lemma ofe_fun_core_singleton x (y : B x) :
core (ofe_fun_singleton x y) ofe_fun_singleton x (core y).
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
?ofe_fun_lookup_singleton_ne // (core_id_core ).
Qed.
Global Instance ofe_fun_singleton_core_id x (y : B x) :
CoreId y CoreId (ofe_fun_singleton x y).
Proof. by rewrite !core_id_total ofe_fun_core_singleton=> ->. Qed.
Lemma ofe_fun_op_singleton (x : A) (y1 y2 : B x) :
ofe_fun_singleton x y1 ofe_fun_singleton x y2 ofe_fun_singleton x (y1 y2).
Proof.
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton.
- by rewrite ofe_fun_lookup_op !ofe_fun_lookup_singleton_ne // left_id.
Qed.
Lemma ofe_fun_insert_updateP x (P : B x Prop) (Q : ofe_fun B Prop) g y1 :
y1 ~~>: P ( y2, P y2 Q (ofe_fun_insert x y2 g))
ofe_fun_insert x y1 g ~~>: Q.
Proof.
intros Hy1 HP; apply cmra_total_updateP.
intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
{ move: (Hg x). by rewrite ofe_fun_lookup_op ofe_fun_lookup_insert. }
exists (ofe_fun_insert x y2 g); split; [auto|].
intros x'; destruct (decide (x' = x)) as [->|];
rewrite ofe_fun_lookup_op ?ofe_fun_lookup_insert //; [].
move: (Hg x'). by rewrite ofe_fun_lookup_op !ofe_fun_lookup_insert_ne.
Qed.
Lemma ofe_fun_insert_updateP' x (P : B x Prop) g y1 :
y1 ~~>: P
ofe_fun_insert x y1 g ~~>: λ g', y2, g' = ofe_fun_insert x y2 g P y2.
Proof. eauto using ofe_fun_insert_updateP. Qed.
Lemma ofe_fun_insert_update g x y1 y2 :
y1 ~~> y2 ofe_fun_insert x y1 g ~~> ofe_fun_insert x y2 g.
Proof.
rewrite !cmra_update_updateP; eauto using ofe_fun_insert_updateP with subst.
Qed.
Lemma ofe_fun_singleton_updateP x (P : B x Prop) (Q : ofe_fun B Prop) y1 :
y1 ~~>: P ( y2, P y2 Q (ofe_fun_singleton x y2))
ofe_fun_singleton x y1 ~~>: Q.
Proof. rewrite /ofe_fun_singleton; eauto using ofe_fun_insert_updateP. Qed.
Lemma ofe_fun_singleton_updateP' x (P : B x Prop) y1 :
y1 ~~>: P
ofe_fun_singleton x y1 ~~>: λ g, y2, g = ofe_fun_singleton x y2 P y2.
Proof. eauto using ofe_fun_singleton_updateP. Qed.
Lemma ofe_fun_singleton_update x (y1 y2 : B x) :
y1 ~~> y2 ofe_fun_singleton x y1 ~~> ofe_fun_singleton x y2.
Proof. eauto using ofe_fun_insert_update. Qed.
Lemma ofe_fun_singleton_updateP_empty x (P : B x Prop) (Q : ofe_fun B Prop) :
ε ~~>: P ( y2, P y2 Q (ofe_fun_singleton x y2)) ε ~~>: Q.
Proof.
intros Hx HQ; apply cmra_total_updateP.
intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
exists (ofe_fun_singleton x y2); split; [by apply HQ|].
intros x'; destruct (decide (x' = x)) as [->|].
- by rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton.
- rewrite ofe_fun_lookup_op ofe_fun_lookup_singleton_ne //. apply Hg.
Qed.
Lemma ofe_fun_singleton_updateP_empty' x (P : B x Prop) :
ε ~~>: P ε ~~>: λ g, y2, g = ofe_fun_singleton x y2 P y2.
Proof. eauto using ofe_fun_singleton_updateP_empty. Qed.
Lemma ofe_fun_singleton_update_empty x (y : B x) :
ε ~~> y ε ~~> ofe_fun_singleton x y.
Proof.
rewrite !cmra_update_updateP;
eauto using ofe_fun_singleton_updateP_empty with subst.
Qed.
End cmra.
This diff is collapsed.
......@@ -507,42 +507,6 @@ Section fixpointAB_ne.
Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_B_ne. Qed.
End fixpointAB_ne.
(** Function space *)
(* We make [ofe_fun] a definition so that we can register it as a canonical
structure. *)
Definition ofe_fun (A : Type) (B : ofeT) := A B.
Section ofe_fun.
Context {A : Type} {B : ofeT}.
Instance ofe_fun_equiv : Equiv (ofe_fun A B) := λ f g, x, f x g x.
Instance ofe_fun_dist : Dist (ofe_fun A B) := λ n f g, x, f x {n} g x.
Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun A B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
intros Hfg k; apply equiv_dist=> n; apply Hfg.
- intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
Canonical Structure ofe_funC := OfeT (ofe_fun A B) ofe_fun_ofe_mixin.
Program Definition ofe_fun_chain `(c : chain ofe_funC)
(x : A) : chain B := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
{ compl c x := compl (ofe_fun_chain c x) }.
Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
End ofe_fun.
Arguments ofe_funC : clear implicits.
Notation "A -c> B" :=
(ofe_funC A B) (at level 99, B at level 200, right associativity).
Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
Inhabited (A -c> B) := populate (λ _, inhabitant).
(** Non-expansive function space *)
Record ofe_mor (A B : ofeT) : Type := CofeMor {
ofe_mor_car :> A B;
......@@ -758,37 +722,6 @@ Proof.
by apply prodC_map_ne; apply cFunctor_contractive.
Qed.
Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') :
NonExpansive (compose f : (A -c> B) A -c> B').
Proof. intros n g g' Hf x; simpl. by rewrite (Hf x). Qed.
Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
@CofeMor (_ -c> _) (_ -c> _) (compose f) _.
Instance ofe_funC_map_ne {A B B'} :
NonExpansive (@ofe_funC_map A B B').
Proof. intros n f f' Hf g x. apply Hf. Qed.
Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
cFunctor_car A B := ofe_funC T (cFunctor_car F A B);
cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (cFunctor_map F fg)
|}.
Next Obligation.
intros ?? A1 A2 B1 B2 n ???; by apply ofe_funC_map_ne; apply cFunctor_ne.
Qed.
Next Obligation. intros F1 F2 A B ??. by rewrite /= /compose /= !cFunctor_id. Qed.
Next Obligation.
intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
by rewrite !cFunctor_compose.
Qed.
Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
cFunctorContractive F cFunctorContractive (ofe_funCF T F).
Proof.
intros ?? A1 A2 B1 B2 n ???;
by apply ofe_funC_map_ne; apply cFunctor_contractive.
Qed.
Program Definition ofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
cFunctor_car A B := cFunctor_car F1 B A -n> cFunctor_car F2 A B;
cFunctor_map A1 A2 B1 B2 fg :=
......@@ -1150,6 +1083,106 @@ Proof.
destruct n as [|n]; simpl in *; first done. apply cFunctor_ne, Hfg.
Qed.
(* Dependently-typed functions over a discrete domain *)
(* We make [ofe_fun] a definition so that we can register it as a canonical
structure. *)
Definition ofe_fun {A} (B : A ofeT) := x : A, B x.
Section ofe_fun.
Context {A : Type} {B : A ofeT}.
Implicit Types f g : ofe_fun B.
Instance ofe_fun_equiv : Equiv (ofe_fun B) := λ f g, x, f x g x.
Instance ofe_fun_dist : Dist (ofe_fun B) := λ n f g, x, f x {n} g x.
Definition ofe_fun_ofe_mixin : OfeMixin (ofe_fun B).
Proof.
split.
- intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
intros Hfg k; apply equiv_dist=> n; apply Hfg.
- intros n; split.
+ by intros f x.
+ by intros f g ? x.
+ by intros f g h ?? x; trans (g x).
- by intros n f g ? x; apply dist_S.
Qed.
Canonical Structure ofe_funC := OfeT (ofe_fun B) ofe_fun_ofe_mixin.
Program Definition ofe_fun_chain `(c : chain ofe_funC)
(x : A) : chain (B x) := {| chain_car n := c n x |}.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Global Program Instance ofe_fun_cofe `{ x, Cofe (B x)} : Cofe ofe_funC :=
{ compl c x := compl (ofe_fun_chain c x) }.
Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
Global Instance ofe_fun_inhabited `{ x, Inhabited (B x)} : Inhabited ofe_funC :=
populate (λ _, inhabitant).
Global Instance ofe_fun_lookup_discrete `{EqDecision A} f x :
Discrete f Discrete (f x).
Proof.
intros Hf y ?.
set (g x' := if decide (x = x') is left H then eq_rect _ B y _ H else f x').
trans (g x).
{ apply Hf=> x'. unfold g. by destruct (decide _) as [[]|]. }
unfold g. destruct (decide _) as [Hx|]; last done.
by rewrite (proof_irrel Hx eq_refl).
Qed.
End ofe_fun.
Arguments ofe_funC {_} _.
Notation "A -c> B" :=
(@ofe_funC A (λ _, B)) (at level 99, B at level 200, right associativity).
Definition ofe_fun_map {A} {B1 B2 : A ofeT} (f : x, B1 x B2 x)
(g : ofe_fun B1) : ofe_fun B2 := λ x, f _ (g x).
Lemma ofe_fun_map_ext {A} {B1 B2 : A ofeT} (f1 f2 : x, B1 x B2 x)
(g : ofe_fun B1) :
( x, f1 x (g x) f2 x (g x)) ofe_fun_map f1 g ofe_fun_map f2 g.
Proof. done. Qed.
Lemma ofe_fun_map_id {A} {B : A ofeT} (g : ofe_fun B) :
ofe_fun_map (λ _, id) g = g.
Proof. done. Qed.
Lemma ofe_fun_map_compose {A} {B1 B2 B3 : A ofeT}
(f1 : x, B1 x B2 x) (f2 : x, B2 x B3 x) (g : ofe_fun B1) :
ofe_fun_map (λ x, f2 x f1 x) g = ofe_fun_map f2 (ofe_fun_map f1 g).
Proof. done. Qed.
Instance ofe_fun_map_ne {A} {B1 B2 : A ofeT} (f : x, B1 x B2 x) n :
( x, Proper (dist n ==> dist n) (f x))
Proper (dist n ==> dist n) (ofe_fun_map f).
Proof. by intros ? y1 y2 Hy x; rewrite /ofe_fun_map (Hy x). Qed.
Definition ofe_funC_map {A} {B1 B2 : A ofeT} (f : ofe_fun (λ x, B1 x -n> B2 x)) :
ofe_funC B1 -n> ofe_funC B2 := CofeMor (ofe_fun_map f).
Instance ofe_funC_map_ne {A} {B1 B2 : A ofeT} :
NonExpansive (@ofe_funC_map A B1 B2).
Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
Program Definition ofe_funCF {C} (F : C cFunctor) : cFunctor := {|
cFunctor_car A B := ofe_funC (λ c, cFunctor_car (F c) A B);
cFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, cFunctor_map (F c) fg)
|}.
Next Obligation.
intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply cFunctor_ne.
Qed.
Next Obligation.
intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
apply ofe_fun_map_ext=> y; apply cFunctor_id.
Qed.
Next Obligation.
intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -ofe_fun_map_compose.
apply ofe_fun_map_ext=>y; apply cFunctor_compose.
Qed.
Notation "T -c> F" := (@ofe_funCF T%type (λ _, F%CF)) : cFunctor_scope.
Instance ofe_funCF_contractive `{Finite C} (F : C cFunctor) :
( c, cFunctorContractive (F c)) cFunctorContractive (ofe_funCF F).
Proof.
intros ? A1 A2 B1 B2 n ?? g.
by apply ofe_funC_map_ne=>c; apply cFunctor_contractive.
Qed.
(** Constructing isomorphic OFEs *)
Lemma iso_ofe_mixin {A : ofeT} `{Equiv B, Dist B} (g : B A)
(g_equiv : y1 y2, y1 y2 g y1 g y2)
......
......@@ -49,7 +49,7 @@ Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Lemma ownM_unit' : uPred_ownM ε True.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
Lemma affinely_plainly_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
rewrite affine_affinely.
......
From iris.base_logic Require Export base_logic.
From iris.algebra Require Import iprod gmap.
From iris.algebra Require Import gmap.
From iris.algebra Require cofe_solver.
Set Default Proof Using "Type".
......@@ -47,7 +47,7 @@ Definition gname := positive.
(** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
Definition iResF (Σ : gFunctors) : urFunctor :=
iprodURF (λ i, gmapURF gname (Σ i)).
ofe_funURF (λ i, gmapURF gname (Σ i)).
(** We define functions for the empty list of functors, the singleton list of
......@@ -116,7 +116,7 @@ construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors ofeT.
Definition iResUR (Σ : gFunctors) : ucmraT :=
iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Notation iProp Σ := (uPredC (iResUR Σ)).
Parameter iProp_unfold: {Σ}, iProp Σ -n> iPreProp Σ.
......@@ -134,7 +134,7 @@ Module Export iProp_solution : iProp_solution_sig.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
Definition iResUR (Σ : gFunctors) : ucmraT :=
iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
ofe_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
Notation iProp Σ := (uPredC (iResUR Σ)).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
......
From iris.algebra Require Import iprod gmap.
From iris.algebra Require Import functions gmap.
From iris.base_logic.lib Require Export iprop.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
......@@ -48,7 +48,7 @@ Ltac solve_inG :=
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
......@@ -67,11 +67,11 @@ Implicit Types a : A.
(** ** Properties of [iRes_singleton] *)
Global Instance iRes_singleton_ne γ :
NonExpansive (@iRes_singleton Σ A _ γ).
Proof. by intros n a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
Proof. by intros n a a' Ha; apply ofe_fun_singleton_ne; rewrite Ha. Qed.
Lemma iRes_singleton_op γ a1 a2 :
iRes_singleton γ (a1 a2) iRes_singleton γ a1 iRes_singleton γ a2.
Proof.
by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
by rewrite /iRes_singleton ofe_fun_op_singleton op_singleton cmra_transport_op.
Qed.
(** ** Properties of [own] *)
......@@ -91,7 +91,7 @@ Proof. intros a1 a2. apply own_mono. Qed.
Lemma own_valid γ a : own γ a a.
Proof.
rewrite !own_eq /own_def ownM_valid /iRes_singleton.
rewrite iprod_validI (forall_elim (inG_id _)) iprod_lookup_singleton.
rewrite ofe_fun_validI (forall_elim (inG_id _)) ofe_fun_lookup_singleton.
rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
(* implicit arguments differ a bit *)
by trans ( cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
......@@ -118,8 +118,8 @@ Lemma own_alloc_strong a (G : gset gname) :
Proof.
intros Ha.
rewrite -(bupd_mono ( m, γ, γ G m = iRes_singleton γ a uPred_ownM m)%I).
- rewrite /uPred_valid /bi_valid ownM_empty.
eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (