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
169
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.ExprInversion.
Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
Local Open Scope ctype_scope.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}.
Local Notation flat_type := (flat_type base_type_code).
Local Notation type := (type base_type_code).
Local Notation exprf := (@exprf base_type_code op).
Local Notation expr := (@expr base_type_code op).
Local Notation Expr := (@Expr base_type_code op).
Local Notation wff := (@wff base_type_code op).
Section with_var.
Context {var1 var2 : base_type_code -> Type}.
Local Hint Constructors Syntax.wff.
Lemma wff_app' {g G0 G1 t e1 e2}
(wf : @wff var1 var2 (G0 ++ G1) t e1 e2)
: wff (G0 ++ g ++ G1) e1 e2.
Proof.
rewrite !List.app_assoc.
revert wf; remember (G0 ++ G1)%list as G eqn:?; intro wf.
revert dependent G0. revert dependent G1.
induction wf; simpl in *; constructor; simpl; eauto.
{ subst; rewrite !List.in_app_iff in *; intuition. }
{ intros; subst.
rewrite !List.app_assoc; eauto using List.app_assoc. }
Qed.
Lemma wff_app_pre {g G t e1 e2}
(wf : @wff var1 var2 G t e1 e2)
: wff (g ++ G) e1 e2.
Proof.
apply (@wff_app' _ nil); assumption.
Qed.
Lemma wff_app_post {g G t e1 e2}
(wf : @wff var1 var2 G t e1 e2)
: wff (G ++ g) e1 e2.
Proof.
pose proof (@wff_app' g G nil t e1 e2) as H.
rewrite !List.app_nil_r in *; auto.
Qed.
Lemma wff_in_impl_Proper G0 G1 {t} e1 e2
: @wff var1 var2 G0 t e1 e2
-> (forall x, List.In x G0 -> List.In x G1)
-> @wff var1 var2 G1 t e1 e2.
Proof.
intro wf; revert G1; induction wf;
repeat match goal with
| _ => setoid_rewrite List.in_app_iff
| _ => progress intros
| _ => progress simpl in *
| [ |- wff _ _ _ ] => constructor
| [ H : _ |- _ ] => apply H
| _ => solve [ intuition eauto ]
end.
Qed.
Local Hint Resolve List.in_app_or List.in_or_app.
Local Hint Extern 1 => progress unfold List.In in *.
Local Hint Resolve wff_in_impl_Proper.
Lemma wff_SmartVarf {t} x1 x2
: @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVarf x1) (SmartVarf x2).
Proof.
unfold SmartVarf.
induction t; simpl; constructor; eauto.
Qed.
Local Hint Resolve wff_SmartVarf.
Lemma wff_SmartVarVarf G {t t'} v1 v2 x1 x2
(Hin : List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x1, x2))
(flatten_binding_list base_type_code (SmartVarVarf v1) (SmartVarVarf v2)))
: @wff var1 var2 (flatten_binding_list base_type_code (t:=t') v1 v2 ++ G) (Tbase t) x1 x2.
Proof.
revert dependent G; induction t'; intros; simpl in *; try tauto.
{ intuition (inversion_sigma; inversion_prod; subst; simpl; eauto).
constructor; eauto. }
{ unfold SmartVarVarf in *; simpl in *.
apply List.in_app_iff in Hin.
intuition (inversion_sigma; inversion_prod; subst; eauto).
{ rewrite <- !List.app_assoc; eauto. } }
Qed.
End with_var.
Definition duplicate_type {var1 var2}
: { t : base_type_code & (var1 t * var2 t)%type }
-> { t1t2 : _ & (var1 (fst t1t2) * var2 (snd t1t2))%type }
:= fun txy => existT _ (projT1 txy, projT1 txy) (projT2 txy).
Definition duplicate_types {var1 var2}
:= List.map (@duplicate_type var1 var2).
Lemma flatten_binding_list_flatten_binding_list2
{var1 var2 t1} x1 x2
: duplicate_types (@flatten_binding_list base_type_code var1 var2 t1 x1 x2)
= @flatten_binding_list2 base_type_code var1 var2 t1 t1 x1 x2.
Proof.
induction t1; simpl; try reflexivity.
rewrite_hyp <- !*.
unfold duplicate_types; rewrite List.map_app; reflexivity.
Qed.
Local Ltac flatten_t :=
repeat first [ reflexivity
| intro
| progress simpl @flatten_binding_list
| progress simpl @flatten_binding_list2
| rewrite !List.map_app
| progress simpl in *
| rewrite_hyp <- !*; reflexivity
| rewrite_hyp !*; reflexivity ].
Lemma flatten_binding_list2_SmartVarfMap
{var1 var1' var2 var2' t1 t2} f g (x1 : interp_flat_type var1 t1) (x2 : interp_flat_type var2 t2)
: flatten_binding_list2 (var1:=var1') (var2:=var2') base_type_code (SmartVarfMap f x1) (SmartVarfMap g x2)
= List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), g _ (snd (projT2 txy)))%core)
(flatten_binding_list2 base_type_code x1 x2).
Proof.
revert dependent t2; induction t1, t2; flatten_t.
Qed.
Lemma flatten_binding_list2_SmartVarfMap1
{var1 var1' var2' t1 t2} f (x1 : interp_flat_type var1 t1) (x2 : interp_flat_type var2' t2)
: flatten_binding_list2 (var1:=var1') (var2:=var2') base_type_code (SmartVarfMap f x1) x2
= List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), snd (projT2 txy))%core)
(flatten_binding_list2 base_type_code x1 x2).
Proof.
revert dependent t2; induction t1, t2; flatten_t.
Qed.
Lemma flatten_binding_list2_SmartVarfMap2
{var1' var2 var2' t1 t2} g (x1 : interp_flat_type var1' t1) (x2 : interp_flat_type var2 t2)
: flatten_binding_list2 (var1:=var1') (var2:=var2') base_type_code x1 (SmartVarfMap g x2)
= List.map (fun txy => existT _ (projT1 txy) (fst (projT2 txy), g _ (snd (projT2 txy)))%core)
(flatten_binding_list2 base_type_code x1 x2).
Proof.
revert dependent t2; induction t1, t2; flatten_t.
Qed.
Lemma flatten_binding_list_SmartVarfMap
{var1 var1' var2 var2' t} f g (x1 : interp_flat_type var1 t) (x2 : interp_flat_type var2 t)
: flatten_binding_list (var1:=var1') (var2:=var2') base_type_code (SmartVarfMap f x1) (SmartVarfMap g x2)
= List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), g _ (snd (projT2 txy)))%core)
(flatten_binding_list base_type_code x1 x2).
Proof. induction t; flatten_t. Qed.
Lemma flatten_binding_list2_SmartValf
{T1 T2} f g t1 t2
: flatten_binding_list2 base_type_code (SmartValf T1 f t1) (SmartValf T2 g t2)
= List.map (fun txy => existT _ (projT1 txy) (f _, g _)%core)
(flatten_binding_list2 base_type_code (SmartFlatTypeUnMap t1) (SmartFlatTypeUnMap t2)).
Proof.
revert dependent t2; induction t1, t2; flatten_t.
Qed.
Lemma flatten_binding_list_SmartValf
{T1 T2} f g t
: flatten_binding_list base_type_code (SmartValf T1 f t) (SmartValf T2 g t)
= List.map (fun txy => existT _ (projT1 txy) (f _, g _)%core)
(flatten_binding_list base_type_code (SmartFlatTypeUnMap t) (SmartFlatTypeUnMap t)).
Proof. induction t; flatten_t. Qed.
End language.
|
