environments.v 7.48 KB
 Robbert Krebbers committed Feb 22, 2017 1 ``````From fast_string Require Export fast_string_lib. `````` Robbert Krebbers committed Apr 11, 2016 2 ``````From iris.algebra Require Export base. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Apr 11, 2016 4 5 6 7 8 9 `````` Inductive env (A : Type) : Type := | Enil : env A | Esnoc : env A → string → A → env A. Arguments Enil {_}. Arguments Esnoc {_} _ _%string _. `````` Robbert Krebbers committed May 07, 2016 10 11 ``````Instance: Params (@Enil) 1. Instance: Params (@Esnoc) 1. `````` Robbert Krebbers committed Apr 11, 2016 12 13 14 15 `````` Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A := match Γ with | Enil => None `````` Robbert Krebbers committed Nov 10, 2016 16 `````` | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ `````` Robbert Krebbers committed Apr 11, 2016 17 `````` end. `````` Robbert Krebbers committed Sep 27, 2016 18 19 20 21 22 23 24 25 26 27 `````` Module env_notations. Notation "x ← y ; z" := (match y with Some x => z | None => None end). Notation "' ( x1 , x2 ) ← y ; z" := (match y with Some (x1,x2) => z | None => None end). Notation "' ( x1 , x2 , x3 ) ← y ; z" := (match y with Some (x1,x2,x3) => z | None => None end). Notation "Γ !! j" := (env_lookup j Γ). End env_notations. Import env_notations. `````` Robbert Krebbers committed Apr 11, 2016 28 29 30 31 32 33 34 35 `````` Inductive env_wf {A} : env A → Prop := | Enil_wf : env_wf Enil | Esnoc_wf Γ i x : Γ !! i = None → env_wf Γ → env_wf (Esnoc Γ i x). Fixpoint env_to_list {A} (E : env A) : list A := match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end. Coercion env_to_list : env >-> list. `````` Robbert Krebbers committed May 07, 2016 36 ``````Instance: Params (@env_to_list) 1. `````` Robbert Krebbers committed Apr 13, 2016 37 `````` `````` Robbert Krebbers committed Jun 01, 2016 38 39 ``````Fixpoint env_dom {A} (Γ : env A) : list string := match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end. `````` Robbert Krebbers committed Apr 13, 2016 40 `````` `````` Robbert Krebbers committed Apr 11, 2016 41 42 43 44 45 46 47 ``````Fixpoint env_app {A} (Γapp : env A) (Γ : env A) : option (env A) := match Γapp with | Enil => Some Γ | Esnoc Γapp i x => Γ' ← env_app Γapp Γ; match Γ' !! i with None => Some (Esnoc Γ' i x) | Some _ => None end end. `````` Robbert Krebbers committed Sep 20, 2016 48 `````` `````` Robbert Krebbers committed Apr 11, 2016 49 50 51 52 ``````Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) := match Γ with | Enil => None | Esnoc Γ j x => `````` Robbert Krebbers committed Nov 10, 2016 53 `````` if string_beq i j then env_app Γi Γ else `````` Robbert Krebbers committed Apr 11, 2016 54 55 56 57 58 `````` match Γi !! j with | None => Γ' ← env_replace i Γi Γ; Some (Esnoc Γ' j x) | Some _ => None end end. `````` Robbert Krebbers committed Sep 20, 2016 59 `````` `````` Robbert Krebbers committed Apr 11, 2016 60 61 62 ``````Fixpoint env_delete {A} (i : string) (Γ : env A) : env A := match Γ with | Enil => Enil `````` Robbert Krebbers committed Nov 10, 2016 63 `````` | Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x `````` Robbert Krebbers committed Apr 11, 2016 64 `````` end. `````` Robbert Krebbers committed Sep 20, 2016 65 `````` `````` Robbert Krebbers committed Apr 11, 2016 66 67 68 69 ``````Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) := match Γ with | Enil => None | Esnoc Γ j x => `````` Robbert Krebbers committed Nov 10, 2016 70 `````` if string_beq i j then Some (x,Γ) `````` Robbert Krebbers committed Apr 11, 2016 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 `````` else '(y,Γ') ← env_lookup_delete i Γ; Some (y, Esnoc Γ' j x) end. Inductive env_Forall2 {A B} (P : A → B → Prop) : env A → env B → Prop := | env_Forall2_nil : env_Forall2 P Enil Enil | env_Forall2_snoc Γ1 Γ2 i x y : env_Forall2 P Γ1 Γ2 → P x y → env_Forall2 P (Esnoc Γ1 i x) (Esnoc Γ2 i y). Section env. Context {A : Type}. Implicit Types Γ : env A. Implicit Types i : string. Implicit Types x : A. Hint Resolve Esnoc_wf Enil_wf. `````` Robbert Krebbers committed Nov 10, 2016 86 87 88 89 90 91 92 ``````Ltac simplify := repeat match goal with | _ => progress simplify_eq/= | H : context [string_beq ?s1 ?s2] |- _ => destruct (string_beq_reflect s1 s2) | |- context [string_beq ?s1 ?s2] => destruct (string_beq_reflect s1 s2) | _ => case_match end. `````` Robbert Krebbers committed Apr 11, 2016 93 94 95 96 97 98 `````` Lemma env_lookup_perm Γ i x : Γ !! i = Some x → Γ ≡ₚ x :: env_delete i Γ. Proof. induction Γ; intros; simplify; rewrite 1?Permutation_swap; f_equiv; eauto. Qed. `````` Robbert Krebbers committed Sep 20, 2016 99 100 101 102 103 104 ``````Lemma env_lookup_snoc Γ i P : env_lookup i (Esnoc Γ i P) = Some P. Proof. induction Γ; simplify; auto. Qed. Lemma env_lookup_snoc_ne Γ i j P : i ≠ j → env_lookup i (Esnoc Γ j P) = env_lookup i Γ. Proof. induction Γ=> ?; simplify; auto. Qed. `````` Robbert Krebbers committed Apr 11, 2016 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 ``````Lemma env_app_perm Γ Γapp Γ' : env_app Γapp Γ = Some Γ' → env_to_list Γ' ≡ₚ Γapp ++ Γ. Proof. revert Γ'; induction Γapp; intros; simplify; f_equal; auto. Qed. Lemma env_app_fresh Γ Γapp Γ' i : env_app Γapp Γ = Some Γ' → Γapp !! i = None → Γ !! i = None → Γ' !! i = None. Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed. Lemma env_app_fresh_1 Γ Γapp Γ' i x : env_app Γapp Γ = Some Γ' → Γ' !! i = None → Γ !! i = None. Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed. Lemma env_app_disjoint Γ Γapp Γ' i : env_app Γapp Γ = Some Γ' → Γapp !! i = None ∨ Γ !! i = None. Proof. revert Γ'. induction Γapp; intros; simplify; naive_solver eauto using env_app_fresh_1. Qed. Lemma env_app_wf Γ Γapp Γ' : env_app Γapp Γ = Some Γ' → env_wf Γ → env_wf Γ'. Proof. revert Γ'. induction Γapp; intros; simplify; eauto. Qed. Lemma env_replace_fresh Γ Γj Γ' i j : env_replace j Γj Γ = Some Γ' → Γj !! i = None → env_delete j Γ !! i = None → Γ' !! i = None. Proof. revert Γ'. induction Γ; intros; simplify; eauto using env_app_fresh. Qed. Lemma env_replace_wf Γ Γi Γ' i : env_replace i Γi Γ = Some Γ' → env_wf (env_delete i Γ) → env_wf Γ'. Proof. revert Γ'. induction Γ; intros ??; simplify; [|inversion_clear 1]; eauto using env_app_wf, env_replace_fresh. Qed. Lemma env_replace_lookup Γ Γi Γ' i : env_replace i Γi Γ = Some Γ' → is_Some (Γ !! i). Proof. revert Γ'. induction Γ; intros; simplify; eauto. Qed. Lemma env_replace_perm Γ Γi Γ' i : env_replace i Γi Γ = Some Γ' → Γ' ≡ₚ Γi ++ env_delete i Γ. Proof. `````` Robbert Krebbers committed Nov 10, 2016 139 140 `````` revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm. rewrite -Permutation_middle -IH //. `````` Robbert Krebbers committed Apr 11, 2016 141 142 143 144 145 146 147 148 ``````Qed. Lemma env_lookup_delete_correct Γ i : env_lookup_delete i Γ = x ← Γ !! i; Some (x,env_delete i Γ). Proof. induction Γ; intros; simplify; eauto. Qed. Lemma env_lookup_delete_Some Γ Γ' i x : env_lookup_delete i Γ = Some (x,Γ') ↔ Γ !! i = Some x ∧ Γ' = env_delete i Γ. Proof. rewrite env_lookup_delete_correct; simplify; naive_solver. Qed. `````` Robbert Krebbers committed Sep 20, 2016 149 150 `````` Lemma env_lookup_env_delete Γ j : env_wf Γ → env_delete j Γ !! j = None. `````` Robbert Krebbers committed Apr 11, 2016 151 ``````Proof. induction 1; intros; simplify; eauto. Qed. `````` Robbert Krebbers committed Sep 20, 2016 152 153 ``````Lemma env_lookup_env_delete_ne Γ i j : i ≠ j → env_delete j Γ !! i = Γ !! i. Proof. induction Γ; intros; simplify; eauto. Qed. `````` Robbert Krebbers committed Apr 11, 2016 154 155 ``````Lemma env_delete_fresh Γ i j : Γ !! i = None → env_delete j Γ !! i = None. Proof. induction Γ; intros; simplify; eauto. Qed. `````` Robbert Krebbers committed Sep 20, 2016 156 `````` `````` Robbert Krebbers committed Apr 11, 2016 157 158 159 ``````Lemma env_delete_wf Γ j : env_wf Γ → env_wf (env_delete j Γ). Proof. induction 1; simplify; eauto using env_delete_fresh. Qed. `````` Robbert Krebbers committed May 07, 2016 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 ``````Global Instance env_Forall2_refl (P : relation A) : Reflexive P → Reflexive (env_Forall2 P). Proof. intros ? Γ. induction Γ; constructor; auto. Qed. Global Instance env_Forall2_sym (P : relation A) : Symmetric P → Symmetric (env_Forall2 P). Proof. induction 2; constructor; auto. Qed. Global Instance env_Forall2_trans (P : relation A) : Transitive P → Transitive (env_Forall2 P). Proof. intros ? Γ1 Γ2 Γ3 HΓ; revert Γ3. induction HΓ; inversion_clear 1; constructor; eauto. Qed. Global Instance env_Forall2_antisymm (P Q : relation A) : AntiSymm P Q → AntiSymm (env_Forall2 P) (env_Forall2 Q). Proof. induction 2; inversion_clear 1; constructor; auto. Qed. Lemma env_Forall2_impl {B} (P Q : A → B → Prop) Γ Σ : env_Forall2 P Γ Σ → (∀ x y, P x y → Q x y) → env_Forall2 Q Γ Σ. Proof. induction 1; constructor; eauto. Qed. Global Instance Esnoc_proper (P : relation A) : Proper (env_Forall2 P ==> (=) ==> P ==> env_Forall2 P) Esnoc. Proof. intros Γ1 Γ2 HΓ i ? <-; by constructor. Qed. Global Instance env_to_list_proper (P : relation A) : Proper (env_Forall2 P ==> Forall2 P) env_to_list. Proof. induction 1; constructor; auto. Qed. `````` Robbert Krebbers committed Apr 11, 2016 186 187 188 189 190 191 192 ``````Lemma env_Forall2_fresh {B} (P : A → B → Prop) Γ Σ i : env_Forall2 P Γ Σ → Γ !! i = None → Σ !! i = None. Proof. by induction 1; simplify. Qed. Lemma env_Forall2_wf {B} (P : A → B → Prop) Γ Σ : env_Forall2 P Γ Σ → env_wf Γ → env_wf Σ. Proof. induction 1; inversion_clear 1; eauto using env_Forall2_fresh. Qed. End env.``````