environments.v 7.56 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.prelude Require Export strings.
2
From iris.proofmode Require Import strings.
Robbert Krebbers's avatar
Robbert Krebbers committed
3 4
From iris.algebra Require Export base.
From iris.prelude Require Import stringmap.
5
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
6 7 8 9 10 11

Inductive env (A : Type) : Type :=
  | Enil : env A
  | Esnoc : env A  string  A  env A.
Arguments Enil {_}.
Arguments Esnoc {_} _ _%string _.
12 13
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
14 15 16 17

Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
  match Γ with
  | Enil => None
18
  | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
Robbert Krebbers's avatar
Robbert Krebbers committed
19
  end.
20 21 22 23 24 25 26 27 28 29

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's avatar
Robbert Krebbers committed
30 31 32 33 34 35 36 37

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

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

Robbert Krebbers's avatar
Robbert Krebbers committed
43 44 45 46 47 48 49
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.
50

Robbert Krebbers's avatar
Robbert Krebbers committed
51 52 53 54
Fixpoint env_replace {A} (i: string) (Γi: env A) (Γ: env A) : option (env A) :=
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
55
     if string_beq i j then env_app Γi Γ else
Robbert Krebbers's avatar
Robbert Krebbers committed
56 57 58 59 60
     match Γi !! j with
     | None => Γ'  env_replace i Γi Γ; Some (Esnoc Γ' j x)
     | Some _ => None
     end
  end.
61

Robbert Krebbers's avatar
Robbert Krebbers committed
62 63 64
Fixpoint env_delete {A} (i : string) (Γ : env A) : env A :=
  match Γ with
  | Enil => Enil
65
  | Esnoc Γ j x => if string_beq i j then Γ else Esnoc (env_delete i Γ) j x
Robbert Krebbers's avatar
Robbert Krebbers committed
66
  end.
67

Robbert Krebbers's avatar
Robbert Krebbers committed
68 69 70 71
Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
72
     if string_beq i j then Some (x,Γ)
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
     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.

88 89 90 91 92 93 94
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's avatar
Robbert Krebbers committed
95 96 97 98 99 100

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.

101 102 103 104 105 106
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's avatar
Robbert Krebbers committed
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
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.
141 142
  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm.
  rewrite -Permutation_middle -IH //.
Robbert Krebbers's avatar
Robbert Krebbers committed
143 144 145 146 147 148 149 150
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.
151 152

Lemma env_lookup_env_delete Γ j : env_wf Γ  env_delete j Γ !! j = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Proof. induction 1; intros; simplify; eauto. Qed.
154 155
Lemma env_lookup_env_delete_ne Γ i j : i  j  env_delete j Γ !! i = Γ !! i.
Proof. induction Γ; intros; simplify; eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157
Lemma env_delete_fresh Γ i j : Γ !! i = None  env_delete j Γ !! i = None.
Proof. induction Γ; intros; simplify; eauto. Qed.
158

Robbert Krebbers's avatar
Robbert Krebbers committed
159 160 161
Lemma env_delete_wf Γ j : env_wf Γ  env_wf (env_delete j Γ).
Proof. induction 1; simplify; eauto using env_delete_fresh. Qed.

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
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
188 189 190 191 192 193 194
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.