From 920b99a9a1b692fdd1601623071992d7d7869165 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Apr 2017 20:29:11 -0400 Subject: Add correctness of Rewriter --- src/Reflection/RewriterInterp.v | 48 ++++++++++++++++++++++++++++++++ src/Reflection/RewriterWf.v | 61 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 109 insertions(+) create mode 100644 src/Reflection/RewriterInterp.v create mode 100644 src/Reflection/RewriterWf.v (limited to 'src/Reflection') diff --git a/src/Reflection/RewriterInterp.v b/src/Reflection/RewriterInterp.v new file mode 100644 index 000000000..4de516dfd --- /dev/null +++ b/src/Reflection/RewriterInterp.v @@ -0,0 +1,48 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Rewriter. +Require Import Crypto.Util.Tactics.RewriteHyp. + +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 flat_type := (flat_type base_type_code). + Local Notation type := (type base_type_code). + Local Notation interp_type := (interp_type interp_base_type). + Local Notation interp_flat_type := (interp_flat_type interp_base_type). + Local Notation exprf := (@exprf base_type_code op interp_base_type). + Local Notation expr := (@expr base_type_code op interp_base_type). + Local Notation Expr := (@Expr base_type_code op). + + Section specialized. + Context {rewrite_op_expr : forall src dst (opc : op src dst), exprf src -> exprf dst} + (Hrewrite : forall src dst opc args, + interpf interp_op (rewrite_op_expr src dst opc args) + = interp_op _ _ opc (interpf interp_op args)). + + Lemma interpf_rewrite_opf {t} (e : exprf t) + : interpf interp_op (rewrite_opf rewrite_op_expr e) = interpf interp_op e. + Proof. + induction e; simpl; unfold LetIn.Let_In; rewrite_hyp ?*; reflexivity. + Qed. + + Lemma interp_rewrite_op {t} (e : expr t) + : forall x, interp interp_op (rewrite_op rewrite_op_expr e) x = interp interp_op e x. + Proof. + destruct e; intro x; apply interpf_rewrite_opf. + Qed. + End specialized. + + Lemma InterpRewriteOp + {rewrite_op_expr} + (Hrewrite : forall src dst opc args, + interpf interp_op (rewrite_op_expr interp_base_type src dst opc args) + = interp_op _ _ opc (interpf interp_op args)) + {t} (e : Expr t) + : forall x, Interp interp_op (RewriteOp rewrite_op_expr e) x = Interp interp_op e x. + Proof. + apply interp_rewrite_op; assumption. + Qed. +End language. diff --git a/src/Reflection/RewriterWf.v b/src/Reflection/RewriterWf.v new file mode 100644 index 000000000..f44832d29 --- /dev/null +++ b/src/Reflection/RewriterWf.v @@ -0,0 +1,61 @@ +Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Wf. +Require Import Crypto.Reflection.WfInversion. +Require Import Crypto.Reflection.Rewriter. + +Section language. + Context {base_type_code : Type} + {op : flat_type base_type_code -> flat_type base_type_code -> Type}. + + Local Notation flat_type := (flat_type base_type_code). + Local Notation type := (type base_type_code). + Local Notation wff := (@wff base_type_code op). + Local Notation wf := (@wf base_type_code op). + Local Notation Wf := (@Wf base_type_code op). + Local Notation exprf := (@exprf base_type_code op). + Local Notation expr := (@expr base_type_code op). + Local Notation Expr := (@Expr base_type_code op). + + Section with_var. + Context {var1 var2 : base_type_code -> Type} + {rewrite_op_expr1 : forall src dst (opc : op src dst), + exprf (var:=var1) src -> exprf (var:=var1) dst} + {rewrite_op_expr2 : forall src dst (opc : op src dst), + exprf (var:=var2) src -> exprf (var:=var2) dst} + (Hrewrite_wf : forall G src dst opc args1 args2, + wff G args1 args2 + -> wff G + (rewrite_op_expr1 src dst opc args1) + (rewrite_op_expr2 src dst opc args2)). + + Lemma wff_rewrite_opf {t} G (e1 : @exprf var1 t) (e2 : @exprf var2 t) + (Hwf : wff G e1 e2) + : wff G (rewrite_opf rewrite_op_expr1 e1) (rewrite_opf rewrite_op_expr2 e2). + Proof. + induction Hwf; simpl; try constructor; auto. + Qed. + + Lemma wf_rewrite_opf {t} (e1 : @expr var1 t) (e2 : @expr var2 t) + (Hwf : wf e1 e2) + : wf (rewrite_op rewrite_op_expr1 e1) (rewrite_op rewrite_op_expr2 e2). + Proof. + destruct Hwf; simpl; constructor; intros; apply wff_rewrite_opf; auto. + Qed. + End with_var. + + Lemma Wf_InterpRewriteOp + {rewrite_op_expr} + (Hrewrite_wff : forall var1 var2 G src dst opc args1 args2, + wff G args1 args2 + -> wff G + (rewrite_op_expr var1 src dst opc args1) + (rewrite_op_expr var2 src dst opc args2)) + {t} (e : Expr t) + (Hwf : Wf e) + : Wf (RewriteOp rewrite_op_expr e). + Proof. + intros var1 var2; apply wf_rewrite_opf; auto. + Qed. +End language. + +Hint Resolve Wf_InterpRewriteOp : wf. -- cgit v1.2.3