-
Notifications
You must be signed in to change notification settings - Fork 4
/
DemoValueTerm.v
169 lines (140 loc) · 4.5 KB
/
DemoValueTerm.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
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
Set Implicit Arguments.
Require Import Dblib.DblibTactics.
Require Import Dblib.DeBruijn.
(* Application to values & terms. *)
Inductive my_term :=
| MyTValue: my_value -> my_term
| MyTApp: my_term -> my_term -> my_term
with my_value :=
| MyVVar: nat -> my_value
| MyVAbs: my_term -> my_value.
Instance Var_my_value : Var my_value := {
var := MyVVar
}.
Fixpoint traverse_my_term (f : nat -> nat -> my_value) l t :=
match t with
| MyTValue v =>
MyTValue (traverse_my_value f l v)
| MyTApp t1 t2 =>
MyTApp (traverse_my_term f l t1) (traverse_my_term f l t2)
end
with traverse_my_value f l v :=
match v with
| MyVVar x =>
f l x
| MyVAbs t =>
MyVAbs (traverse_my_term f (1 + l) t)
end.
Instance Traverse_my_value_my_value : Traverse my_value my_value := {
traverse := traverse_my_value
}.
Instance Traverse_my_value_my_term : Traverse my_value my_term := {
traverse := traverse_my_term
}.
(* TEMPORARY It is unfortunate that we have to first prove two
mutually dependent lemmas using [Lemma ... with ...], then write
down two independent [Instance] declarations. I would prefer to be
able to directly write two mutually depdendent instance
declarations, using [Instance ... with ...]. Here, I am forced to
duplicate the statement of the properties of interest, which is
unpleasant. *)
Lemma traverse_my_value_injective:
forall f,
(forall x1 x2 l, f l x1 = f l x2 -> x1 = x2) ->
forall (t1 t2 : my_value) l,
traverse_var f l t1 = traverse_var f l t2 ->
t1 = t2
with traverse_my_term_injective:
forall f,
(forall x1 x2 l, f l x1 = f l x2 -> x1 = x2) ->
forall (t1 t2 : my_term) l,
traverse_var f l t1 = traverse_var f l t2 ->
t1 = t2.
Proof.
prove_traverse_var_injective.
prove_traverse_var_injective.
Qed.
Instance TraverseVarInjective_my_value_my_value :
@TraverseVarInjective my_value _ my_value _.
Proof.
constructor. apply traverse_my_value_injective.
Qed.
Instance TraverseVarInjective_my_value_my_term :
@TraverseVarInjective my_value _ my_term _.
Proof.
constructor. apply traverse_my_term_injective.
Qed.
Lemma traverse_functorial_value_value:
forall f g (t : my_value) l,
traverse g l (traverse f l t) = traverse (fun l x => traverse g l (f l x)) l t
with traverse_functorial_value_term:
forall f g (t : my_term) l,
traverse g l (traverse f l t) = traverse (fun l x => traverse g l (f l x)) l t.
Proof.
prove_traverse_functorial.
prove_traverse_functorial.
Qed.
Instance TraverseFunctorial_my_value_my_value : @TraverseFunctorial my_value _ my_value _.
Proof. constructor. apply traverse_functorial_value_value. Qed.
Instance TraverseFunctorial_my_term_my_term : @TraverseFunctorial my_value _ my_term _.
Proof. constructor. apply traverse_functorial_value_term. Qed.
Instance TraverseIdentifiesVar_my_value : TraverseIdentifiesVar.
Proof. constructor. prove_traverse_identifies_var. Qed.
Lemma traverse_relative_my_value_my_value:
forall f g p (t : my_value) m l,
(forall l x, f (l + p) x = g l x) ->
m = l + p ->
traverse f m t =
traverse g l t
with traverse_relative_my_value_my_term:
forall f g p (t : my_term) m l,
(forall l x, f (l + p) x = g l x) ->
m = l + p ->
traverse f m t =
traverse g l t.
Proof.
prove_traverse_relative.
prove_traverse_relative.
Qed.
Instance TraverseRelative_my_value_my_value : @TraverseRelative my_value my_value _.
Proof.
constructor. apply traverse_relative_my_value_my_value.
Qed.
Instance TraverseRelative_my_value_my_term : @TraverseRelative my_value my_term _.
Proof.
constructor. apply traverse_relative_my_value_my_term.
Qed.
Lemma traverse_my_value_var_is_identity:
forall f,
(forall l x, f l x = var x) ->
forall (t : my_value) l,
traverse f l t = t
with traverse_my_term_var_is_identity:
forall f,
(forall l x, f l x = var x) ->
forall (t : my_term) l,
traverse f l t = t.
Proof.
prove_traverse_var_is_identity.
prove_traverse_var_is_identity.
Qed.
Instance TraverseVarIsIdentity_my_value_my_value : @TraverseVarIsIdentity my_value _ my_value _.
Proof.
constructor. apply traverse_my_value_var_is_identity.
Qed.
Instance TraverseVarIsIdentity_my_value_my_term : @TraverseVarIsIdentity my_value _ my_term _.
Proof.
constructor. apply traverse_my_term_var_is_identity.
Qed.
Lemma lift_MyVAbs:
forall w k t,
lift w k (MyVAbs t) = MyVAbs (lift w (1 + k) t).
Proof.
intros. simpl_lift_goal. reflexivity.
Qed.
Lemma subst_MyVAbs:
forall v k t,
subst v k (MyVAbs t) = MyVAbs (subst (shift 0 v) (1 + k) t).
Proof.
intros. simpl_subst_goal. reflexivity.
Qed.