diff options
author | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2017-04-06 22:53:07 -0400 |
commit | c9fc5a3cdf1f5ea2d104c150c30d1b1a6ac64239 (patch) | |
tree | db7187f6984acff324ca468e7b33d9285806a1eb /src/Reflection/EtaInterp.v | |
parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) |
rename-everything
Diffstat (limited to 'src/Reflection/EtaInterp.v')
-rw-r--r-- | src/Reflection/EtaInterp.v | 105 |
1 files changed, 0 insertions, 105 deletions
diff --git a/src/Reflection/EtaInterp.v b/src/Reflection/EtaInterp.v deleted file mode 100644 index deb551d7d..000000000 --- a/src/Reflection/EtaInterp.v +++ /dev/null @@ -1,105 +0,0 @@ -Require Import Crypto.Reflection.Syntax. -Require Import Crypto.Reflection.Eta. -Require Import Crypto.Reflection.ExprInversion. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.DestructHead. - -Section language. - Context {base_type_code : Type} - {interp_base_type : base_type_code -> 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}. - - Local Notation exprf := (@exprf base_type_code op interp_base_type). - - Local Ltac t_step := - match goal with - | _ => reflexivity - | _ => progress simpl in * - | _ => intro - | _ => progress break_match - | _ => progress destruct_head prod - | _ => progress cbv [LetIn.Let_In] - | [ H : _ |- _ ] => rewrite H - | _ => progress autorewrite with core - | [ H : forall A B x, ?f A B x = x, H' : context[?f _ _ _] |- _ ] - => rewrite H in H' - | _ => progress unfold interp_flat_type_eta, interp_flat_type_eta', exprf_eta, exprf_eta', expr_eta, expr_eta' - end. - Local Ltac t := repeat t_step. - - Section gen_flat_type. - Context (eta : forall {A B}, A * B -> A * B) - (eq_eta : forall A B x, @eta A B x = x). - Lemma eq_interp_flat_type_eta_gen {var t T f} x - : @interp_flat_type_eta_gen base_type_code var eta t T f x = f x. - Proof using eq_eta. induction t; t. Qed. - - (* 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} - : forall x, - interp (@interp_op) (expr_eta_gen eta exprf_eta (t:=t) e) x = interp (@interp_op) e x. - Proof using Type*. t. Qed. - 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 using eq_eta. induction e; t. Qed. - - Lemma InterpExprEtaGen {t e} - : forall x, Interp (@interp_op) (ExprEtaGen eta (t:=t) e) x = Interp (@interp_op) e x. - Proof using eq_eta. 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 - : @interp_flat_type_eta base_type_code var t T f x = f x. - Proof using Type. t. Qed. - (* Local *) Hint Rewrite @eq_interp_flat_type_eta. - Lemma eq_interp_flat_type_eta' {var t T f} x - : @interp_flat_type_eta' base_type_code var t T f x = f x. - Proof using Type. t. Qed. - (* Local *) Hint Rewrite @eq_interp_flat_type_eta'. - Lemma interpf_exprf_eta {t e} - : interpf (@interp_op) (exprf_eta (t:=t) e) = interpf (@interp_op) e. - Proof using Type. t. Qed. - (* Local *) Hint Rewrite @interpf_exprf_eta. - Lemma interpf_exprf_eta' {t e} - : interpf (@interp_op) (exprf_eta' (t:=t) e) = interpf (@interp_op) e. - Proof using Type. t. Qed. - (* Local *) Hint Rewrite @interpf_exprf_eta'. - Lemma interp_expr_eta {t e} - : forall x, interp (@interp_op) (expr_eta (t:=t) e) x = interp (@interp_op) e x. - Proof using Type. t. Qed. - Lemma interp_expr_eta' {t e} - : forall x, interp (@interp_op) (expr_eta' (t:=t) e) x = interp (@interp_op) e x. - Proof using Type. t. Qed. - Lemma InterpExprEta {t e} - : forall x, Interp (@interp_op) (ExprEta (t:=t) e) x = Interp (@interp_op) e x. - Proof using Type. apply interp_expr_eta. Qed. - Lemma InterpExprEta' {t e} - : forall x, Interp (@interp_op) (ExprEta' (t:=t) e) x = Interp (@interp_op) e x. - Proof using Type. apply interp_expr_eta'. Qed. - Lemma InterpExprEta_arrow {s d e} - : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x = Interp (@interp_op) e x. - Proof using Type. exact (@InterpExprEta (Arrow s d) e). Qed. - Lemma InterpExprEta'_arrow {s d e} - : forall x, Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x = Interp (@interp_op) e x. - Proof using Type. exact (@InterpExprEta' (Arrow s d) e). Qed. - - Lemma eq_interp_eta {t e} - : forall x, interp_eta interp_op (t:=t) e x = interp interp_op e x. - Proof using Type. apply eq_interp_flat_type_eta. Qed. - Lemma eq_InterpEta {t e} - : forall x, InterpEta interp_op (t:=t) e x = Interp interp_op e x. - Proof using Type. apply eq_interp_eta. Qed. -End language. - -Hint Rewrite @eq_interp_flat_type_eta @eq_interp_flat_type_eta' @interpf_exprf_eta @interpf_exprf_eta' @interp_expr_eta @interp_expr_eta' @InterpExprEta @InterpExprEta' @InterpExprEta_arrow @InterpExprEta'_arrow @eq_interp_eta @eq_InterpEta : reflective_interp. |