diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-14 13:16:25 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-14 13:16:25 -0400 |
commit | 8c8a223fc8b4ddae385f79c700b2983bbf794862 (patch) | |
tree | f7062dee220d069b612addccb136421f63654135 | |
parent | feb04cf2e22e4924219d147dd23154692046220a (diff) |
Add lemma about wff and interpf of Named
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Reflection/Named/WfInterp.v | 41 |
2 files changed, 42 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 6602f9b54..4a5583bba 100644 --- a/_CoqProject +++ b/_CoqProject @@ -162,6 +162,7 @@ src/Reflection/Named/RegisterAssign.v src/Reflection/Named/SmartMap.v src/Reflection/Named/Syntax.v src/Reflection/Named/Wf.v +src/Reflection/Named/WfInterp.v src/Reflection/Z/BinaryNotationConstants.v src/Reflection/Z/BoundsInterpretations.v src/Reflection/Z/CNotations.v diff --git a/src/Reflection/Named/WfInterp.v b/src/Reflection/Named/WfInterp.v new file mode 100644 index 000000000..b8cfb7fbe --- /dev/null +++ b/src/Reflection/Named/WfInterp.v @@ -0,0 +1,41 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Named.Syntax. +Require Import Crypto.Reflection.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} + {ContextOk : ContextOk Context}. + + 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 ctx t e <> None. + Proof. + 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 ctx t e v <> None. + Proof. + destruct e; unfold interp, wf in *; apply wff_interpf_not_None; auto. + Qed. +End language. |