blob: 4e49050b0a53f435dec0dd7a51e8f52548e30a33 (
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
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.WfProofs.
Require Import Crypto.Util.LetIn.
Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
Local Open Scope ctype_scope.
Section language.
Context (base_type_code : Type).
Local Notation flat_type := (flat_type base_type_code).
Local Notation type := (type base_type_code).
Let Tbase := @Tbase base_type_code.
Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
Context (interp_base_type : base_type_code -> Type).
Context (op : flat_type (* input tuple *) -> flat_type (* output type *) -> Type).
Let interp_type := interp_type interp_base_type.
Let interp_flat_type := interp_flat_type interp_base_type.
Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
Lemma interpf_LetIn tx ex tC eC
: Syntax.interpf interp_op (LetIn (tx:=tx) ex (tC:=tC) eC)
= dlet x := Syntax.interpf interp_op ex in
Syntax.interpf interp_op (eC x).
Proof. reflexivity. Qed.
Lemma interpf_SmartVarf t v
: Syntax.interpf interp_op (SmartVarf (t:=t) v) = v.
Proof.
unfold SmartVarf; induction t;
repeat match goal with
| _ => reflexivity
| _ => progress simpl in *
| _ => progress rewrite_hyp *
| _ => rewrite <- surjective_pairing
end.
Qed.
Lemma interpf_SmartConstf {t t'} v x x'
(Hin : List.In
(existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
t (x, x'))
(flatten_binding_list (t := t') base_type_code (SmartConstf v) v))
: interpf interp_op x = x'.
Proof.
clear -Hin.
induction t'; simpl in *.
{ intuition (inversion_sigma; inversion_prod; subst; eauto). }
{ apply List.in_app_iff in Hin.
intuition (inversion_sigma; inversion_prod; subst; eauto). }
Qed.
Lemma interpf_SmartVarVarf {t t'} v x x'
(Hin : List.In
(existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
t (x, x'))
(flatten_binding_list (t := t') base_type_code (SmartVarVarf v) v))
: interpf interp_op x = x'.
Proof.
clear -Hin.
induction t'; simpl in *.
{ intuition (inversion_sigma; inversion_prod; subst; eauto). }
{ apply List.in_app_iff in Hin.
intuition (inversion_sigma; inversion_prod; subst; eauto). }
Qed.
Lemma interpf_SmartVarVarf_eq {t t'} v v' x x'
(Heq : v = v')
(Hin : List.In
(existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
t (x, x'))
(flatten_binding_list (t := t') base_type_code (SmartVarVarf v') v))
: interpf interp_op x = x'.
Proof.
subst; eapply interpf_SmartVarVarf; eassumption.
Qed.
End language.
|