-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathEnvironment.v
126 lines (113 loc) · 2.41 KB
/
Environment.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
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
Require Import Arith List.
Inductive environment A :=
| Empty : environment A
| Extend : nat -> A -> environment A -> environment A.
Fixpoint lookup {A : Type} x env : option A :=
match env with
| Empty =>
None
| Extend x' a env' =>
if beq_nat x x'
then Some a
else lookup x env'
end.
Definition env_equiv {A : Type} env env' :=
forall x,
@lookup A x env = lookup x env'.
Require Import Setoid.
Instance tc_env_equiv {A : Type} : Equivalence (@env_equiv A).
Proof.
unfold env_equiv.
split.
unfold Reflexive; intros.
reflexivity.
unfold Symmetric; intros.
rewrite H.
reflexivity.
unfold Transitive; intros.
rewrite H, H0.
reflexivity.
Qed.
Lemma env_equiv_extend_eq {A : Type} :
forall x v env env',
env_equiv env env' ->
env_equiv (Extend A x v env) (Extend A x v env').
Proof.
unfold env_equiv.
intros.
simpl.
destruct (beq_nat x0 x).
reflexivity.
apply H.
Qed.
Lemma lookup_empty {A : Type} :
forall x,
lookup x (Empty A) = None.
Proof.
reflexivity.
Qed.
Lemma lookup_extend_eq {A : Type} :
forall x v env,
lookup x (Extend A x v env) = Some v.
Proof.
intros.
simpl.
rewrite <- beq_nat_refl.
reflexivity.
Qed.
Lemma lookup_extend_neq {A : Type} :
forall x x' v' env,
beq_nat x x' = false ->
lookup x (Extend A x' v' env) = lookup x env.
Proof.
intros.
simpl.
rewrite H.
reflexivity.
Qed.
Lemma env_shadow :
forall A x v v' env,
env_equiv (Extend A x v (Extend A x v' env)) (Extend A x v env).
Proof.
intros.
unfold env_equiv.
intros x'.
simpl.
remember (beq_nat x' x) as b.
destruct b.
reflexivity.
reflexivity.
Qed.
Lemma env_permute :
forall A x x' v v' env,
beq_nat x x' = false ->
env_equiv (Extend A x v (Extend A x' v' env)) (Extend A x' v' (Extend A x v env)).
Proof.
intros.
unfold env_equiv.
intros y.
simpl.
remember (beq_nat y x) as eqyx.
destruct eqyx.
symmetry in Heqeqyx.
apply beq_nat_true in Heqeqyx.
rewrite Heqeqyx.
rewrite H.
reflexivity.
reflexivity.
Qed.
Fixpoint drop {A : Type} x env : environment A :=
match env with
| Empty =>
Empty _
| Extend x' a env' =>
if beq_nat x x'
then drop x env'
else Extend _ x' a (drop x env')
end.
Definition distinct {A : Type} (env : environment A) :=
forall x v,
lookup x env = Some v ->
exists env',
env_equiv (Extend A x v env') env /\
lookup x env' = None.