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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Eta.
Require Import Crypto.Compilers.ExprInversion.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.DestructHead.
Section language.
Context {base_type_code : Type}
{interp_base_type : base_type_code -> Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
{interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}.
Local Notation exprf := (@exprf base_type_code op interp_base_type).
Local Ltac t_step :=
match goal with
| _ => reflexivity
| _ => progress simpl in *
| _ => intro
| _ => progress break_match
| _ => progress destruct_head prod
| _ => progress cbv [LetIn.Let_In]
| [ H : _ |- _ ] => rewrite H
| _ => progress autorewrite with core
| [ H : forall A B x, ?f A B x = x, H' : context[?f _ _ _] |- _ ]
=> rewrite H in H'
| _ => progress unfold interp_flat_type_eta, interp_flat_type_eta', exprf_eta, exprf_eta', expr_eta, expr_eta'
end.
Local Ltac t := repeat t_step.
Section gen_flat_type.
Context (eta : forall {A B}, A * B -> A * B)
(eq_eta : forall A B x, @eta A B x = x).
Lemma eq_interp_flat_type_eta_gen {var t T f} x
: @interp_flat_type_eta_gen base_type_code var eta t T f x = f x.
Proof using eq_eta. induction t; t. Qed.
(* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen.
Section gen_type.
Context (exprf_eta : forall {t} (e : exprf t), exprf t)
(eq_interp_exprf_eta : forall t e, interpf (@interp_op) (@exprf_eta t e) = interpf (@interp_op) e).
Lemma interp_expr_eta_gen {t e}
: forall x,
interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e) x = interp (@interp_op) e x.
Proof using Type*. t. Qed.
End gen_type.
(* Local *) Hint Rewrite @interp_expr_eta_gen.
Lemma interpf_exprf_eta_gen {t e}
: interpf (@interp_op) (exprf_eta_gen eta (t:=t) e) = interpf (@interp_op) e.
Proof using eq_eta. induction e; t. Qed.
Lemma InterpExprEtaGen {t e}
: forall x, Interp (@interp_op) (ExprEtaGen eta (t:=t) e) x = Interp (@interp_op) e x.
Proof using eq_eta. apply interp_expr_eta_gen; intros; apply interpf_exprf_eta_gen. Qed.
End gen_flat_type.
(* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen.
(* Local *) Hint Rewrite @interp_expr_eta_gen.
(* Local *) Hint Rewrite @interpf_exprf_eta_gen.
Lemma eq_interp_flat_type_eta {var t T f} x
: @interp_flat_type_eta base_type_code var t T f x = f x.
Proof using Type. t. Qed.
(* Local *) Hint Rewrite @eq_interp_flat_type_eta.
Lemma eq_interp_flat_type_eta' {var t T f} x
: @interp_flat_type_eta' base_type_code var t T f x = f x.
Proof using Type. t. Qed.
(* Local *) Hint Rewrite @eq_interp_flat_type_eta'.
Lemma interpf_exprf_eta {t e}
: interpf (@interp_op) (exprf_eta (t:=t) e) = interpf (@interp_op) e.
Proof using Type. t. Qed.
(* Local *) Hint Rewrite @interpf_exprf_eta.
Lemma interpf_exprf_eta' {t e}
: interpf (@interp_op) (exprf_eta' (t:=t) e) = interpf (@interp_op) e.
Proof using Type. t. Qed.
(* Local *) Hint Rewrite @interpf_exprf_eta'.
Lemma interp_expr_eta {t e}
: forall x, interp (@interp_op) (expr_eta (t:=t) e) x = interp (@interp_op) e x.
Proof using Type. t. Qed.
Lemma interp_expr_eta' {t e}
: forall x, interp (@interp_op) (expr_eta' (t:=t) e) x = interp (@interp_op) e x.
Proof using Type. t. Qed.
Lemma InterpExprEta {t e}
: forall x, Interp (@interp_op) (ExprEta (t:=t) e) x = Interp (@interp_op) e x.
Proof using Type. apply interp_expr_eta. Qed.
Lemma InterpExprEta' {t e}
: forall x, Interp (@interp_op) (ExprEta' (t:=t) e) x = Interp (@interp_op) e x.
Proof using Type. apply interp_expr_eta'. Qed.
Lemma InterpExprEta_arrow {s d e}
: forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x = Interp (@interp_op) e x.
Proof using Type. exact (@InterpExprEta (Arrow s d) e). Qed.
Lemma InterpExprEta'_arrow {s d e}
: forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x = Interp (@interp_op) e x.
Proof using Type. exact (@InterpExprEta' (Arrow s d) e). Qed.
Lemma InterpExprEta_ind {t} (P : _ -> Prop) {e x}
: P (Interp (@interp_op) e x) -> P (Interp (@interp_op) (ExprEta (t:=t) e) x).
Proof using Type. rewrite InterpExprEta; exact id. Qed.
Lemma InterpExprEta'_ind {t} (P : _ -> Prop) {e x}
: P (Interp (@interp_op) e x) -> P (Interp (@interp_op) (ExprEta' (t:=t) e) x).
Proof using Type. rewrite InterpExprEta'; exact id. Qed.
Lemma InterpExprEta_arrow_ind {s d} (P : _ -> Prop) {e x}
: P (Interp (@interp_op) e x) -> P (Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x).
Proof using Type. rewrite InterpExprEta_arrow; exact id. Qed.
Lemma InterpExprEta'_arrow_ind {s d} (P : _ -> Prop) {e x}
: P (Interp (@interp_op) e x) -> P (Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x).
Proof using Type. rewrite InterpExprEta'_arrow; exact id. Qed.
Lemma eq_interp_eta {t e}
: forall x, interp_eta interp_op (t:=t) e x = interp interp_op e x.
Proof using Type. apply eq_interp_flat_type_eta. Qed.
Lemma eq_InterpEta {t e}
: forall x, InterpEta interp_op (t:=t) e x = Interp interp_op e x.
Proof using Type. apply eq_interp_eta. Qed.
End language.
Hint Rewrite @eq_interp_flat_type_eta @eq_interp_flat_type_eta' @interpf_exprf_eta @interpf_exprf_eta' @interp_expr_eta @interp_expr_eta' @InterpExprEta @InterpExprEta' @InterpExprEta_arrow @InterpExprEta'_arrow @eq_interp_eta @eq_InterpEta : reflective_interp.
|
