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/Compilers/Z/ArithmeticSimplifierWf.v | |
parent | 21198245dab432d3c0ba2bb8a02254e7d0594382 (diff) |
rename-everything
Diffstat (limited to 'src/Compilers/Z/ArithmeticSimplifierWf.v')
-rw-r--r-- | src/Compilers/Z/ArithmeticSimplifierWf.v | 168 |
1 files changed, 168 insertions, 0 deletions
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v new file mode 100644 index 000000000..24a9b4d23 --- /dev/null +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -0,0 +1,168 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.WfInversion. +Require Import Crypto.Compilers.TypeInversion. +Require Import Crypto.Compilers.ExprInversion. +Require Import Crypto.Compilers.RewriterWf. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.OpInversion. +Require Import Crypto.Compilers.Z.ArithmeticSimplifier. +Require Import Crypto.Compilers.Z.Syntax.Equality. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Sum. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.HProp. + +Local Notation exprf := (@exprf base_type op). +Local Notation expr := (@expr base_type op). +Local Notation Expr := (@Expr base_type op). +Local Notation wff := (@wff base_type op). +Local Notation Wf := (@Wf base_type op). + +Local Ltac fin_t := + first [ exact I + | reflexivity + | congruence + | assumption + | exfalso; assumption ]. +Local Ltac break_t_step := + first [ progress subst + | progress inversion_option + | progress inversion_sum + | progress inversion_expr + | progress inversion_prod + | progress invert_op + | progress inversion_flat_type + | progress destruct_head'_and + | progress destruct_head' iff + | progress destruct_head'_prod + | progress destruct_head'_sig + | progress specialize_by reflexivity + | progress eliminate_hprop_eq + | progress break_innermost_match_step + | progress break_match_hyps + | progress inversion_wf_constr ]. + + +Lemma interp_as_expr_or_const_None_iff {var1 var2 t} {G e1 e2} + (Hwf : @wff var1 var2 G t e1 e2) + : @interp_as_expr_or_const var1 t e1 = None + <-> @interp_as_expr_or_const var2 t e2 = None. +Proof. + induction Hwf; + repeat first [ fin_t + | split; congruence + | progress simpl in * + | progress intros + | break_t_step ]. +Qed. + +Lemma interp_as_expr_or_const_None_Some {var1 var2 t} {G e1 e2 v} + (Hwf : @wff var1 var2 G t e1 e2) + : @interp_as_expr_or_const var1 t e1 = None + -> @interp_as_expr_or_const var2 t e2 = Some v + -> False. +Proof. + erewrite interp_as_expr_or_const_None_iff by eassumption; congruence. +Qed. + +Lemma interp_as_expr_or_const_Some_None {var1 var2 t} {G e1 e2 v} + (Hwf : @wff var1 var2 G t e1 e2) + : @interp_as_expr_or_const var1 t e1 = Some v + -> @interp_as_expr_or_const var2 t e2 = None + -> False. +Proof. + erewrite <- interp_as_expr_or_const_None_iff by eassumption; congruence. +Qed. + +Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2} + (Hwf : @wff var1 var2 G (Tbase t) e1 e2) + : @interp_as_expr_or_const var1 (Tbase t) e1 = Some v1 + -> @interp_as_expr_or_const var2 (Tbase t) e2 = Some v2 + -> match v1, v2 with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end. +Proof. + invert_one_expr e1; intros; break_innermost_match; intros; + try invert_one_expr e2; intros; + repeat first [ fin_t + | progress simpl in * + | progress intros + | break_t_step + | match goal with + | [ H : wff _ _ ?e |- _ ] => is_var e; invert_one_expr e + end ]. +Qed. + +Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ * _} + (Hwf : wff G e1 e2) + : @interp_as_expr_or_const var1 (Prod (Tbase A) (Tbase B)) e1 = Some v1 + -> @interp_as_expr_or_const var2 (Prod (Tbase A) (Tbase B)) e2 = Some v2 + -> match fst v1, fst v2 with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end + /\ match snd v1, snd v2 with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end. +Proof. + invert_one_expr e1; intros; break_innermost_match; intros; try exact I; + try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; + repeat first [ fin_t + | progress simpl in * + | break_t_step + | match goal with + | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2 + | [ |- and _ _ ] => split + end ]. +Qed. + +Lemma Wf_SimplifyArith {t} (e : Expr t) + (Hwf : Wf e) + : Wf (SimplifyArith e). +Proof. + apply Wf_RewriteOp; [ | assumption ]. + intros ???????? Hwf'; unfold simplify_op_expr; + break_innermost_match; repeat constructor; auto; + repeat first [ fin_t + | progress simpl in * + | progress subst + | progress Z.ltb_to_lt + | match goal with + | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2 + | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2 + | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ] + => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2 + | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2 + | [ |- wff _ _ _ ] => constructor + end + | break_t_step ]. +Qed. |