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
|
(** * Convert between interpretations of types *)
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Map.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Tactics.RewriteHyp.
Local Open Scope expr_scope.
Section language.
Context (base_type_code : Type).
Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
Section map.
Context {var1 var2 : base_type_code -> Type}.
Context (f_var12 : forall t, var1 t -> var2 t)
(f_var21 : forall t, var2 t -> var1 t).
Fixpoint mapf
{t}
(e : @exprf base_type_code op var1 t)
: @exprf base_type_code op var2 t
:= match e in @exprf _ _ _ t return @exprf _ _ _ t with
| TT => TT
| Var _ x => Var (f_var12 _ x)
| Op _ _ op args => Op op (@mapf _ args)
| LetIn _ ex _ eC => LetIn (@mapf _ ex)
(fun x => @mapf _ (eC (mapf_interp_flat_type f_var21 x)))
| Pair _ ex _ ey => Pair (@mapf _ ex)
(@mapf _ ey)
end.
Definition map {t} (e : @expr base_type_code op var1 t)
: @expr base_type_code op var2 t
:= match e with
| Abs _ _ f => Abs (fun x => mapf (f (mapf_interp_flat_type f_var21 x)))
end.
End map.
Section mapf_id.
Context (functional_extensionality : forall {A B} (f g : A -> B), (forall x, f x = g x) -> f = g)
{var : base_type_code -> Type}.
Lemma mapf_idmap_ext {t} e
: @mapf var var
(fun _ x => x) (fun _ x => x)
t e
= e.
Proof using functional_extensionality.
induction e;
repeat match goal with
| _ => reflexivity
| _ => progress simpl in *
| _ => rewrite_hyp !*
| _ => apply (f_equal2 (fun x f => LetIn x f))
| _ => solve [ eauto ]
| _ => apply functional_extensionality; intro
end.
clear e IHe H.
revert dependent tC; induction tx; simpl; [ reflexivity | reflexivity | ]; intros.
destruct x as [x0 x1]; simpl in *.
lazymatch goal with
| [ |- ?e0 (?x0', ?x1')%core = _ ]
=> rewrite (IHtx1 x0 _ (fun x0'' => e0 (x0'', x1')%core)); cbv beta in *
end.
lazymatch goal with
| [ |- ?e0 (?x0', ?x1')%core = _ ]
=> rewrite (IHtx2 x1 _ (fun x1'' => e0 (x0', x1'')%core)); cbv beta in *
end.
reflexivity.
Qed.
End mapf_id.
Section mapf_id_interp.
Context {interp_base_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)
(f_var12 f_var21 : forall t, interp_base_type t -> interp_base_type t)
(f_var12_id : forall t x, f_var12 t x = x)
(f_var21_id : forall t x, f_var21 t x = x).
Lemma mapf_idmap {t} e
: interpf interp_op
(@mapf _ _
f_var12 f_var21
t e)
= interpf interp_op e.
Proof using f_var12_id f_var21_id.
induction e;
repeat match goal with
| _ => progress unfold LetIn.Let_In
| _ => reflexivity
| _ => progress simpl in *
| _ => rewrite_hyp !*
| _ => apply (f_equal2 (fun x f => LetIn x f))
| _ => solve [ eauto ]
end.
clear H IHe.
generalize (interpf interp_op e); intro x; clear e.
revert dependent tC; induction tx; simpl;
[ intros; rewrite_hyp ?*; reflexivity | reflexivity | ]; intros.
destruct x as [x0 x1]; simpl in *.
lazymatch goal with
| [ |- interpf _ (?e0 (?x0', ?x1')%core) = _ ]
=> rewrite (IHtx1 x0 _ (fun x0'' => e0 (x0'', x1')%core)); cbv beta in *
end.
lazymatch goal with
| [ |- interpf _ (?e0 (?x0', ?x1')%core) = _ ]
=> apply (IHtx2 x1 _ (fun x1'' => e0 (x0', x1'')%core)); cbv beta in *
end.
Qed.
End mapf_id_interp.
End language.
|
