From d18c285997255051579ff4d3d761cdeb8a4ec75b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 11 Nov 2017 00:56:52 -0500 Subject: First intro and split in Zring_prod_eq_tac, before cbv - --- src/Util/SideConditions/RingPackage.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/Util/SideConditions') diff --git a/src/Util/SideConditions/RingPackage.v b/src/Util/SideConditions/RingPackage.v index f979b77ba..ef01dd069 100644 --- a/src/Util/SideConditions/RingPackage.v +++ b/src/Util/SideConditions/RingPackage.v @@ -6,15 +6,22 @@ Require Export Crypto.Util.FixCoqMistakes. Definition eq_by_Zring_prod_package (P : Prop) := P. -Ltac auto_split_prod_step _ := +Ltac auto_split_prod_step_early _ := match goal with + | _ => progress hnf | [ H : prod _ _ |- _ ] => destruct H | [ |- forall a, _ ] => let a := fresh in intro a; compute in a + end. + +Ltac auto_split_prod_step _ := + match goal with + | _ => auto_split_prod_step_early () | [ |- pair _ _ = pair _ _ ] => apply f_equal2 | [ |- @eq (prod _ _) _ _ ] => apply path_prod end. Ltac Zring_prod_eq_tac _ := + repeat auto_split_prod_step_early (); cbv -[Z.add Z.sub Z.mul Z.div Z.pow Z.opp Z.log2 Z.land Z.lor Z.log2_up Z.abs]; repeat match goal with | _ => auto_split_prod_step () -- cgit v1.2.3