diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-21 21:35:15 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-02-21 21:35:15 -0500 |
| commit | 57a0a97fdbeee2954128d0917d534a7ed8c433cb (patch) | |
| tree | 14a267c94f5381965d02db5c45461e2283158e27 /src/Reflection/EtaInterp.v | |
| parent | 371ba4b6eb769d3a9a4518df5d4063cf57a6396b (diff) | |
Add various reflection improvements, boundbycast
Diffstat (limited to 'src/Reflection/EtaInterp.v')
| -rw-r--r-- | src/Reflection/EtaInterp.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v index 95732ad3d..54240947a 100644 --- a/src/Reflection/EtaInterp.v +++ b/src/Reflection/EtaInterp.v @@ -1,5 +1,6 @@ Require Import Crypto.Reflection.Syntax. Require Import Crypto.Reflection.Eta. +Require Import Crypto.Reflection.Relations. Require Import Crypto.Reflection.ExprInversion. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. @@ -37,11 +38,31 @@ Section language. (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen. + Section gen_type. + Context (exprf_eta : forall {t} (e : exprf t), exprf t) + (eq_interp_exprf_eta : forall t e, interpf (@interp_op) (@exprf_eta t e) = interpf (@interp_op) e). + Lemma interp_expr_eta_gen {t e} + : interp_type_gen_rel_pointwise + (fun _ => eq) + (interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e)) + (interp (@interp_op) e). + Proof. t. Admitted. + End gen_type. + (* Local *) Hint Rewrite @interp_expr_eta_gen. + Lemma interpf_exprf_eta_gen {t e} : interpf (@interp_op) (exprf_eta_gen eta (t:=t) e) = interpf (@interp_op) e. Proof. induction e; t. Qed. + + Lemma InterpExprEtaGen {t e} + : interp_type_gen_rel_pointwise + (fun _ => eq) + (Interp (@interp_op) (ExprEtaGen eta (t:=t) e)) + (Interp (@interp_op) e). + Proof. apply interp_expr_eta_gen; intros; apply interpf_exprf_eta_gen. Qed. End gen_flat_type. (* Local *) Hint Rewrite @eq_interp_flat_type_eta_gen. + (* Local *) Hint Rewrite @interp_expr_eta_gen. (* Local *) Hint Rewrite @interpf_exprf_eta_gen. Lemma eq_interp_flat_type_eta {var t T f} x @@ -60,4 +81,16 @@ Section language. : interpf (@interp_op) (exprf_eta' (t:=t) e) = interpf (@interp_op) e. Proof. t. Qed. (* Local *) Hint Rewrite @interpf_exprf_eta'. + Lemma interp_expr_eta {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (interp (@interp_op) (expr_eta (t:=t) e)) (interp (@interp_op) e). + Proof. t. Qed. + Lemma interp_expr_eta' {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (interp (@interp_op) (expr_eta' (t:=t) e)) (interp (@interp_op) e). + Proof. t. Qed. + Lemma InterpExprEta {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (Interp (@interp_op) (ExprEta (t:=t) e)) (Interp (@interp_op) e). + Proof. apply interp_expr_eta. Qed. + Lemma InterpExprEta' {t e} + : interp_type_gen_rel_pointwise (fun _ => eq) (Interp (@interp_op) (ExprEta' (t:=t) e)) (Interp (@interp_op) e). + Proof. apply interp_expr_eta'. Qed. End language. |