environments.v 7.48 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From fast_string Require Export fast_string_lib.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.algebra Require Export base.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
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 _.
10
11
Instance: Params (@Enil) 1.
Instance: Params (@Esnoc) 1.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
14
15

Fixpoint env_lookup {A} (i : string) (Γ : env A) : option A :=
  match Γ with
  | Enil => None
16
  | Esnoc Γ j x => if string_beq i j then Some x else env_lookup i Γ
Robbert Krebbers's avatar
Robbert Krebbers committed
17
  end.
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's avatar
Robbert Krebbers committed
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.
36
Instance: Params (@env_to_list) 1.
37

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

Robbert Krebbers's avatar
Robbert Krebbers committed
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.
48

Robbert Krebbers's avatar
Robbert Krebbers committed
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 =>
53
     if string_beq i j then env_app Γi Γ else
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
56
57
58
     match Γi !! j with
     | None => Γ'  env_replace i Γi Γ; Some (Esnoc Γ' j x)
     | Some _ => None
     end
  end.
59

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

Robbert Krebbers's avatar
Robbert Krebbers committed
66
67
68
69
Fixpoint env_lookup_delete {A} (i : string) (Γ : env A) : option (A * env A) :=
  match Γ with
  | Enil => None
  | Esnoc Γ j x =>
70
     if string_beq i j then Some (x,Γ)
Robbert Krebbers's avatar
Robbert Krebbers committed
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.

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's avatar
Robbert Krebbers committed
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.

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's avatar
Robbert Krebbers committed
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.
139
140
  revert Γ'. induction Γ as [|Γ IH j y]=>Γ' ?; simplify; auto using env_app_perm.
  rewrite -Permutation_middle -IH //.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
149
150

Lemma env_lookup_env_delete Γ j : env_wf Γ  env_delete j Γ !! j = None.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
Proof. induction 1; intros; simplify; eauto. Qed.
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's avatar
Robbert Krebbers committed
154
155
Lemma env_delete_fresh Γ i j : Γ !! i = None  env_delete j Γ !! i = None.
Proof. induction Γ; intros; simplify; eauto. Qed.
156

Robbert Krebbers's avatar
Robbert Krebbers committed
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.

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's avatar
Robbert Krebbers committed
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.