### Turn equality and metric on res into an inductive.

```This way, they are non-delta unfoldable constants, which showed a positive
impact on the performance of setoid rewriting. We may want to do this for
other cmra/cofe structures too.```
parent 6b1c085d
 ... ... @@ -25,8 +25,8 @@ Qed. (* Resources *) Record res (Σ : iParam) (A : cofeT) := Res { wld : gmap positive (agree (later A)); pst : excl (leibnizC (istate Σ)); wld : mapRA positive (agreeRA (laterC A)); pst : exclRA (leibnizC (istate Σ)); gst : icmra Σ (laterC A); }. Add Printing Constructor res. ... ... @@ -43,46 +43,50 @@ Section res. Context (Σ : iParam) (A : cofeT). Implicit Types r : res Σ A. Instance res_equiv : Equiv (res Σ A) := λ r1 r2, wld r1 ≡ wld r2 ∧ pst r1 ≡ pst r2 ∧ gst r1 ≡ gst r2. Instance res_dist : Dist (res Σ A) := λ n r1 r2, wld r1 ={n}= wld r2 ∧ pst r1 ={n}= pst r2 ∧ gst r1 ={n}= gst r2. Inductive res_equiv' (r1 r2 : res Σ A) := Res_equiv : wld r1 ≡ wld r2 → pst r1 ≡ pst r2 → gst r1 ≡ gst r2 → res_equiv' r1 r2. Instance res_equiv : Equiv (res Σ A) := res_equiv'. Inductive res_dist' (n : nat) (r1 r2 : res Σ A) := Res_dist : wld r1 ={n}= wld r2 → pst r1 ={n}= pst r2 → gst r1 ={n}= gst r2 → res_dist' n r1 r2. Instance res_dist : Dist (res Σ A) := res_dist'. Global Instance Res_ne n : Proper (dist n ==> dist n ==> dist n ==> dist n) (@Res Σ A). Proof. done. Qed. Global Instance Res_proper : Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) (@Res Σ A). Proof. done. Qed. Global Instance wld_ne n : Proper (dist n ==> dist n) (@wld Σ A). Proof. by intros r1 r2 (?&?&?). Qed. Proof. by destruct 1. Qed. Global Instance wld_proper : Proper ((≡) ==> (≡)) (@wld Σ A). Proof. by intros r1 r2 (?&?&?). Qed. Proof. by destruct 1. Qed. Global Instance pst_ne n : Proper (dist n ==> dist n) (@pst Σ A). Proof. by intros r1 r2 (?&?&?). Qed. Proof. by destruct 1. Qed. Global Instance pst_ne' n : Proper (dist (S n) ==> (≡)) (@pst Σ A). Proof. intros σ σ' (_&?&_); apply (timeless _), dist_le with (S n); auto with lia. intros σ σ' [???]; apply (timeless _), dist_le with (S n); auto with lia. Qed. Global Instance pst_proper : Proper ((≡) ==> (≡)) (@pst Σ A). Proof. by intros r1 r2 (?&?&?). Qed. Proof. by destruct 1. Qed. Global Instance gst_ne n : Proper (dist n ==> dist n) (@gst Σ A). Proof. by intros r1 r2 (?&?&?). Qed. Proof. by destruct 1. Qed. Global Instance gst_proper : Proper ((≡) ==> (≡)) (@gst Σ A). Proof. by intros r1 r2 (?&?&?). Qed. Proof. by destruct 1. Qed. Instance res_compl : Compl (res Σ A) := λ c, Res (compl (chain_map wld c)) (compl (chain_map pst c)) (compl (chain_map gst c)). Definition res_cofe_mixin : CofeMixin (res Σ A). Proof. split. * intros w1 w2; unfold equiv, res_equiv, dist, res_dist. rewrite !equiv_dist; naive_solver. * intros w1 w2; split. + by destruct 1; constructor; apply equiv_dist. + by intros Hw; constructor; apply equiv_dist=>n; destruct (Hw n). * intros n; split. + done. + by intros ?? (?&?&?); split_ands'. + intros ??? (?&?&?) (?&?&?); split_ands'; etransitivity; eauto. * by intros n ?? (?&?&?); split_ands'; apply dist_S. + by destruct 1; constructor. + do 2 destruct 1; constructor; etransitivity; eauto. * by destruct 1; constructor; apply dist_S. * done. * intros c n; split_ands'. * intros c n; constructor. + apply (conv_compl (chain_map wld c) n). + apply (conv_compl (chain_map pst c) n). + apply (conv_compl (chain_map gst c) n). ... ... @@ -90,15 +94,14 @@ Qed. Canonical Structure resC : cofeT := CofeT res_cofe_mixin. Global Instance res_timeless r : Timeless (wld r) → Timeless (gst r) → Timeless r. Proof. by intros ??? (?&?&?); split_ands'; try apply (timeless _). Qed. Proof. by destruct 3; constructor; try apply (timeless _). Qed. Instance res_op : Op (res Σ A) := λ r1 r2, Res (wld r1 ⋅ wld r2) (pst r1 ⋅ pst r2) (gst r1 ⋅ gst r2). Global Instance res_empty : Empty (res Σ A) := Res ∅ ∅ ∅. Instance res_unit : Unit (res Σ A) := λ r, Res (unit (wld r)) (unit (pst r)) (unit (gst r)). Instance res_valid : Valid (res Σ A) := λ r, ✓ (wld r) ∧ ✓ (pst r) ∧ ✓ (gst r). Instance res_valid : Valid (res Σ A) := λ r, ✓ (wld r) ∧ ✓ (pst r) ∧ ✓ (gst r). Instance res_validN : ValidN (res Σ A) := λ n r, ✓{n} (wld r) ∧ ✓{n} (pst r) ∧ ✓{n} (gst r). Instance res_minus : Minus (res Σ A) := λ r1 r2, ... ... @@ -120,25 +123,25 @@ Qed. Definition res_cmra_mixin : CMRAMixin (res Σ A). Proof. split. * by intros n x [???] ? (?&?&?); split_ands'; simpl in *; cofe_subst. * by intros n [???] ? (?&?&?); split_ands'; simpl in *; cofe_subst. * by intros n [???] ? (?&?&?) (?&?&?); split_ands'; simpl in *; cofe_subst. * by intros n [???] ? (?&?&?) [???] ? (?&?&?); split_ands'; simpl in *; cofe_subst. * by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst. * by intros n [???] ? [???]; constructor; simpl in *; cofe_subst. * by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst. * by intros n [???] ? [???] [???] ? [???]; constructor; simpl in *; cofe_subst. * done. * by intros n ? (?&?&?); split_ands'; apply cmra_valid_S. * intros r; unfold valid, res_valid, validN, res_validN. rewrite !cmra_valid_validN; naive_solver. * intros ???; split_ands'; simpl; apply (associative _). * intros ??; split_ands'; simpl; apply (commutative _). * intros ?; split_ands'; simpl; apply ra_unit_l. * intros ?; split_ands'; simpl; apply ra_unit_idempotent. * intros ???; constructor; simpl; apply (associative _). * intros ??; constructor; simpl; apply (commutative _). * intros ?; constructor; simpl; apply ra_unit_l. * intros ?; constructor; simpl; apply ra_unit_idempotent. * intros n r1 r2; rewrite !res_includedN. by intros (?&?&?); split_ands'; apply cmra_unit_preserving. * intros n r1 r2 (?&?&?); split_ands'; simpl in *; eapply cmra_valid_op_l; eauto. * intros n r1 r2; rewrite res_includedN; intros (?&?&?). by split_ands'; apply cmra_op_minus. by constructor; apply cmra_op_minus. Qed. Global Instance res_ra_empty : RAIdentity (res Σ A). Proof. ... ... @@ -147,7 +150,7 @@ Qed. Definition res_cmra_extend_mixin : CMRAExtendMixin (res Σ A). Proof. intros n r r1 r2 (?&?&?) (?&?&?); simpl in *. intros n r r1 r2 (?&?&?) [???]; simpl in *. destruct (cmra_extend_op n (wld r) (wld r1) (wld r2)) as ([w w']&?&?&?), (cmra_extend_op n (pst r) (pst r1) (pst r2)) as ([σ σ']&?&?&?), (cmra_extend_op n (gst r) (gst r1) (gst r2)) as ([m m']&?&?&?); auto. ... ... @@ -169,10 +172,10 @@ Definition res_map {Σ A B} (f : A -n> B) (r : res Σ A) : res Σ B := Instance res_map_ne Σ (A B : cofeT) (f : A -n> B) : (∀ n, Proper (dist n ==> dist n) f) → ∀ n, Proper (dist n ==> dist n) (@res_map Σ _ _ f). Proof. by intros Hf n [] ? (?&?&?); split_ands'; simpl in *; cofe_subst. Qed. Proof. by intros Hf n [] ? [???]; constructor; simpl in *; cofe_subst. Qed. Lemma res_map_id {Σ A} (r : res Σ A) : res_map cid r ≡ r. Proof. split_ands'; simpl; [|done|]. constructor; simpl; [|done|]. * rewrite -{2}(map_fmap_id (wld r)); apply map_fmap_setoid_ext=> i y ? /=. rewrite -{2}(agree_map_id y); apply agree_map_ext=> y' /=. by rewrite later_map_id. ... ... @@ -182,7 +185,7 @@ Qed. Lemma res_map_compose {Σ A B C} (f : A -n> B) (g : B -n> C) (r : res Σ A) : res_map (g ◎ f) r ≡ res_map g (res_map f r). Proof. split_ands'; simpl; [|done|]. constructor; simpl; [|done|]. * rewrite -map_fmap_compose; apply map_fmap_setoid_ext=> i y _ /=. rewrite -agree_map_compose; apply agree_map_ext=> y' /=. by rewrite later_map_compose. ... ... @@ -201,7 +204,7 @@ Proof. Qed. Instance resRA_map_contractive {Σ A B} : Contractive (@resRA_map Σ A B). Proof. intros n f g ? r; split_ands'; simpl; [|done|]. intros n f g ? r; constructor; simpl; [|done|]. * by apply (mapRA_map_ne _ (agreeRA_map (laterC_map f)) (agreeRA_map (laterC_map g))), agreeRA_map_ne, laterC_map_contractive. * by apply icmra_map_ne, laterC_map_contractive. ... ... @@ -226,7 +229,7 @@ End iProp. (* Solution *) Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ. Notation res' Σ := (resRA Σ (iPreProp Σ)). Notation res' Σ := (res Σ (iPreProp Σ)). Notation icmra' Σ := (icmra Σ (laterC (iPreProp Σ))). Definition iProp (Σ : iParam) : cofeT := uPredC (resRA Σ (iPreProp Σ)). Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!