From 758d8d652f002394eb6f8f2f0b5fee39881356eb Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Wed, 1 Jun 2016 18:59:41 +0200 Subject: [PATCH] Simplify frac : use a pair of a rational and a carrier --- algebra/cmra.v | 6 +- algebra/frac.v | 206 +++++------------------------------------------ heap_lang/heap.v | 46 +++++------ prelude/base.v | 5 ++ 4 files changed, 51 insertions(+), 212 deletions(-) diff --git a/algebra/cmra.v b/algebra/cmra.v index 130a7a78..2b71bea2 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -950,6 +950,10 @@ Section prod. Canonical Structure prodR := CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin. + Lemma pair_op (a a' : A) (b b' : B) : + (a, b) ⋅ (a', b') ≡ (a ⋅ a', b ⋅ b'). + Proof. done. Qed. + Global Instance prod_cmra_total : CMRATotal A → CMRATotal B → CMRATotal prodR. Proof. intros H1 H2 [a b]. destruct (H1 a) as [ca ?], (H2 b) as [cb ?]. @@ -1017,7 +1021,7 @@ Section prod_unit. UCMRAT (A * B) prod_cofe_mixin prod_cmra_mixin prod_ucmra_mixin. Lemma pair_split (x : A) (y : B) : (x, y) ≡ (x, ∅) ⋅ (∅, y). - Proof. constructor; by rewrite /= ?left_id ?right_id. Qed. + Proof. by rewrite pair_op left_id right_id. Qed. End prod_unit. Arguments prodUR : clear implicits. diff --git a/algebra/frac.v b/algebra/frac.v index b967451a..84774bf2 100644 --- a/algebra/frac.v +++ b/algebra/frac.v @@ -5,207 +5,37 @@ Local Arguments op _ _ !_ !_ /. Local Arguments validN _ _ _ !_ /. Local Arguments valid _ _ !_ /. -Inductive frac A := Frac { frac_perm : Qp ; frac_car : A }. -Add Printing Constructor frac. -Arguments Frac {_} _ _. -Arguments frac_perm {_} _. -Arguments frac_car {_} _. -Instance: Params (@Frac) 2. +Notation frac := Qp. -Section cofe. -Context {A : cofeT}. -Implicit Types a b : A. -Implicit Types x y : frac A. +Section frac. -(* Cofe *) -Instance frac_equiv : Equiv (frac A) := λ x y, - frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y. -Instance frac_dist : Dist (frac A) := λ n x y, - frac_perm x = frac_perm y ∧ frac_car x ≡{n}≡ frac_car y. +Canonical Structure fracC := leibnizC frac. -Global Instance Frac_ne q n : Proper (dist n ==> dist n) (@Frac A q). -Proof. by constructor. Qed. -Global Instance Frac_proper q : Proper ((≡) ==> (≡)) (@Frac A q). -Proof. by constructor. Qed. -Global Instance Frac_inj : Inj2 (=) (≡) (≡) (@Frac A). -Proof. by destruct 1. Qed. -Global Instance Frac_dist_inj n : Inj2 (=) (dist n) (dist n) (@Frac A). -Proof. by destruct 1. Qed. +Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc. +Instance frac_pcore : PCore frac := λ _, None. +Instance frac_op : Op frac := λ x y, (x + y)%Qp. -Global Instance frac_perm_ne n : Proper (dist n ==> (=)) (@frac_perm A). -Proof. by destruct 1. Qed. -Global Instance frac_car_ne n : Proper (dist n ==> dist n) (@frac_car A). -Proof. by destruct 1. Qed. -Global Instance frac_perm_proper : Proper ((≡) ==> (=)) (@frac_perm A). -Proof. by destruct 1. Qed. -Global Instance frac_car_proper : Proper ((≡) ==> (≡)) (@frac_car A). -Proof. by destruct 1. Qed. - -Program Definition frac_chain (c : chain (frac A)) : chain A := - {| chain_car n := match c n return _ with Frac _ b => b end |}. -Next Obligation. - intros c n i ?; simpl. destruct (c 0) eqn:?; simplify_eq/=. - by feed inversion (chain_cauchy c n i). -Qed. -Instance frac_compl : Compl (frac A) := λ c, - Frac (frac_perm (c 0)) (compl (frac_chain c)). -Definition frac_cofe_mixin : CofeMixin (frac A). -Proof. - split. - - intros mx my; split. - + by destruct 1; subst; constructor; try apply equiv_dist. - + intros Hxy; feed inversion (Hxy 0); subst; constructor; try done. - apply equiv_dist=> n; by feed inversion (Hxy n). - - intros n; split. - + by intros [q a]; constructor. - + by destruct 1; constructor. - + destruct 1; inversion_clear 1; constructor; etrans; eauto. - - by inversion_clear 1; constructor; done || apply dist_S. - - intros n c; constructor; simpl. - + destruct (chain_cauchy c 0 n); auto with lia. - + apply (conv_compl n (frac_chain c)). -Qed. -Canonical Structure fracC : cofeT := CofeT (frac A) frac_cofe_mixin. -Global Instance frac_discrete : Discrete A → Discrete fracC. -Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. -Global Instance frac_leibniz : LeibnizEquiv A → LeibnizEquiv (frac A). -Proof. intros ? [??] [??] [??]; f_equal; done || by apply leibniz_equiv. Qed. - -Global Instance Frac_timeless q (a : A) : Timeless a → Timeless (Frac q a). -Proof. by inversion_clear 2; constructor; done || apply (timeless _). Qed. -End cofe. - -Arguments fracC : clear implicits. - -(* Functor on COFEs *) -Definition frac_map {A B} (f : A → B) (x : frac A) : frac B := - match x with Frac q a => Frac q (f a) end. -Instance: Params (@frac_map) 2. - -Lemma frac_map_id {A} (x : frac A) : frac_map id x = x. -Proof. by destruct x. Qed. -Lemma frac_map_compose {A B C} (f : A → B) (g : B → C) (x : frac A) : - frac_map (g ∘ f) x = frac_map g (frac_map f x). -Proof. by destruct x. Qed. -Lemma frac_map_ext {A B : cofeT} (f g : A → B) x : - (∀ x, f x ≡ g x) → frac_map f x ≡ frac_map g x. -Proof. destruct x; constructor; simpl; auto. Qed. -Instance frac_map_cmra_ne {A B : cofeT} n : - Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@frac_map A B). -Proof. intros f f' Hf [??] [??] [??]; constructor; by try apply Hf. Qed. -Definition fracC_map {A B} (f : A -n> B) : fracC A -n> fracC B := - CofeMor (frac_map f). -Instance fracC_map_ne A B n : Proper (dist n ==> dist n) (@fracC_map A B). -Proof. intros f f' Hf []; constructor; by try apply Hf. Qed. - -Section cmra. -Context {A : cmraT}. -Implicit Types a b : A. -Implicit Types x y : frac A. - -Instance frac_valid : Valid (frac A) := λ x, - (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x. -Global Arguments frac_valid !_/. -Instance frac_validN : ValidN (frac A) := λ n x, - (frac_perm x ≤ 1)%Qc ∧ ✓{n} frac_car x. -Global Arguments frac_validN _ !_/. -Instance frac_pcore : PCore (frac A) := λ _, None. -Instance frac_op : Op (frac A) := λ x y, - Frac (frac_perm x + frac_perm y) (frac_car x ⋅ frac_car y). -Global Arguments frac_op !_ !_ /. - -Lemma Frac_op q1 q2 a b : Frac q1 a ⋅ Frac q2 b = Frac (q1 + q2) (a ⋅ b). -Proof. done. Qed. - -Definition frac_cmra_mixin : CMRAMixin (frac A). +Definition frac_ra_mixin : RAMixin frac. Proof. - split; try discriminate. - - intros n [??] [??] [??] [??]; constructor; by cofe_subst. - - intros ? [??] [??] [??] [??]; split; by cofe_subst. - - intros [??]; rewrite /= ?cmra_valid_validN; naive_solver eauto using O. - - intros n [q a]; destruct 1; split; auto using cmra_validN_S. - - intros [q1 a1] [q2 a2] [q3 a3]; constructor; by rewrite /= ?assoc. - - intros [q1 a1] [q2 a2]; constructor; by rewrite /= 1?comm ?[(q1+_)%Qp]comm. - - intros n [q1 a1] [q2 a2]; destruct 1; split; eauto using cmra_validN_op_l. - trans (q1 + q2)%Qp; simpl; last done. - rewrite -{1}(Qcplus_0_r q1) -Qcplus_le_mono_l; auto using Qclt_le_weak. - - intros n [q a] y1 y2 Hx Hx'. - destruct Hx, y1 as [q1 b1], y2 as [q2 b2]. - apply (inj2 Frac) in Hx'; destruct Hx' as [-> ?]. - destruct (cmra_extend n a b1 b2) as ([z1 z2]&?&?&?); auto. - exists (Frac q1 z1,Frac q2 z2); by repeat constructor. + split; try apply _; try done. + unfold valid, op, frac_op, frac_valid. intros. trans (x+y)%Qp. 2:done. + rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak. Qed. -Canonical Structure fracR := CMRAT (frac A) frac_cofe_mixin frac_cmra_mixin. +Canonical Structure fracR := discreteR frac frac_ra_mixin. -Global Instance frac_cmra_discrete : CMRADiscrete A → CMRADiscrete fracR. -Proof. - split; first apply _. - intros [q a]; destruct 1; split; auto using cmra_discrete_valid. -Qed. +End frac. (** Internalized properties *) -Lemma frac_equivI {M} (x y : frac A) : - x ≡ y ⊣⊢ (frac_perm x = frac_perm y ∧ frac_car x ≡ frac_car y : uPred M). +Lemma frac_equivI {M} (x y : frac) : + x ≡ y ⊣⊢ (x = y : uPred M). Proof. by uPred.unseal. Qed. -Lemma frac_validI {M} (x : frac A) : - ✓ x ⊣⊢ (■ (frac_perm x ≤ 1)%Qc ∧ ✓ frac_car x : uPred M). +Lemma frac_validI {M} (x : frac) : + ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M). Proof. by uPred.unseal. Qed. (** Exclusive *) -Global Instance frac_full_exclusive a : Exclusive (Frac 1 a). +Global Instance frac_full_exclusive : Exclusive 1%Qp. Proof. - move => [[??]?][/Qcle_not_lt[]]; simpl in *. + move => ? /Qcle_not_lt[]; simpl in *. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l. Qed. - -(** ** Local updates *) -Global Instance frac_local_update `{!LocalUpdate Lv L} : - LocalUpdate (λ x, Lv (frac_car x)) (frac_map L). -Proof. - split; first apply _. intros n [p a] [q b]; simpl. - intros ? [??]; constructor; [done|by apply (local_updateN L)]. -Qed. - -(** Updates *) -Lemma frac_update (a1 a2 : A) p : a1 ~~> a2 → Frac p a1 ~~> Frac p a2. -Proof. - intros Ha n mz [??]; split; first by destruct mz. - pose proof (Ha n (frac_car <\$> mz)); destruct mz; naive_solver. -Qed. -End cmra. - -Arguments fracR : clear implicits. - -(* Functor *) -Instance frac_map_cmra_monotone {A B : cmraT} (f : A → B) : - CMRAMonotone f → CMRAMonotone (frac_map f). -Proof. - split; try apply _. - - intros n [p a]; destruct 1; split; simpl in *; auto using validN_preserving. - - intros [q1 a1] [q2 a2] [[q3 a3] [??]]; setoid_subst. - destruct (included_preserving f a1 (a1 ⋅ a3)) as [b ?]. - { by apply cmra_included_l. } - by exists (Frac q3 b); constructor. -Qed. - -Program Definition fracRF (F : rFunctor) : rFunctor := {| - rFunctor_car A B := fracR (rFunctor_car F A B); - rFunctor_map A1 A2 B1 B2 fg := fracC_map (rFunctor_map F fg) -|}. -Next Obligation. - by intros F A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_ne. -Qed. -Next Obligation. - intros F A B x. rewrite /= -{2}(frac_map_id x). - apply frac_map_ext=>y; apply rFunctor_id. -Qed. -Next Obligation. - intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -frac_map_compose. - apply frac_map_ext=>y; apply rFunctor_compose. -Qed. - -Instance fracRF_contractive F : - rFunctorContractive F → rFunctorContractive (fracRF F). -Proof. - by intros ? A1 A2 B1 B2 n f g Hfg; apply fracC_map_ne, rFunctor_contractive. -Qed. diff --git a/heap_lang/heap.v b/heap_lang/heap.v index e491bb4e..c164dafc 100644 --- a/heap_lang/heap.v +++ b/heap_lang/heap.v @@ -8,7 +8,7 @@ Import uPred. a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary predicates over finmaps instead of just ownP. *) -Definition heapUR : ucmraT := gmapUR loc (fracR (dec_agreeR val)). +Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)). (** The CMRA we need. *) Class heapG Σ := HeapG { @@ -18,14 +18,14 @@ Class heapG Σ := HeapG { (** The Functor we need. *) Definition heapGF : gFunctor := authGF heapUR. -Definition to_heap : state → heapUR := fmap (λ v, Frac 1 (DecAgree v)). -Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ frac_car). +Definition to_heap : state → heapUR := fmap (λ v, (1%Qp, DecAgree v)). +Definition of_heap : heapUR → state := omap (maybe DecAgree ∘ snd). Section definitions. Context `{i : heapG Σ}. Definition heap_mapsto (l : loc) (q : Qp) (v: val) : iPropG heap_lang Σ := - auth_own heap_name {[ l := Frac q (DecAgree v) ]}. + auth_own heap_name {[ l := (q, DecAgree v) ]}. Definition heap_inv (h : heapUR) : iPropG heap_lang Σ := ownP (of_heap h). Definition heap_ctx (N : namespace) : iPropG heap_lang Σ := @@ -60,11 +60,11 @@ Section heap. Lemma to_heap_valid σ : ✓ to_heap σ. Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed. Lemma of_heap_insert l v h : - of_heap (<[l:=Frac 1 (DecAgree v)]> h) = <[l:=v]> (of_heap h). - Proof. by rewrite /of_heap -(omap_insert _ _ _ (Frac 1 (DecAgree v))). Qed. + of_heap (<[l:=(1%Qp, DecAgree v)]> h) = <[l:=v]> (of_heap h). + Proof. by rewrite /of_heap -(omap_insert _ _ _ (1%Qp, DecAgree v)). Qed. Lemma of_heap_singleton_op l q v h : - ✓ ({[l := Frac q (DecAgree v)]} ⋅ h) → - of_heap ({[l := Frac q (DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h). + ✓ ({[l := (q, DecAgree v)]} ⋅ h) → + of_heap ({[l := (q, DecAgree v)]} ⋅ h) = <[l:=v]> (of_heap h). Proof. intros Hv. apply map_eq=> l'; destruct (decide (l' = l)) as [->|]. - move: (Hv l). rewrite /of_heap lookup_insert @@ -75,7 +75,7 @@ Section heap. by rewrite (lookup_op _ h) lookup_singleton_ne // left_id_L. Qed. Lemma to_heap_insert l v σ : - to_heap (<[l:=v]> σ) = <[l:=Frac 1 (DecAgree v)]> (to_heap σ). + to_heap (<[l:=v]> σ) = <[l:=(1%Qp, DecAgree v)]> (to_heap σ). Proof. by rewrite /to_heap -fmap_insert. Qed. Lemma of_heap_None h l : ✓ h → of_heap h !! l = None → h !! l = None. @@ -84,8 +84,8 @@ Section heap. by case: (h !! l)=> [[q [v|]]|] //=; destruct 1; auto. Qed. Lemma heap_store_valid l h v1 v2 : - ✓ ({[l := Frac 1 (DecAgree v1)]} ⋅ h) → - ✓ ({[l := Frac 1 (DecAgree v2)]} ⋅ h). + ✓ ({[l := (1%Qp, DecAgree v1)]} ⋅ h) → + ✓ ({[l := (1%Qp, DecAgree v2)]} ⋅ h). Proof. intros Hv l'; move: (Hv l'). destruct (decide (l' = l)) as [->|]. - rewrite !lookup_op !lookup_singleton. @@ -120,17 +120,17 @@ Section heap. Proof. rewrite /heap_mapsto. apply _. Qed. Lemma heap_mapsto_op_eq l q1 q2 v : (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ l ↦{q1+q2} v. - Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed. + Proof. by rewrite -auth_own_op op_singleton pair_op dec_agree_idemp. Qed. Lemma heap_mapsto_op l q1 q2 v1 v2 : (l ↦{q1} v1 ★ l ↦{q2} v2) ⊣⊢ (v1 = v2 ∧ l ↦{q1+q2} v1). Proof. destruct (decide (v1 = v2)) as [->|]. { by rewrite heap_mapsto_op_eq const_equiv // left_id. } - rewrite -auth_own_op op_singleton Frac_op dec_agree_ne //. + rewrite -auth_own_op op_singleton pair_op dec_agree_ne //. apply (anti_symm (⊢)); last by apply const_elim_l. rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton. - rewrite option_validI frac_validI discrete_valid. by apply const_elim_r. + rewrite option_validI prod_validI frac_validI discrete_valid. by apply const_elim_r. Qed. Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v). @@ -147,7 +147,7 @@ Section heap. iFrame "Hinv Hheap". iIntros {h}. rewrite [∅ ⋅ h]left_id. iIntros "[% Hheap]". rewrite /heap_inv. iApply wp_alloc_pst; first done. iFrame "Hheap". iNext. - iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _. + iIntros {l} "[% Hheap]". iExists (op {[ l := (1%Qp, DecAgree v) ]}), _, _. rewrite [{[ _ := _ ]} ⋅ ∅]right_id. rewrite -of_heap_insert -(insert_singleton_op h); last by apply of_heap_None. iFrame "Hheap". iSplit. @@ -162,7 +162,7 @@ Section heap. Proof. iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto. iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _ - heap_name {[ l := Frac q (DecAgree v) ]}); simpl; eauto. + heap_name {[ l := (q, DecAgree v) ]}); simpl; eauto. iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert. rewrite of_heap_singleton_op //. iFrame "Hl". iNext. @@ -175,13 +175,13 @@ Section heap. ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}. Proof. iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto. - iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l) _ - N _ heap_name {[ l := Frac 1 (DecAgree v') ]}); simpl; eauto. + iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, (1%Qp, DecAgree v)) l) _ + N _ heap_name {[ l := (1%Qp, DecAgree v') ]}); simpl; eauto. iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //. rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto. iFrame "Hl". iNext. iIntros "\$". iFrame "HΦ". - iPureIntro. eauto with typeclass_instances. + iPureIntro. eauto 10 with typeclass_instances. Qed. Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ : @@ -191,7 +191,7 @@ Section heap. Proof. iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto. iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _ - heap_name {[ l := Frac q (DecAgree v') ]}); simpl; eauto 10. + heap_name {[ l := (q, DecAgree v') ]}); simpl; eauto 10. iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //. rewrite of_heap_singleton_op //. iFrame "Hl". iNext. @@ -204,12 +204,12 @@ Section heap. ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}. Proof. iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto. - iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l) - _ N _ heap_name {[ l := Frac 1 (DecAgree v1) ]}); simpl; eauto 10. + iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, (1%Qp, DecAgree v2)) l) + _ N _ heap_name {[ l := (1%Qp, DecAgree v1) ]}); simpl; eauto 10. iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv. iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //. rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto. iFrame "Hl". iNext. iIntros "\$". iFrame "HΦ". - iPureIntro. eauto with typeclass_instances. + iPureIntro. eauto 10 with typeclass_instances. Qed. End heap. diff --git a/prelude/base.v b/prelude/base.v index bfcb09ae..6872ec7f 100644 --- a/prelude/base.v +++ b/prelude/base.v @@ -466,6 +466,11 @@ Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _. Typeclasses Opaque prod_equiv. +Instance prod_leibniz `{LeibnizEquiv A, !Equivalence ((≡) : relation A), + LeibnizEquiv B, !Equivalence ((≡) : relation B)} + : LeibnizEquiv (A * B). +Proof. intros [] [] []; fold_leibniz; simpl; congruence. Qed. + (** ** Sums *) Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' := match xy with inl x => inl (f x) | inr y => inr (g y) end. -- 2.26.2