diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-22 20:08:38 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-22 23:34:43 -0500 |
commit | b8200f3ae9dc13110033ad424eba335632e7a4a1 (patch) | |
tree | 74927204b54234c941186dab36fc3857bbee112e | |
parent | a63973a4e9388a66575c64057e389995e341426d (diff) |
Add lemmas about application
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Reflection/ApplicationLemmas.v | 38 |
2 files changed, 39 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 84d2cbe14..24dbd5005 100644 --- a/_CoqProject +++ b/_CoqProject @@ -95,6 +95,7 @@ src/ModularArithmetic/Montgomery/Z.v src/ModularArithmetic/Montgomery/ZBounded.v src/ModularArithmetic/Montgomery/ZProofs.v src/Reflection/Application.v +src/Reflection/ApplicationLemmas.v src/Reflection/CommonSubexpressionElimination.v src/Reflection/Conversion.v src/Reflection/CountLets.v diff --git a/src/Reflection/ApplicationLemmas.v b/src/Reflection/ApplicationLemmas.v new file mode 100644 index 000000000..aa589f889 --- /dev/null +++ b/src/Reflection/ApplicationLemmas.v @@ -0,0 +1,38 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Application. + +Section language. + Context {base_type : Type} + {interp_base_type : base_type -> Type} + {op : flat_type base_type -> flat_type base_type -> Type} + {interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst}. + + Lemma interp_apply' {n t} + (x : @expr base_type interp_base_type op _ t) + (args : binders_for' n t interp_base_type) + : interp interp_op (Apply' n x args) = ApplyInterped' n (interp interp_op x) args. + Proof. + generalize dependent t; induction n as [|n IHn]; intros. + { destruct x; reflexivity. } + { destruct x as [|?? x]; simpl; [ reflexivity | ]. + apply IHn. } + Qed. + + Lemma interp_apply {n t} + (x : @expr base_type interp_base_type op _ t) + (args : binders_for n t interp_base_type) + : interp interp_op (Apply n x args) = ApplyInterped (interp interp_op x) args. + Proof. + destruct n; [ reflexivity | ]. + apply interp_apply'. + Qed. + + Lemma interp_apply_all {t} + (x : @expr base_type interp_base_type op _ t) + (args : interp_all_binders_for t interp_base_type) + : interp interp_op (ApplyAll x args) = ApplyInterpedAll (interp interp_op x) args. + Proof. + induction x as [|?? x IHx]; [ reflexivity | ]. + simpl; rewrite <- IHx; reflexivity. + Qed. +End language. |