blob: 5790178e72186eaba0cb5be79da7a421147cf68e (
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
|
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Util.Tactics.
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_gen interp_base_type.
Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
Lemma interpf_SmartVar t v
: Syntax.interpf base_type_code interp_base_type op interp_op (SmartVar (t:=t) v) = v.
Proof.
unfold SmartVar; induction t;
repeat match goal with
| _ => reflexivity
| _ => progress simpl in *
| _ => progress rewrite_hyp *
| _ => rewrite <- surjective_pairing
end.
Qed.
End language.
|
