blob: ef01dd069a84a08d7c218f2dd8e4490f4d940ed5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.setoid_ring.Ring_tac.
Require Import Crypto.Util.Prod.
Require Import Crypto.Util.SideConditions.CorePackages.
Require Export Crypto.Util.FixCoqMistakes.
Definition eq_by_Zring_prod_package (P : Prop) := P.
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 ()
| [ |- @eq Z _ _ ] => ring
end.
Ltac autosolve else_tac :=
lazymatch goal with
| [ |- eq_by_Zring_prod_package _ ]
=> solve [ Zring_prod_eq_tac () ]
| _ => else_tac ()
end.
|
