Commit f66f7f16 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Revert "Remove the domain finiteness hypothesis for the function CMRA, and put...

Revert "Remove the domain finiteness hypothesis for the function CMRA, and put cmra_extend in Type."

This reverts commit fa897ff5.
parent fa897ff5
...@@ -61,7 +61,7 @@ Section mixin. ...@@ -61,7 +61,7 @@ Section mixin.
mixin_cmra_validN_op_l n x y : {n} (x y) {n} x; mixin_cmra_validN_op_l n x y : {n} (x y) {n} x;
mixin_cmra_extend n x y1 y2 : mixin_cmra_extend n x y1 y2 :
{n} x x {n} y1 y2 {n} x x {n} y1 y2
{ z1 : A & { z2 | x z1 z2 z1 {n} y1 z2 {n} y2 } } z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2
}. }.
End mixin. End mixin.
...@@ -135,7 +135,7 @@ Section cmra_mixin. ...@@ -135,7 +135,7 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed. Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_extend n x y1 y2 : Lemma cmra_extend n x y1 y2 :
{n} x x {n} y1 y2 {n} x x {n} y1 y2
{ z1 : A & { z2 | x z1 z2 z1 {n} y1 z2 {n} y2 } }. z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed. Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin. End cmra_mixin.
...@@ -722,7 +722,7 @@ Section cmra_total. ...@@ -722,7 +722,7 @@ Section cmra_total.
Context (validN_op_l : n (x y : A), {n} (x y) {n} x). Context (validN_op_l : n (x y : A), {n} (x y) {n} x).
Context (extend : n (x y1 y2 : A), Context (extend : n (x y1 y2 : A),
{n} x x {n} y1 y2 {n} x x {n} y1 y2
{ z1 : A & { z2 | x z1 z2 z1 {n} y1 z2 {n} y2 } }). z1 z2, x z1 z2 z1 {n} y1 z2 {n} y2).
Lemma cmra_total_mixin : CmraMixin A. Lemma cmra_total_mixin : CmraMixin A.
Proof using Type*. Proof using Type*.
split; auto. split; auto.
...@@ -1311,7 +1311,7 @@ Section option. ...@@ -1311,7 +1311,7 @@ Section option.
eauto using cmra_validN_op_l. eauto using cmra_validN_op_l.
- intros n ma mb1 mb2. - intros n ma mb1 mb2.
destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx'; destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx';
(try by exfalso; inversion Hx'); (try (apply (inj Some) in Hx')). inversion_clear Hx'; auto.
+ destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto. + destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto.
by exists (Some c1), (Some c2); repeat constructor. by exists (Some c1), (Some c2); repeat constructor.
+ by exists (Some a), None; repeat constructor. + by exists (Some a), None; repeat constructor.
...@@ -1475,7 +1475,7 @@ Qed. ...@@ -1475,7 +1475,7 @@ Qed.
(* Dependently-typed functions over a finite discrete domain *) (* Dependently-typed functions over a finite discrete domain *)
Section ofe_fun_cmra. Section ofe_fun_cmra.
Context {A: Type} {B : A ucmraT}. Context `{Hfin : Finite A} {B : A ucmraT}.
Implicit Types f g : ofe_fun B. 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_op : Op (ofe_fun B) := λ f g x, f x g x.
...@@ -1486,17 +1486,14 @@ Section ofe_fun_cmra. ...@@ -1486,17 +1486,14 @@ Section ofe_fun_cmra.
Definition ofe_fun_lookup_op f g x : (f g) x = f x g x := eq_refl. 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. Definition ofe_fun_lookup_core f x : (core f) x = core (f x) := eq_refl.
Lemma ofe_fun_included_spec_1 (f g : ofe_fun B) x : f g f x g x. Lemma ofe_fun_included_spec (f g : ofe_fun B) : f g x, f x g x.
Proof. by intros [h Hh]; exists (h x); rewrite /op /ofe_fun_op (Hh x). Qed. Proof using Hfin.
split; [by intros [h Hh] x; exists (h x); rewrite /op /ofe_fun_op (Hh x)|].
Lemma ofe_fun_included_spec `{Hfin : Finite A} (f g : ofe_fun B) : f g x, f x g x. intros [h ?]%finite_choice. by exists h.
Proof.
split; [by intros; apply ofe_fun_included_spec_1|].
intros [h ?]%finite_choice; by exists h.
Qed. Qed.
Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B). Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B).
Proof. Proof using Hfin.
apply cmra_total_mixin. apply cmra_total_mixin.
- eauto. - eauto.
- by intros n f1 f2 f3 Hf x; rewrite ofe_fun_lookup_op (Hf x). - by intros n f1 f2 f3 Hf x; rewrite ofe_fun_lookup_op (Hf x).
...@@ -1510,16 +1507,16 @@ Section ofe_fun_cmra. ...@@ -1510,16 +1507,16 @@ Section ofe_fun_cmra.
- by intros f1 f2 x; rewrite ofe_fun_lookup_op comm. - 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_op ofe_fun_lookup_core cmra_core_l.
- by intros f x; rewrite ofe_fun_lookup_core cmra_core_idemp. - by intros f x; rewrite ofe_fun_lookup_core cmra_core_idemp.
- intros f1 f2 Hf12. exists (core f2)=>x. rewrite ofe_fun_lookup_op. - intros f1 f2; rewrite !ofe_fun_included_spec=> Hf x.
apply (ofe_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12. by rewrite ofe_fun_lookup_core; apply cmra_core_mono, Hf.
rewrite !ofe_fun_lookup_core. destruct Hf12 as [? ->].
rewrite assoc -cmra_core_dup //.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf. - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12. - intros n f f1 f2 Hf Hf12.
assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). destruct (finite_choice (λ x (yy : B x * B x),
exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))). f x yy.1 yy.2 yy.1 {n} f1 x yy.2 {n} f2 x)) as [gg Hgg].
split; [|split]=>x; [rewrite ofe_fun_lookup_op| |]; { intros x. specialize (Hf12 x).
by destruct (FUN x) as (?&?&?&?&?). 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. Qed.
Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin. Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin.
...@@ -1540,10 +1537,11 @@ Section ofe_fun_cmra. ...@@ -1540,10 +1537,11 @@ Section ofe_fun_cmra.
Proof. intros ? f Hf x. by apply: discrete. Qed. Proof. intros ? f Hf x. by apply: discrete. Qed.
End ofe_fun_cmra. End ofe_fun_cmra.
Arguments ofe_funR {_} _. Arguments ofe_funR {_ _ _} _.
Arguments ofe_funUR {_} _. Arguments ofe_funUR {_ _ _} _.
Instance ofe_fun_map_cmra_morphism {A} {B1 B2 : A ucmraT} (f : x, B1 x B2 x) : 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). ( x, CmraMorphism (f x)) CmraMorphism (ofe_fun_map f).
Proof. Proof.
split; first apply _. split; first apply _.
...@@ -1552,22 +1550,23 @@ Proof. ...@@ -1552,22 +1550,23 @@ Proof.
- intros g1 g2 i. by rewrite /ofe_fun_map ofe_fun_lookup_op cmra_morphism_op. - intros g1 g2 i. by rewrite /ofe_fun_map ofe_fun_lookup_op cmra_morphism_op.
Qed. Qed.
Program Definition ofe_funURF {C} (F : C urFunctor) : urFunctor := {| Program Definition ofe_funURF `{Finite C} (F : C urFunctor) : urFunctor := {|
urFunctor_car A B := ofe_funUR (λ c, urFunctor_car (F c) A B); 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) urFunctor_map A1 A2 B1 B2 fg := ofe_funC_map (λ c, urFunctor_map (F c) fg)
|}. |}.
Next Obligation. Next Obligation.
intros C F A1 A2 B1 B2 n ?? g. by apply ofe_funC_map_ne=>?; apply urFunctor_ne. intros C ?? F A1 A2 B1 B2 n ?? g.
by apply ofe_funC_map_ne=>?; apply urFunctor_ne.
Qed. Qed.
Next Obligation. Next Obligation.
intros C F A B g; simpl. rewrite -{2}(ofe_fun_map_id g). intros C ?? F A B g; simpl. rewrite -{2}(ofe_fun_map_id g).
apply ofe_fun_map_ext=> y; apply urFunctor_id. apply ofe_fun_map_ext=> y; apply urFunctor_id.
Qed. Qed.
Next Obligation. Next Obligation.
intros C F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-ofe_fun_map_compose. 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. apply ofe_fun_map_ext=>y; apply urFunctor_compose.
Qed. Qed.
Instance ofe_funURF_contractive {C} (F : C urFunctor) : Instance ofe_funURF_contractive `{Finite C} (F : C urFunctor) :
( c, urFunctorContractive (F c)) urFunctorContractive (ofe_funURF F). ( c, urFunctorContractive (F c)) urFunctorContractive (ofe_funURF F).
Proof. Proof.
intros ? A1 A2 B1 B2 n ?? g. intros ? A1 A2 B1 B2 n ?? g.
......
...@@ -239,11 +239,11 @@ Proof. ...@@ -239,11 +239,11 @@ Proof.
exists (Cinr cb'). rewrite csum_included; eauto 10. exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done. - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'. - intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'. + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); [done|apply (inj Cinl), Hx'|]. destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); auto.
exists (Cinl z1), (Cinl z2). by repeat constructor. exists (Cinl z1), (Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'. + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); [done|apply (inj Cinr), Hx'|]. destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); auto.
exists (Cinr z1), (Cinr z2). by repeat constructor. exists (Cinr z1), (Cinr z2). by repeat constructor.
+ by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'. + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
Qed. Qed.
......
...@@ -87,7 +87,7 @@ Proof. ...@@ -87,7 +87,7 @@ Proof.
- by intros [?|] [?|] [?|]; constructor. - by intros [?|] [?|] [?|]; constructor.
- by intros [?|] [?|]; constructor. - by intros [?|] [?|]; constructor.
- by intros n [?|] [?|]. - by intros n [?|] [?|].
- intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto. - intros n x [?|] [?|] ?; inversion_clear 1; eauto.
Qed. Qed.
Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin. Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin.
......
...@@ -8,7 +8,7 @@ Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT} ...@@ -8,7 +8,7 @@ Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end. match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Instance: Params (@ofe_fun_insert) 5. Instance: Params (@ofe_fun_insert) 5.
Definition ofe_fun_singleton `{EqDecision A} {B : A ucmraT} Definition ofe_fun_singleton `{Finite A} {B : A ucmraT}
(x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε. (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
Instance: Params (@ofe_fun_singleton) 5. Instance: Params (@ofe_fun_singleton) 5.
...@@ -48,7 +48,7 @@ Section ofe. ...@@ -48,7 +48,7 @@ Section ofe.
End ofe. End ofe.
Section cmra. Section cmra.
Context `{EqDecision A} {B : A ucmraT}. Context `{Finite A} {B : A ucmraT}.
Implicit Types x : A. Implicit Types x : A.
Implicit Types f g : ofe_fun B. Implicit Types f g : ofe_fun B.
......
...@@ -147,16 +147,30 @@ Proof. ...@@ -147,16 +147,30 @@ Proof.
rewrite !lookup_core. by apply cmra_core_mono. rewrite !lookup_core. by apply cmra_core_mono.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op. by rewrite -lookup_op.
- intros n m y1 y2 Hm Heq. - intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm.
refine ((λ FUN, _) (λ i, cmra_extend n (m !! i) (y1 !! i) (y2 !! i) (Hm i) _)); { eexists , . split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
last by rewrite -lookup_op. rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. }
exists (map_imap (λ i _, projT1 (FUN i)) y1). destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2').
exists (map_imap (λ i _, proj1_sig (projT2 (FUN i))) y2). { intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|].
split; [|split]=>i; rewrite ?lookup_op !lookup_imap; + intros _. by rewrite Hi.
destruct (FUN i) as (z1i&z2i&Hmi&Hz1i&Hz2i)=>/=. + by rewrite lookup_insert_ne. }
+ destruct (y1 !! i), (y2 !! i); inversion Hz1i; inversion Hz2i; subst=>//. { intros j; move: Hm=> /(_ j); destruct (decide (i = j)) as [->|].
+ revert Hz1i. case: (y1!!i)=>[?|] //. + intros _. by rewrite lookup_op !lookup_delete Hi.
+ revert Hz2i. case: (y2!!i)=>[?|] //. + by rewrite !lookup_op lookup_insert_ne // !lookup_delete_ne. }
destruct (cmra_extend n (Some x) (m1 !! i) (m2 !! i)) as (y1&y2&?&?&?).
{ move: Hmv=> /(_ i). by rewrite lookup_insert. }
{ move: Hm=> /(_ i). by rewrite lookup_insert lookup_op. }
exists (partial_alter (λ _, y1) i m1'), (partial_alter (λ _, y2) i m2').
split_and!.
+ intros j. destruct (decide (i = j)) as [->|].
* by rewrite lookup_insert lookup_op !lookup_partial_alter.
* by rewrite lookup_insert_ne // Hm' !lookup_op !lookup_partial_alter_ne.
+ intros j. destruct (decide (i = j)) as [->|].
* by rewrite lookup_partial_alter.
* by rewrite lookup_partial_alter_ne // Hm1' lookup_delete_ne.
+ intros j. destruct (decide (i = j)) as [->|].
* by rewrite lookup_partial_alter.
* by rewrite lookup_partial_alter_ne // Hm2' lookup_delete_ne.
Qed. Qed.
Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin. Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin.
......
...@@ -212,14 +212,12 @@ Section cmra. ...@@ -212,14 +212,12 @@ Section cmra.
- intros n l1 l2. rewrite !list_lookup_validN. - intros n l1 l2. rewrite !list_lookup_validN.
setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l. setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
- intros n l. - intros n l.
induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Heq; induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl; inversion_clear 1.
(try by exfalso; inversion Heq).
+ by exists [], []. + by exists [], [].
+ exists [], (x :: l); inversion Heq; by repeat constructor. + exists [], (x :: l); by repeat constructor.
+ exists (x :: l), []; inversion Heq; by repeat constructor. + exists (x :: l), []; by repeat constructor.
+ destruct (IH l1 l2) as (l1'&l2'&?&?&?), + inversion_clear Hl. destruct (IH l1 l2) as (l1'&l2'&?&?&?),
(cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
[by inversion_clear Heq; inversion_clear Hl..|].
exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto. exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
Qed. Qed.
Canonical Structure listR := CmraT (list A) list_cmra_mixin. Canonical Structure listR := CmraT (list A) list_cmra_mixin.
......
...@@ -639,11 +639,10 @@ Qed. ...@@ -639,11 +639,10 @@ Qed.
(* Function extensionality *) (* Function extensionality *)
Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f g x, f x g x. Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f g x, f x g x.
Proof. by unseal. Qed. Proof. by unseal. Qed.
Lemma ofe_fun_equivI `{B : A ofeT} (g1 g2 : ofe_fun B) : Lemma ofe_fun_equivI `{B : A ofeT} (g1 g2 : ofe_fun B) : g1 g2 i, g1 i g2 i.
g1 g2 i, g1 i g2 i.
Proof. by uPred.unseal. Qed. Proof. by uPred.unseal. Qed.
Lemma ofe_fun_validI `{B : A ucmraT} (g : ofe_fun B) : g i, g i. Lemma ofe_fun_validI `{Finite A} {B : A ucmraT} (g : ofe_fun B) : g i, g i.
Proof. by uPred.unseal. Qed. Proof. by uPred.unseal. Qed.
(* Sigma OFE *) (* Sigma OFE *)
......
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