blob: 72bb9c9e036eded93de3dbe371ef318a59af2b41 (
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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Named.Syntax.
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.InterpSideConditions.
Require Import Crypto.Util.PointedProp.
Require Import Crypto.Util.Notations.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Option.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
{Name : Type}
{interp_base_type : base_type_code -> Type}
{Context : Context Name interp_base_type}
{interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
{interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop}.
Local Notation exprf := (@exprf base_type_code op Name).
Local Notation expr := (@expr base_type_code op Name).
Lemma snd_interpf_side_conditions_gen_eq {t} {ctx : Context} {e}
: interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e
= option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e).
Proof.
revert ctx; induction e; intros;
repeat first [ reflexivity
| progress subst
| progress inversion_option
| progress unfold option_map, LetIn.Let_In in *
| break_innermost_match_step
| break_innermost_match_hyps_step
| progress simpl in *
| match goal with
| [ H : forall ctx, interpf ?e = _, H' : context[interpf ?e] |- _ ]
=> rewrite H in H'
| [ H : forall ctx, interpf ?e = _ |- context[interpf ?e] ]
=> rewrite H
end ].
Qed.
Lemma snd_interpf_side_conditions_gen_Some {t} {ctx : Context} {e v}
: interpf (t:=t) (ctx:=ctx) (interp_op:=interp_op) e = Some v
<-> option_map (@snd _ _) (interpf_side_conditions_gen interp_op interped_op_side_conditions ctx e) = Some v.
Proof. rewrite snd_interpf_side_conditions_gen_eq; reflexivity. Qed.
End language.
|
