diff options
Diffstat (limited to 'src/Compilers/EtaInterp.v')
| -rw-r--r-- | src/Compilers/EtaInterp.v | 118 |
1 files changed, 0 insertions, 118 deletions
diff --git a/src/Compilers/EtaInterp.v b/src/Compilers/EtaInterp.v deleted file mode 100644 index 2b6bd9b86..000000000 --- a/src/Compilers/EtaInterp.v +++ /dev/null @@ -1,118 +0,0 @@ -Require Import Crypto.Compilers.Syntax. -Require Import Crypto.Compilers.Eta. -Require Import Crypto.Compilers.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 InterpExprEta_ind {t} (P : _ -> Prop) {e x} - : P (Interp (@interp_op) e x) -> P (Interp (@interp_op) (ExprEta (t:=t) e) x). - Proof using Type. rewrite InterpExprEta; exact id. Qed. - Lemma InterpExprEta'_ind {t} (P : _ -> Prop) {e x} - : P (Interp (@interp_op) e x) -> P (Interp (@interp_op) (ExprEta' (t:=t) e) x). - Proof using Type. rewrite InterpExprEta'; exact id. Qed. - Lemma InterpExprEta_arrow_ind {s d} (P : _ -> Prop) {e x} - : P (Interp (@interp_op) e x) -> P (Interp (t:=Arrow s d) (@interp_op) (ExprEta (t:=Arrow s d) e) x). - Proof using Type. rewrite InterpExprEta_arrow; exact id. Qed. - Lemma InterpExprEta'_arrow_ind {s d} (P : _ -> Prop) {e x} - : P (Interp (@interp_op) e x) -> P (Interp (t:=Arrow s d) (@interp_op) (ExprEta' (t:=Arrow s d) e) x). - Proof using Type. rewrite InterpExprEta'_arrow; exact id. 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. |