Commit 758d8d65 by Jacques-Henri Jourdan

### Simplify frac : use a pair of a rational and a carrier

parent 8f839433
 ... ... @@ -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. ... ...
 ... ... @@ -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.
 ... ... @@ -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.
 ... ... @@ -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. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!