environments.v 9.87 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2 3 4 5 6 7 8 9
From iris.prelude Require Export strings.
From iris.algebra Require Export base.
From iris.prelude Require Import stringmap.

Inductive env (A : Type) : Type :=
  | Enil : env A
  | Esnoc : env A  string  A  env A.
Arguments Enil {_}.
Arguments Esnoc {_} _ _%string _.
10 11
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32

Local Notation "x ← y ; z" := (match y with Some x => z | None => None end).
Local Notation "' ( x1 , x2 ) ← y ; z" :=
  (match y with Some (x1,x2) => z | None => None end).
Local Notation "' ( x1 , x2 , x3 ) ← y ; z" :=
  (match y with Some (x1,x2,x3) => z | None => None end).

Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
  match Γ with
  | Enil => None
  | Esnoc Γ j x => if decide (i = j) then Some x else env_lookup i Γ
  end.
Local Notation "Γ !! j" := (env_lookup j Γ).

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.
33
Instance: Params (@env_to_list) 1.
34

35 36
Fixpoint env_dom {A} (Γ : env A) : list string :=
  match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
37 38 39 40 41 42

Fixpoint env_fold {A B} (f : B  A  A) (x : A) (Γ : env B) : A :=
  match Γ with
  | Enil => x
  | Esnoc Γ _ y => env_fold f (f y x) Γ
  end.
Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 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 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 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 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203

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.
Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
     if decide (i = j) then env_app Γi Γ else
     match Γi !! j with
     | None => Γ'  env_replace i Γi Γ; Some (Esnoc Γ' j x)
     | Some _ => None
     end
  end.
Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
  match Γ with
  | Enil => Enil
  | Esnoc Γ j x => if decide (i = j) then Γ else Esnoc (env_delete i Γ) j x
  end.
Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
     if decide (i = j) then Some (x,Γ)
     else '(y,Γ')  env_lookup_delete i Γ; Some (y, Esnoc Γ' j x)
  end.
Fixpoint env_split_go {A} (js : list string)
    (Γ1 Γ2 : env A) : option (env A * env A) :=
  match js with
  | [] => Some (Γ1, Γ2)
  | j::js => '(x,Γ2)  env_lookup_delete j Γ2; env_split_go js (Esnoc Γ1 j x) Γ2
  end.
Definition env_split {A} (js : list string)
  (Γ : env A) : option (env A * env A) := env_split_go js Enil Γ.

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.

Ltac simplify := repeat (case_match || simplify_option_eq).

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.

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.
  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify_eq/=.
  destruct (decide (i = j)); simplify_eq/=; auto using env_app_perm.
  destruct (Γi !! j), (env_replace i Γi Γ) as [Γ''|] eqn:?; simplify_eq/=.
  rewrite -Permutation_middle; f_equiv; eauto.
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.
Lemma env_delete_fresh_eq Γ j : env_wf Γ  env_delete j Γ !! j = None.
Proof. induction 1; intros; simplify; eauto. Qed.
Lemma env_delete_fresh Γ i j : Γ !! i = None  env_delete j Γ !! i = None.
Proof. induction Γ; intros; simplify; eauto. Qed.
Lemma env_delete_wf Γ j : env_wf Γ  env_wf (env_delete j Γ).
Proof. induction 1; simplify; eauto using env_delete_fresh. Qed.

Lemma env_split_fresh Γ1 Γ2 Γ1' Γ2' js i :
  env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') 
  Γ1 !! i = None  Γ2 !! i = None  Γ1' !! i = None  Γ2' !! i = None.
Proof.
  revert Γ1 Γ2.
  induction js as [|j js IH]=> Γ1 Γ2 ???; simplify_eq/=; eauto.
  destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=.
  apply env_lookup_delete_Some in Hdelete as [? ->].
  eapply IH; eauto; simplify; eauto using env_delete_fresh.
Qed.
Lemma env_split_go_wf Γ1 Γ2 Γ1' Γ2' js :
  env_split_go js Γ1 Γ2 = Some (Γ1',Γ2') 
  ( i, Γ1 !! i = None  Γ2 !! i = None) 
  env_wf Γ1  env_wf Γ2  env_wf Γ1'  env_wf Γ2'.
Proof.
  revert Γ1 Γ2.
  induction js as [|j js IH]=> Γ1 Γ2 ? Hdisjoint ??; simplify_eq/=; auto.
  destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=.
  apply env_lookup_delete_Some in Hdelete as [? ->].
  eapply IH; eauto using env_delete_wf.
  - intros i; simplify; eauto using env_delete_fresh_eq.
    destruct (Hdisjoint i); eauto using env_delete_fresh.  
  - constructor; auto.
    destruct (Hdisjoint j) as [?|[]%eq_None_not_Some]; eauto.
Qed.
Lemma env_split_go_perm Γ1 Γ2 Γ1' Γ2' js :
  env_split_go js Γ1 Γ2 = Some (Γ1',Γ2')  Γ1 ++ Γ2  Γ1' ++ Γ2'.
Proof.
  revert Γ1 Γ2. induction js as [|j js IH]=> Γ1 Γ2 ?; simplify_eq/=; auto.
  destruct (env_lookup_delete j Γ2) as [[x Γ2'']|] eqn:Hdelete; simplify_eq/=.
  apply env_lookup_delete_Some in Hdelete as [? ->].
  by rewrite -(IH (Esnoc _ _ _) (env_delete _ _)) //=
    Permutation_middle -env_lookup_perm.
Qed.

Lemma env_split_fresh_1 Γ Γ1 Γ2 js i :
  env_split js Γ = Some (Γ1,Γ2)  Γ !! i = None  Γ1 !! i = None.
Proof. intros. by apply (env_split_fresh Enil Γ Γ1 Γ2 js). Qed.
Lemma env_split_fresh_2 Γ Γ1 Γ2 js i :
  env_split js Γ = Some (Γ1,Γ2)  Γ !! i = None  Γ2 !! i = None.
Proof. intros. by apply (env_split_fresh Enil Γ Γ1 Γ2 js). Qed.
Lemma env_split_wf_1 Γ Γ1 Γ2 js :
  env_split js Γ = Some (Γ1,Γ2)  env_wf Γ  env_wf Γ1.
Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed.
Lemma env_split_wf_2 Γ Γ1 Γ2 js :
  env_split js Γ = Some (Γ1,Γ2)  env_wf Γ  env_wf Γ2.
Proof. intros. apply (env_split_go_wf Enil Γ Γ1 Γ2 js); eauto. Qed.
Lemma env_split_perm Γ Γ1 Γ2 js : env_split js Γ = Some (Γ1,Γ2)  Γ  Γ1 ++ Γ2.
Proof. apply env_split_go_perm. Qed.

204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
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's avatar
Robbert Krebbers committed
230 231 232 233 234 235 236
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.