blob: e9cd8737ce952c340aecd9296d1c44e041f847de (
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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.Syntax.
Require Import Crypto.Compilers.Named.Wf.
Require Import Crypto.Util.PointedProp.
Require Import Crypto.Util.Tactics.BreakMatch.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.DestructHead.
Section language.
Context {base_type_code Name interp_base_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}
{Context : @Context base_type_code Name interp_base_type}.
Lemma wff_interpf_not_None {ctx : Context} {t} {e : @exprf base_type_code op Name t}
(Hwf : prop_of_option (wff ctx e))
: @interpf base_type_code interp_base_type op Name Context interp_op t ctx e <> None.
Proof using Type.
revert dependent ctx; induction e;
repeat first [ progress intros
| progress simpl in *
| progress unfold option_map, LetIn.Let_In in *
| congruence
| progress specialize_by_assumption
| progress destruct_head' and
| progress break_innermost_match_step
| progress break_match_hyps
| progress autorewrite with push_prop_of_option in *
| progress specialize_by auto
| solve [ intuition eauto ] ].
Qed.
Lemma wf_interp_not_None {ctx : Context} {t} {e : @expr base_type_code op Name t}
(Hwf : wf ctx e)
v
: @interp base_type_code interp_base_type op Name Context interp_op t ctx e v <> None.
Proof using Type.
destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto.
Qed.
End language.
|
