aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v')
-rw-r--r--src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v197
1 files changed, 0 insertions, 197 deletions
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
deleted file mode 100644
index 6486b2e00..000000000
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v
+++ /dev/null
@@ -1,197 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Psatz.
-Require Import Crypto.Compilers.Z.Bounds.Interpretation.
-Require Import Crypto.Util.ZUtil.Hints.
-Require Import Crypto.Util.ZUtil.Hints.Core.
-Require Import Crypto.Util.ZUtil.ZSimplify.Core.
-Require Import Crypto.Util.ZUtil.Log2.
-Require Import Crypto.Util.ZUtil.Shift.
-Require Import Crypto.Util.ZUtil.LandLorShiftBounds.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Notations.
-Require Import Crypto.Util.ZRange.Operations.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.FixedWordSizesEquality.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Tactics.SpecializeBy.
-Require Import Crypto.Util.Tactics.SplitInContext.
-Require Import Crypto.Util.Tactics.UniquePose.
-Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax.
-
-Local Open Scope Z_scope.
-
-Ltac break_t_step :=
- first [ progress destruct_head'_and
- | progress destruct_head'_or
- | progress destruct_head'_prod
- | progress split_andb
- | break_innermost_match_step ].
-
-Ltac fin_t :=
- first [ reflexivity
- | assumption
- | match goal with
- | [ |- and _ _ ]
- => first [ split; [ | solve [ fin_t ] ]
- | split; [ solve [ fin_t ] | ] ];
- try solve [ fin_t ]
- end
- | omega ].
-
-Ltac specializer_t_step :=
- first [ progress specialize_by_assumption
- | progress specialize_by fin_t ].
-
-Ltac Zarith_t_step :=
- first [ match goal with
- | [ H : (?x <= ?y)%Z, H' : (?y <= ?x)%Z |- _ ]
- => assert (x = y) by omega; clear H H'
- end
- | progress Z.ltb_to_lt_in_context ].
-Ltac Zarith_land_lor_t_step :=
- match goal with
- | [ |- _ <= Z.lor _ _ <= _ ]
- => split; etransitivity; [ | apply Z.lor_bounds; omega | apply Z.lor_bounds; omega | ]
- | [ |- 2^Z.log2_up (?x + 1) - 1 <= 2^Z.log2_up (?y + 1) - 1 ]
- => let H := fresh in assert (H : x <= y) by omega; rewrite H; reflexivity
- end.
-Ltac word_arith_t :=
- match goal with
- | [ |- (0 <= FixedWordSizes.wordToZ ?w <= 2^2^Z.of_nat ?logsz - 1)%Z ]
- => clear; pose proof (@wordToZ_range logsz w); autorewrite with push_Zof_nat zsimplify_const in *; try omega
- end.
-
-Ltac case_Zvar_nonneg_on x :=
- is_var x;
- lazymatch type of x with
- | Z => lazymatch goal with
- | [ H : (0 <= x)%Z |- _ ] => fail
- | [ H : (x < 0)%Z |- _ ] => fail
- | _ => destruct (Z_lt_le_dec x 0); try omega
- end
- end.
-Ltac case_Zvar_nonneg_step :=
- match goal with
- | [ |- context[?x] ]
- => case_Zvar_nonneg_on x
- end.
-Ltac case_Zvar_nonneg := repeat case_Zvar_nonneg_step.
-
-Ltac remove_binary_operation_le_hyps_step :=
- match goal with
- | [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ]
- => assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia);
- clear H
- | [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ]
- => assert ((y = y') \/ (y < y' /\ 0 <= x))%Z by (assert (y <= y')%Z by omega; nia);
- clear H
- | [ H : (?f ?x ?y <= ?f ?x ?y')%Z |- _ ]
- => assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia);
- clear H
- | [ H : (?f ?y ?x <= ?f ?y' ?x)%Z |- _ ]
- => assert ((y = y') \/ (y' < y /\ x <= 0))%Z by (assert (y' <= y)%Z by omega; nia);
- clear H
- | [ H : ?T, H' : ?T |- _ ] => clear H'
- | [ H : ?A \/ (~?A /\ ?B), H' : ?A \/ (~?A /\ ?C) |- _ ]
- => assert (A \/ (~A /\ (B /\ C))) by (clear -H H'; tauto); clear H H'
- | _ => progress destruct_head' or; destruct_head' and; subst; try omega
- | [ |- (_ <= _ <= _)%Z ] => split
- | _ => case_Zvar_nonneg_step
- end.
-
-Ltac saturate_with_shift_facts :=
- repeat match goal with
- | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x << ?x'] ]
- => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
- | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y << ?y'] ]
- => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
- | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?x >> ?y'] ]
- => unique assert (x >> y' <= y >> x') by (Z.shiftr_le_mono; omega)
- | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[?y >> ?x'] ]
- => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega)
- end.
-Ltac saturate_with_all_shift_facts :=
- repeat match goal with
- | _ => progress saturate_with_shift_facts
- | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftl _ _] ]
- => unique assert (x << x' <= y << y') by (apply Z.shiftl_le_mono; omega)
- | [ H : ?x <= ?y, H' : ?x' <= ?y' |- context[Z.shiftr _ _] ]
- => unique assert (x >> y' <= y >> x') by (apply Z.shiftr_le_mono; omega)
- end.
-Ltac preprocess_shift_min_max :=
- repeat first [ rewrite (Z.min_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
- | rewrite (Z.min_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
- | rewrite (Z.max_r (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
- | rewrite (Z.max_l (_ >> _) (_ >> _)) by (apply Z.shiftr_le_mono; omega)
- | rewrite (Z.min_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
- | rewrite (Z.min_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
- | rewrite (Z.max_r (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega)
- | rewrite (Z.max_l (_ << _) (_ << _)) by (apply Z.shiftl_le_mono; omega) ].
-Ltac saturate_land_lor_facts :=
- repeat match goal with
- | [ |- context[Z.land ?x ?y] ]
- => let H := fresh in
- let H' := fresh in
- assert (H : 0 <= x) by omega;
- assert (H' : 0 <= y) by omega;
- unique pose proof (Z.land_upper_bound_r x y H H');
- unique pose proof (Z.land_upper_bound_l x y H H')
- | [ |- context[Z.land ?x ?y] ]
- => unique assert (0 <= Z.land x y) by (apply Z.land_nonneg; omega)
- | [ |- context[Z.land ?x ?y] ]
- => case_Zvar_nonneg_on x; case_Zvar_nonneg_on y
- | [ |- context[Z.lor ?x ?y] ]
- => let H := fresh in
- let H' := fresh in
- assert (H : 0 <= x) by omega;
- assert (H' : 0 <= y) by omega;
- unique pose proof (proj1 (Z.lor_bounds x y H H'));
- unique pose proof (proj2 (Z.lor_bounds x y H H'))
- | [ |- context[Z.lor ?x ?y] ]
- => unique assert (0 <= Z.lor x y) by (apply Z.lor_nonneg; omega)
- | [ |- context[Z.lor ?x ?y] ]
- => case_Zvar_nonneg_on x; case_Zvar_nonneg_on y
- end.
-Ltac handle_shift_neg :=
- repeat first [ rewrite !Z.shiftr_opp_r
- | rewrite !Z.shiftl_opp_r
- | rewrite !Z.shiftr_opp_l
- | rewrite !Z.shiftl_opp_l ].
-
-Ltac handle_four_corners_step_fast :=
- first [ progress destruct_head Bounds.t
- | progress cbv [ZRange.four_corners] in *
- | progress subst
- | Zarith_t_step
- | progress split_min_max
- | omega
- | nia ].
-Ltac handle_four_corners_step :=
- first [ handle_four_corners_step_fast
- | remove_binary_operation_le_hyps_step ].
-Ltac handle_four_corners :=
- lazymatch goal with
- | [ |- (ZRange.lower (ZRange.four_corners _ _ _) <= _ <= _)%Z ]
- => idtac
- end;
- repeat handle_four_corners_step.
-
-Ltac rewriter_t :=
- first [ rewrite !Bool.andb_true_iff
- | rewrite !Bool.andb_false_iff
- | rewrite !Bool.orb_true_iff
- | rewrite !Bool.orb_false_iff
- | rewrite !Z.abs_opp
- | rewrite !Z.max_log2_up
- | rewrite !Z.add_max_distr_r
- | rewrite !Z.add_max_distr_l
- | rewrite wordToZ_ZToWord by (autorewrite with push_Zof_nat zsimplify_const; omega)
- | match goal with
- | [ H : _ |- _ ]
- => first [ rewrite !Bool.andb_true_iff in H
- | rewrite !Bool.andb_false_iff in H
- | rewrite !Bool.orb_true_iff in H
- | rewrite !Bool.orb_false_iff in H ]
- end ].
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 18:05:30 +0000