blob: c26c1c3ce9774ae8af3b2ec3e1ed13e97a061c5e (
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
|
Require Import Coq.Strings.String Coq.Classes.RelationClasses.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.Relations.
Require Import Crypto.Util.Tuple.
Require Import Crypto.Util.Sigma.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.Tactics.
Require Import Crypto.Util.Notations.
Local Open Scope ctype_scope.
Local Open Scope expr_scope.
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 Notation expr := (@expr base_type_code op interp_base_type).
Local Notation Expr := (@Expr base_type_code op).
Local Notation interpf := (@interpf base_type_code interp_base_type op interp_op).
Local Notation interp := (@interp base_type_code interp_base_type op interp_op).
Local Notation Interp := (@Interp base_type_code interp_base_type op interp_op).
Lemma eq_in_flatten_binding_list
{t x x' T e}
(HIn : List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core)
(flatten_binding_list base_type_code (t:=T) e e))
: x = x'.
Proof.
induction T; simpl in *; [ | | rewrite List.in_app_iff in HIn ];
repeat first [ progress destruct_head or
| progress destruct_head False
| progress destruct_head and
| progress inversion_sigma
| progress inversion_prod
| progress subst
| solve [ eauto ] ].
Qed.
Local Hint Resolve List.in_app_or List.in_or_app eq_in_flatten_binding_list.
Section wf.
Lemma interpf_wff
{t} {e1 e2 : exprf t}
{G}
(HG : forall t x x',
List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) G
-> x = x')
(Rwf : wff G e1 e2)
: interpf e1 = interpf e2.
Proof.
induction Rwf; simpl; auto;
specialize_by auto; try congruence.
rewrite_hyp !*; auto.
repeat match goal with
| [ H : context[List.In _ (_ ++ _)] |- _ ]
=> setoid_rewrite List.in_app_iff in H
end.
match goal with
| [ H : _ |- _ ]
=> apply H; intros; destruct_head' or; solve [ eauto ]
end.
Qed.
Local Hint Resolve interpf_wff.
Lemma interp_wf
{t} {e1 e2 : expr t}
{G}
(HG : forall t x x',
List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) G
-> x = x')
(Rwf : wf G e1 e2)
: interp_type_gen_rel_pointwise (fun _ => eq) (interp e1) (interp e2).
Proof.
induction Rwf; simpl; repeat intro; simpl in *; subst; eauto.
match goal with
| [ H : _ |- _ ]
=> apply H; intros; progress destruct_head' or; [ | solve [ eauto ] ]
end.
inversion_sigma; inversion_prod; repeat subst; simpl; auto.
Qed.
End wf.
End language.
|
