diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v index 0c1a040fe84a3579d0eb511bb74d34e1ac80caf9..ead9780844ed6546cb6057f31d43902d5558d648 100644 --- a/theories/algebra/cmra.v +++ b/theories/algebra/cmra.v @@ -61,7 +61,7 @@ Section mixin. mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x; mixin_cmra_extend n x y1 y2 : ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → - ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 + { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } } }. End mixin. @@ -135,7 +135,7 @@ Section cmra_mixin. Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed. Lemma cmra_extend n x y1 y2 : ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → - ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2. + { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }. Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed. End cmra_mixin. @@ -722,7 +722,7 @@ Section cmra_total. Context (validN_op_l : ∀ n (x y : A), ✓{n} (x ⋅ y) → ✓{n} x). Context (extend : ∀ n (x y1 y2 : A), ✓{n} x → x ≡{n}≡ y1 ⋅ y2 → - ∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2). + { z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }). Lemma cmra_total_mixin : CmraMixin A. Proof using Type*. split; auto. @@ -1311,7 +1311,7 @@ Section option. eauto using cmra_validN_op_l. - intros n ma mb1 mb2. destruct ma as [a|], mb1 as [b1|], mb2 as [b2|]; intros Hx Hx'; - inversion_clear Hx'; auto. + (try by exfalso; inversion Hx'); (try (apply (inj Some) in Hx')). + destruct (cmra_extend n a b1 b2) as (c1&c2&?&?&?); auto. by exists (Some c1), (Some c2); repeat constructor. + by exists (Some a), None; repeat constructor. @@ -1475,7 +1475,7 @@ Qed. (* Dependently-typed functions over a finite discrete domain *) Section ofe_fun_cmra. - Context `{Hfin : Finite A} {B : A → ucmraT}. + Context `{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. @@ -1486,14 +1486,17 @@ 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_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. + Lemma ofe_fun_included_spec_1 (f g : ofe_fun B) x : f ≼ g → f x ≼ g x. + Proof. by intros [h Hh]; exists (h x); rewrite /op /ofe_fun_op (Hh x). Qed. + + Lemma ofe_fun_included_spec `{Hfin : Finite A} (f g : ofe_fun B) : f ≼ g ↔ ∀ x, f x ≼ g x. + Proof. + split; [by intros; apply ofe_fun_included_spec_1|]. + intros [h ?]%finite_choice; by exists h. Qed. Lemma ofe_fun_cmra_mixin : CmraMixin (ofe_fun B). - Proof using Hfin. + Proof. apply cmra_total_mixin. - eauto. - by intros n f1 f2 f3 Hf x; rewrite ofe_fun_lookup_op (Hf x). @@ -1507,16 +1510,16 @@ Section ofe_fun_cmra. - 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 f1 f2 Hf12. exists (core f2)=>x. rewrite ofe_fun_lookup_op. + apply (ofe_fun_included_spec_1 _ _ x), (cmra_core_mono (f1 x)) in Hf12. + 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 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. + assert (FUN := λ x, cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)). + exists (λ x, projT1 (FUN x)), (λ x, proj1_sig (projT2 (FUN x))). + split; [|split]=>x; [rewrite ofe_fun_lookup_op| |]; + by destruct (FUN x) as (?&?&?&?&?). Qed. Canonical Structure ofe_funR := CmraT (ofe_fun B) ofe_fun_cmra_mixin. @@ -1537,11 +1540,10 @@ Section ofe_fun_cmra. Proof. intros ? f Hf x. by apply: discrete. Qed. End ofe_fun_cmra. -Arguments ofe_funR {_ _ _} _. -Arguments ofe_funUR {_ _ _} _. +Arguments ofe_funR {_} _. +Arguments ofe_funUR {_} _. -Instance ofe_fun_map_cmra_morphism - `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) : +Instance ofe_fun_map_cmra_morphism {A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) : (∀ x, CmraMorphism (f x)) → CmraMorphism (ofe_fun_map f). Proof. split; first apply _. @@ -1550,23 +1552,22 @@ Proof. - 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 := {| +Program Definition ofe_funURF {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. + 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). + 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. + 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) : +Instance ofe_funURF_contractive {C} (F : C → urFunctor) : (∀ c, urFunctorContractive (F c)) → urFunctorContractive (ofe_funURF F). Proof. intros ? A1 A2 B1 B2 n ?? g. diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v index f330344a0cdb00d86ee640574af8a206a360d019..7e3c9047ca283cd6ee31de6b0d692b2974bfa3ff 100644 --- a/theories/algebra/csum.v +++ b/theories/algebra/csum.v @@ -239,11 +239,11 @@ Proof. exists (Cinr cb'). rewrite csum_included; eauto 10. - intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done. - intros n [a|b|] y1 y2 Hx Hx'. - + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'. - destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); auto. + + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'. + destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); [done|apply (inj Cinl), Hx'|]. exists (Cinl z1), (Cinl z2). by repeat constructor. - + destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'. - destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); auto. + + destruct y1 as [a1|b1|], y2 as [a2|b2|]; try by exfalso; inversion Hx'. + destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); [done|apply (inj Cinr), Hx'|]. exists (Cinr z1), (Cinr z2). by repeat constructor. + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'. Qed. diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v index b73aaa01e635b775c07fb9e40d0a71903b410877..ddf7a9295899cceef2168135e0b16d7882edfad7 100644 --- a/theories/algebra/excl.v +++ b/theories/algebra/excl.v @@ -87,7 +87,7 @@ Proof. - by intros [?|] [?|] [?|]; constructor. - by intros [?|] [?|]; constructor. - by intros n [?|] [?|]. - - intros n x [?|] [?|] ?; inversion_clear 1; eauto. + - intros n x [?|] [?|] ? Hx; eexists _, _; inversion_clear Hx; eauto. Qed. Canonical Structure exclR := CmraT (excl A) excl_cmra_mixin. diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v index 62c200d3a29649b1308a1423ad35d271e19057ca..6983a95f3fac022c900e358f5e119719934ccac4 100644 --- a/theories/algebra/functions.v +++ b/theories/algebra/functions.v @@ -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. Instance: Params (@ofe_fun_insert) 5. -Definition ofe_fun_singleton `{Finite A} {B : A → ucmraT} +Definition ofe_fun_singleton `{EqDecision A} {B : A → ucmraT} (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε. Instance: Params (@ofe_fun_singleton) 5. @@ -48,7 +48,7 @@ Section ofe. End ofe. Section cmra. - Context `{Finite A} {B : A → ucmraT}. + Context `{EqDecision A} {B : A → ucmraT}. Implicit Types x : A. Implicit Types f g : ofe_fun B. diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v index b9a995537ea553ed15d6c179b48769353d47beb4..fd4df4077a947e71a69c410b39c14357bbda90cc 100644 --- a/theories/algebra/gmap.v +++ b/theories/algebra/gmap.v @@ -147,30 +147,16 @@ Proof. rewrite !lookup_core. by apply cmra_core_mono. - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i). by rewrite -lookup_op. - - intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm. - { eexists ∅, ∅. split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i); - rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. } - destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2'). - { intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|]. - + intros _. by rewrite Hi. - + by rewrite lookup_insert_ne. } - { intros j; move: Hm=> /(_ j); destruct (decide (i = j)) as [->|]. - + intros _. by rewrite lookup_op !lookup_delete Hi. - + 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. + - intros n m y1 y2 Hm Heq. + refine ((λ FUN, _) (λ i, cmra_extend n (m !! i) (y1 !! i) (y2 !! i) (Hm i) _)); + last by rewrite -lookup_op. + exists (map_imap (λ i _, projT1 (FUN i)) y1). + exists (map_imap (λ i _, proj1_sig (projT2 (FUN i))) y2). + split; [|split]=>i; rewrite ?lookup_op !lookup_imap; + destruct (FUN i) as (z1i&z2i&Hmi&Hz1i&Hz2i)=>/=. + + destruct (y1 !! i), (y2 !! i); inversion Hz1i; inversion Hz2i; subst=>//. + + revert Hz1i. case: (y1!!i)=>[?|] //. + + revert Hz2i. case: (y2!!i)=>[?|] //. Qed. Canonical Structure gmapR := CmraT (gmap K A) gmap_cmra_mixin. diff --git a/theories/algebra/list.v b/theories/algebra/list.v index 67f56c2f782c5a6844f9c9998799824eeb3821f3..ec603646ce481741cec12a3427a1fa5c5c5cea27 100644 --- a/theories/algebra/list.v +++ b/theories/algebra/list.v @@ -212,12 +212,14 @@ Section cmra. - intros n l1 l2. rewrite !list_lookup_validN. setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l. - intros n l. - induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl; inversion_clear 1. + induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Heq; + (try by exfalso; inversion Heq). + by exists [], []. - + exists [], (x :: l); by repeat constructor. - + exists (x :: l), []; by repeat constructor. - + inversion_clear Hl. destruct (IH l1 l2) as (l1'&l2'&?&?&?), - (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto. + + exists [], (x :: l); inversion Heq; by repeat constructor. + + exists (x :: l), []; inversion Heq; by repeat constructor. + + destruct (IH l1 l2) as (l1'&l2'&?&?&?), + (cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); + [by inversion_clear Heq; inversion_clear Hl..|]. exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto. Qed. Canonical Structure listR := CmraT (list A) list_cmra_mixin. diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v index d2724cedd474bf08d4910d9b4ba9e1e021a08744..6cb248ce7e7ae690522d12d3c6a8d027d1cac635 100644 --- a/theories/base_logic/primitive.v +++ b/theories/base_logic/primitive.v @@ -639,10 +639,11 @@ Qed. (* Function extensionality *) Lemma ofe_morC_equivI {A B : ofeT} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x. Proof. by unseal. Qed. -Lemma ofe_fun_equivI `{B : A → ofeT} (g1 g2 : ofe_fun B) : g1 ≡ g2 ⊣⊢ ∀ i, g1 i ≡ g2 i. +Lemma ofe_fun_equivI `{B : A → ofeT} (g1 g2 : ofe_fun B) : + g1 ≡ g2 ⊣⊢ ∀ i, g1 i ≡ g2 i. Proof. by uPred.unseal. Qed. -Lemma ofe_fun_validI `{Finite A} {B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i. +Lemma ofe_fun_validI `{B : A → ucmraT} (g : ofe_fun B) : ✓ g ⊣⊢ ∀ i, ✓ g i. Proof. by uPred.unseal. Qed. (* Sigma OFE *)