blob: 1134b5d052a069252e8c593ed524db783d8bc420 (
plain)
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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Wf.
Require Import Crypto.Compilers.Eta.
Require Import Crypto.Compilers.EtaInterp.
Require Import Crypto.Compilers.ExprInversion.
Require Import Crypto.Compilers.WfInversion.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.SplitInContext.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}.
Local Notation exprf := (@exprf base_type_code op).
Local Ltac t_step :=
match goal with
| _ => intro
| _ => progress subst
| _ => progress destruct_head' sig
| _ => progress destruct_head' and
| _ => progress simpl in *
| _ => progress inversion_expr
| _ => progress destruct_head' @expr
| _ => progress invert_expr_step
| [ |- iff _ _ ] => split
| [ |- wf _ _ ] => constructor
| _ => progress split_iff
| _ => rewrite eq_interp_flat_type_eta_gen by assumption
| [ H : _ |- _ ] => rewrite eq_interp_flat_type_eta_gen in H by assumption
| [ H : context[interp_flat_type_eta_gen] |- _ ]
=> setoid_rewrite eq_interp_flat_type_eta_gen in H; [ | assumption.. ]
| _ => progress break_match
| [ H : wff _ _ _ |- _ ] => solve [ inversion H ]
| [ |- wff _ _ _ ] => constructor
| _ => solve [ auto | congruence | tauto ]
end.
Local Ltac t := repeat t_step.
Local Hint Constructors wff.
Section with_var.
Context {var1 var2 : base_type_code -> Type}.
Section gen_flat_type.
Context (eta : forall {A B}, A * B -> A * B)
(eq_eta : forall A B x, @eta A B x = x).
Section gen_type.
Context (exprf_eta1 : forall {t} (e : exprf t), exprf t)
(exprf_eta2 : forall {t} (e : exprf t), exprf t)
(wff_exprf_eta : forall G t e1 e2, @wff _ _ var1 var2 G t e1 e2
<-> @wff _ _ var1 var2 G t (@exprf_eta1 t e1) (@exprf_eta2 t e2)).
Lemma wf_expr_eta_gen {t e1 e2}
: wf (expr_eta_gen eta exprf_eta1 (t:=t) e1)
(expr_eta_gen eta exprf_eta2 (t:=t) e2)
<-> wf e1 e2.
Proof using Type*. unfold expr_eta_gen; t; inversion_wf_step; t. Qed.
End gen_type.
Lemma wff_exprf_eta_gen {t e1 e2} G
: wff G (exprf_eta_gen eta (t:=t) e1) (exprf_eta_gen eta (t:=t) e2)
<-> @wff base_type_code op var1 var2 G t e1 e2.
Proof using eq_eta.
revert G; induction e1; first [ progress invert_expr | destruct e2 ];
t; inversion_wf_step; t.
Qed.
End gen_flat_type.
(* Local *) Hint Resolve -> wff_exprf_eta_gen.
(* Local *) Hint Resolve <- wff_exprf_eta_gen.
Lemma wff_exprf_eta {G t e1 e2}
: wff G (exprf_eta (t:=t) e1) (exprf_eta (t:=t) e2)
<-> @wff base_type_code op var1 var2 G t e1 e2.
Proof using Type. setoid_rewrite wff_exprf_eta_gen; reflexivity. Qed.
Lemma wff_exprf_eta' {G t e1 e2}
: wff G (exprf_eta' (t:=t) e1) (exprf_eta' (t:=t) e2)
<-> @wff base_type_code op var1 var2 G t e1 e2.
Proof using Type. setoid_rewrite wff_exprf_eta_gen; intuition. Qed.
Lemma wf_expr_eta {t e1 e2}
: wf (expr_eta (t:=t) e1) (expr_eta (t:=t) e2)
<-> @wf base_type_code op var1 var2 t e1 e2.
Proof using Type.
unfold expr_eta, exprf_eta.
setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto).
Qed.
Lemma wf_expr_eta' {t e1 e2}
: wf (expr_eta' (t:=t) e1) (expr_eta' (t:=t) e2)
<-> @wf base_type_code op var1 var2 t e1 e2.
Proof using Type.
unfold expr_eta', exprf_eta'.
setoid_rewrite wf_expr_eta_gen; intuition (solve [ eapply wff_exprf_eta_gen; [ | eassumption ]; intuition ] || eauto).
Qed.
End with_var.
Lemma Wf_ExprEtaGen
(eta : forall {A B}, A * B -> A * B)
(eq_eta : forall A B x, @eta A B x = x)
{t e}
: Wf (ExprEtaGen (@eta) e) <-> @Wf base_type_code op t e.
Proof using Type.
split; intros H var1 var2; specialize (H var1 var2);
revert H; eapply wf_expr_eta_gen; try eassumption; intros;
symmetry; apply wff_exprf_eta_gen;
auto.
Qed.
Lemma Wf_ExprEta_iff
{t e}
: Wf (ExprEta e) <-> @Wf base_type_code op t e.
Proof using Type.
unfold Wf; setoid_rewrite wf_expr_eta; reflexivity.
Qed.
Lemma Wf_ExprEta'_iff
{t e}
: Wf (ExprEta' e) <-> @Wf base_type_code op t e.
Proof using Type.
unfold Wf; setoid_rewrite wf_expr_eta'; reflexivity.
Qed.
Definition Wf_ExprEta {t e} : Wf e -> Wf (ExprEta e) := proj2 (@Wf_ExprEta_iff t e).
Definition Wf_ExprEta' {t e} : Wf e -> Wf (ExprEta' e) := proj2 (@Wf_ExprEta'_iff t e).
End language.
Hint Resolve Wf_ExprEta Wf_ExprEta' : wf.
|
