functions.v 7.31 KB
 Jacques-Henri Jourdan committed Sep 13, 2019 1 ``````From stdpp Require Import finite. `````` Robbert Krebbers committed Nov 27, 2017 2 3 4 5 ``````From iris.algebra Require Export cmra. From iris.algebra Require Import updates. Set Default Proof Using "Type". `````` Robbert Krebbers committed Jun 16, 2019 6 7 ``````Definition discrete_fun_insert `{EqDecision A} {B : A → ofeT} (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x', `````` Robbert Krebbers committed Nov 27, 2017 8 `````` match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end. `````` Robbert Krebbers committed Jun 16, 2019 9 ``````Instance: Params (@discrete_fun_insert) 5 := {}. `````` Robbert Krebbers committed Nov 27, 2017 10 `````` `````` Robbert Krebbers committed Jun 16, 2019 11 12 13 ``````Definition discrete_fun_singleton `{EqDecision A} {B : A → ucmraT} (x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε. Instance: Params (@discrete_fun_singleton) 5 := {}. `````` Robbert Krebbers committed Nov 27, 2017 14 15 16 17 `````` Section ofe. Context `{Heqdec : EqDecision A} {B : A → ofeT}. Implicit Types x : A. `````` Robbert Krebbers committed Jun 16, 2019 18 `````` Implicit Types f g : discrete_fun B. `````` Robbert Krebbers committed Nov 27, 2017 19 `````` `````` Robbert Krebbers committed Jun 16, 2019 20 21 `````` Global Instance discrete_funO_ofe_discrete : (∀ i, OfeDiscrete (B i)) → OfeDiscrete (discrete_funO B). `````` Jacques-Henri Jourdan committed Apr 09, 2018 22 23 `````` Proof. intros HB f f' Heq i. apply HB, Heq. Qed. `````` Robbert Krebbers committed Jun 16, 2019 24 25 26 `````` (** Properties of discrete_fun_insert. *) Global Instance discrete_fun_insert_ne x : NonExpansive2 (discrete_fun_insert (B:=B) x). `````` Robbert Krebbers committed Nov 27, 2017 27 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2019 28 `````` intros n y1 y2 ? f1 f2 ? x'; rewrite /discrete_fun_insert. `````` Robbert Krebbers committed Nov 27, 2017 29 30 `````` by destruct (decide _) as [[]|]. Qed. `````` Robbert Krebbers committed Jun 16, 2019 31 32 `````` Global Instance discrete_fun_insert_proper x : Proper ((≡) ==> (≡) ==> (≡)) (discrete_fun_insert (B:=B) x) := ne_proper_2 _. `````` Robbert Krebbers committed Nov 27, 2017 33 `````` `````` Robbert Krebbers committed Jun 16, 2019 34 `````` Lemma discrete_fun_lookup_insert f x y : (discrete_fun_insert x y f) x = y. `````` Robbert Krebbers committed Nov 27, 2017 35 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2019 36 `````` rewrite /discrete_fun_insert; destruct (decide _) as [Hx|]; last done. `````` Robbert Krebbers committed Nov 27, 2017 37 38 `````` by rewrite (proof_irrel Hx eq_refl). Qed. `````` Robbert Krebbers committed Jun 16, 2019 39 40 41 `````` Lemma discrete_fun_lookup_insert_ne f x x' y : x ≠ x' → (discrete_fun_insert x y f) x' = f x'. Proof. by rewrite /discrete_fun_insert; destruct (decide _). Qed. `````` Robbert Krebbers committed Nov 27, 2017 42 `````` `````` Robbert Krebbers committed Jun 16, 2019 43 44 `````` Global Instance discrete_fun_insert_discrete f x y : Discrete f → Discrete y → Discrete (discrete_fun_insert x y f). `````` Robbert Krebbers committed Nov 27, 2017 45 46 `````` Proof. intros ?? g Heq x'; destruct (decide (x = x')) as [->|]. `````` Robbert Krebbers committed Jun 16, 2019 47 48 49 50 `````` - rewrite discrete_fun_lookup_insert. apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert. - rewrite discrete_fun_lookup_insert_ne //. apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert_ne. `````` Robbert Krebbers committed Nov 27, 2017 51 52 53 54 `````` Qed. End ofe. Section cmra. `````` 55 `````` Context `{EqDecision A} {B : A → ucmraT}. `````` Robbert Krebbers committed Nov 27, 2017 56 `````` Implicit Types x : A. `````` Robbert Krebbers committed Jun 16, 2019 57 `````` Implicit Types f g : discrete_fun B. `````` Robbert Krebbers committed Nov 27, 2017 58 `````` `````` Robbert Krebbers committed Jun 16, 2019 59 60 `````` Global Instance discrete_funR_cmra_discrete: (∀ i, CmraDiscrete (B i)) → CmraDiscrete (discrete_funR B). `````` Jacques-Henri Jourdan committed Apr 09, 2018 61 62 `````` Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed. `````` Robbert Krebbers committed Jun 16, 2019 63 64 65 66 67 `````` Global Instance discrete_fun_singleton_ne x : NonExpansive (discrete_fun_singleton x : B x → _). Proof. intros n y1 y2 ?; apply discrete_fun_insert_ne. done. by apply equiv_dist. Qed. Global Instance discrete_fun_singleton_proper x : Proper ((≡) ==> (≡)) (discrete_fun_singleton x) := ne_proper _. `````` Robbert Krebbers committed Nov 27, 2017 68 `````` `````` Robbert Krebbers committed Jun 16, 2019 69 70 71 72 73 `````` Lemma discrete_fun_lookup_singleton x (y : B x) : (discrete_fun_singleton x y) x = y. Proof. by rewrite /discrete_fun_singleton discrete_fun_lookup_insert. Qed. Lemma discrete_fun_lookup_singleton_ne x x' (y : B x) : x ≠ x' → (discrete_fun_singleton x y) x' = ε. Proof. intros; by rewrite /discrete_fun_singleton discrete_fun_lookup_insert_ne. Qed. `````` Robbert Krebbers committed Nov 27, 2017 74 `````` `````` Robbert Krebbers committed Jun 16, 2019 75 76 `````` Global Instance discrete_fun_singleton_discrete x (y : B x) : (∀ i, Discrete (ε : B i)) → Discrete y → Discrete (discrete_fun_singleton x y). `````` Robbert Krebbers committed Nov 27, 2017 77 78 `````` Proof. apply _. Qed. `````` Robbert Krebbers committed Jun 16, 2019 79 `````` Lemma discrete_fun_singleton_validN n x (y : B x) : ✓{n} discrete_fun_singleton x y ↔ ✓{n} y. `````` Robbert Krebbers committed Nov 27, 2017 80 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2019 81 `````` split; [by move=>/(_ x); rewrite discrete_fun_lookup_singleton|]. `````` Robbert Krebbers committed Nov 27, 2017 82 `````` move=>Hx x'; destruct (decide (x = x')) as [->|]; `````` Robbert Krebbers committed Jun 16, 2019 83 `````` rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //. `````` Robbert Krebbers committed Nov 27, 2017 84 85 86 `````` by apply ucmra_unit_validN. Qed. `````` Robbert Krebbers committed Jun 16, 2019 87 88 `````` Lemma discrete_fun_core_singleton x (y : B x) : core (discrete_fun_singleton x y) ≡ discrete_fun_singleton x (core y). `````` Robbert Krebbers committed Nov 27, 2017 89 90 `````` Proof. move=>x'; destruct (decide (x = x')) as [->|]; `````` Robbert Krebbers committed Jun 16, 2019 91 92 `````` by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne // (core_id_core ∅). `````` Robbert Krebbers committed Nov 27, 2017 93 94 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2019 95 96 97 `````` Global Instance discrete_fun_singleton_core_id x (y : B x) : CoreId y → CoreId (discrete_fun_singleton x y). Proof. by rewrite !core_id_total discrete_fun_core_singleton=> ->. Qed. `````` Robbert Krebbers committed Nov 27, 2017 98 `````` `````` Robbert Krebbers committed Jun 16, 2019 99 100 `````` Lemma discrete_fun_op_singleton (x : A) (y1 y2 : B x) : discrete_fun_singleton x y1 ⋅ discrete_fun_singleton x y2 ≡ discrete_fun_singleton x (y1 ⋅ y2). `````` Robbert Krebbers committed Nov 27, 2017 101 102 `````` Proof. intros x'; destruct (decide (x' = x)) as [->|]. `````` Robbert Krebbers committed Jun 16, 2019 103 104 `````` - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton. - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton_ne // left_id. `````` Robbert Krebbers committed Nov 27, 2017 105 106 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2019 107 108 109 `````` Lemma discrete_fun_insert_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) g y1 : y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_insert x y2 g)) → discrete_fun_insert x y1 g ~~>: Q. `````` Robbert Krebbers committed Nov 27, 2017 110 111 112 `````` Proof. intros Hy1 HP; apply cmra_total_updateP. intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?). `````` Robbert Krebbers committed Jun 16, 2019 113 114 `````` { move: (Hg x). by rewrite discrete_fun_lookup_op discrete_fun_lookup_insert. } exists (discrete_fun_insert x y2 g); split; [auto|]. `````` Robbert Krebbers committed Nov 27, 2017 115 `````` intros x'; destruct (decide (x' = x)) as [->|]; `````` Robbert Krebbers committed Jun 16, 2019 116 117 `````` rewrite discrete_fun_lookup_op ?discrete_fun_lookup_insert //; []. move: (Hg x'). by rewrite discrete_fun_lookup_op !discrete_fun_lookup_insert_ne. `````` Robbert Krebbers committed Nov 27, 2017 118 119 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2019 120 `````` Lemma discrete_fun_insert_updateP' x (P : B x → Prop) g y1 : `````` Robbert Krebbers committed Nov 27, 2017 121 `````` y1 ~~>: P → `````` Robbert Krebbers committed Jun 16, 2019 122 123 124 125 `````` discrete_fun_insert x y1 g ~~>: λ g', ∃ y2, g' = discrete_fun_insert x y2 g ∧ P y2. Proof. eauto using discrete_fun_insert_updateP. Qed. Lemma discrete_fun_insert_update g x y1 y2 : y1 ~~> y2 → discrete_fun_insert x y1 g ~~> discrete_fun_insert x y2 g. `````` Robbert Krebbers committed Nov 27, 2017 126 `````` Proof. `````` Robbert Krebbers committed Jun 16, 2019 127 `````` rewrite !cmra_update_updateP; eauto using discrete_fun_insert_updateP with subst. `````` Robbert Krebbers committed Nov 27, 2017 128 129 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2019 130 131 132 133 134 `````` Lemma discrete_fun_singleton_updateP x (P : B x → Prop) (Q : discrete_fun B → Prop) y1 : y1 ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) → discrete_fun_singleton x y1 ~~>: Q. Proof. rewrite /discrete_fun_singleton; eauto using discrete_fun_insert_updateP. Qed. Lemma discrete_fun_singleton_updateP' x (P : B x → Prop) y1 : `````` Robbert Krebbers committed Nov 27, 2017 135 `````` y1 ~~>: P → `````` Robbert Krebbers committed Jun 16, 2019 136 137 138 139 140 141 142 143 `````` discrete_fun_singleton x y1 ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2. Proof. eauto using discrete_fun_singleton_updateP. Qed. Lemma discrete_fun_singleton_update x (y1 y2 : B x) : y1 ~~> y2 → discrete_fun_singleton x y1 ~~> discrete_fun_singleton x y2. Proof. eauto using discrete_fun_insert_update. Qed. Lemma discrete_fun_singleton_updateP_empty x (P : B x → Prop) (Q : discrete_fun B → Prop) : ε ~~>: P → (∀ y2, P y2 → Q (discrete_fun_singleton x y2)) → ε ~~>: Q. `````` Robbert Krebbers committed Nov 27, 2017 144 145 146 `````` Proof. intros Hx HQ; apply cmra_total_updateP. intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg. `````` Robbert Krebbers committed Jun 16, 2019 147 `````` exists (discrete_fun_singleton x y2); split; [by apply HQ|]. `````` Robbert Krebbers committed Nov 27, 2017 148 `````` intros x'; destruct (decide (x' = x)) as [->|]. `````` Robbert Krebbers committed Jun 16, 2019 149 150 `````` - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton. - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //. apply Hg. `````` Robbert Krebbers committed Nov 27, 2017 151 `````` Qed. `````` Robbert Krebbers committed Jun 16, 2019 152 153 154 155 156 `````` Lemma discrete_fun_singleton_updateP_empty' x (P : B x → Prop) : ε ~~>: P → ε ~~>: λ g, ∃ y2, g = discrete_fun_singleton x y2 ∧ P y2. Proof. eauto using discrete_fun_singleton_updateP_empty. Qed. Lemma discrete_fun_singleton_update_empty x (y : B x) : ε ~~> y → ε ~~> discrete_fun_singleton x y. `````` Robbert Krebbers committed Nov 27, 2017 157 158 `````` Proof. rewrite !cmra_update_updateP; `````` Robbert Krebbers committed Jun 16, 2019 159 `````` eauto using discrete_fun_singleton_updateP_empty with subst. `````` Robbert Krebbers committed Nov 27, 2017 160 161 `````` Qed. End cmra.``````