blob: e8105c2f0e275bcf2878f0474fe4db544f806b79 (
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
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Application.
Section language.
Context {base_type : Type}
{interp_base_type : base_type -> Type}
{op : flat_type base_type -> flat_type base_type -> Type}
{interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}.
Lemma interp_apply' {n t}
(x : @expr base_type op _ t)
(args : binders_for' n t interp_base_type)
: interp interp_op (Apply' n x args) = ApplyInterped' n (interp interp_op x) args.
Proof.
generalize dependent t; induction n as [|n IHn]; intros.
{ destruct x; reflexivity. }
{ destruct x as [|?? x]; simpl; [ reflexivity | ].
apply IHn. }
Qed.
Lemma interp_apply {n t}
(x : @expr base_type op _ t)
(args : binders_for n t interp_base_type)
: interp interp_op (Apply n x args) = ApplyInterped (interp interp_op x) args.
Proof.
destruct n; [ reflexivity | ].
apply interp_apply'.
Qed.
Lemma fst_interp_all_binders_for_of' {A B}
(args : interp_all_binders_for' (Arrow A B) interp_base_type)
: fst_binder (interp_all_binders_for_of' args) = fst args.
Proof.
destruct B; reflexivity.
Qed.
Lemma snd_interp_all_binders_for_of' {A B}
(args : interp_all_binders_for' (Arrow A B) interp_base_type)
: snd_binder (interp_all_binders_for_of' args) = interp_all_binders_for_of' (snd args).
Proof.
destruct B.
{ destruct args as [? []]; reflexivity. }
{ destruct args; reflexivity. }
Qed.
Lemma fst_interp_all_binders_for_to' {A B}
(args : interp_all_binders_for (Arrow A B) interp_base_type)
: fst (interp_all_binders_for_to' args) = fst_binder args.
Proof.
destruct B; reflexivity.
Qed.
Lemma snd_interp_all_binders_for_to' {A B}
(args : interp_all_binders_for (Arrow A B) interp_base_type)
: snd (interp_all_binders_for_to' args) = interp_all_binders_for_to' (snd_binder args).
Proof.
destruct B; reflexivity.
Qed.
Lemma interp_all_binders_for_to'_of' {t} (args : interp_all_binders_for' t interp_base_type)
: interp_all_binders_for_to' (interp_all_binders_for_of' args) = args.
Proof.
induction t; destruct args; [ reflexivity | ].
apply injective_projections;
[ rewrite fst_interp_all_binders_for_to', fst_interp_all_binders_for_of'; reflexivity
| rewrite snd_interp_all_binders_for_to', snd_interp_all_binders_for_of', IHt; reflexivity ].
Qed.
Lemma interp_all_binders_for_of'_to' {t} (args : interp_all_binders_for t interp_base_type)
: interp_all_binders_for_of' (interp_all_binders_for_to' args) = args.
Proof.
induction t as [|A B IHt].
{ destruct args; reflexivity. }
{ destruct B; [ reflexivity | ].
destruct args; simpl; rewrite IHt; reflexivity. }
Qed.
Lemma interp_apply_all' {t}
(x : @expr base_type op _ t)
(args : interp_all_binders_for' t interp_base_type)
: interp interp_op (ApplyAll x (interp_all_binders_for_of' args)) = ApplyInterpedAll' (interp interp_op x) args.
Proof.
induction x as [|?? x IHx]; [ reflexivity | ].
simpl; rewrite <- IHx; destruct args.
rewrite snd_interp_all_binders_for_of', fst_interp_all_binders_for_of'; reflexivity.
Qed.
Lemma interp_apply_all {t}
(x : @expr base_type op _ t)
(args : interp_all_binders_for t interp_base_type)
: interp interp_op (ApplyAll x args) = ApplyInterpedAll (interp interp_op x) args.
Proof.
unfold ApplyInterpedAll.
rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity.
Qed.
Lemma interp_apply_all_to' {t}
(x : @expr base_type op _ t)
(args : interp_all_binders_for t interp_base_type)
: interp interp_op (ApplyAll x args) = ApplyInterpedAll' (interp interp_op x) (interp_all_binders_for_to' args).
Proof.
rewrite <- interp_apply_all', interp_all_binders_for_of'_to'; reflexivity.
Qed.
End language.
|
