Skip to content

Commit 88b5291

Browse files
proux01lukaszcz
proux01
authored and
lukaszcz
committed
1 parent 8649603 commit 88b5291

File tree

3 files changed

+84
-84
lines changed

3 files changed

+84
-84
lines changed

‎theories/Tactics/Hints.v‎

Lines changed: 52 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -1,32 +1,32 @@
11
From Hammer Require Import Tactics.
22
Require List Arith ZArith Bool.
33

4-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_0_r : shints.
5-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_1_r : shints.
6-
Global Hint Rewrite -> Arith.PeanoNat.Nat.sub_0_r : shints.
7-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_0_r : shints.
8-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_1_r : shints.
9-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_assoc : shints.
10-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_assoc : shints.
11-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_add_distr_r : shints.
12-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_add_distr_l : shints.
13-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_sub_distr_r : shints.
14-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_sub_distr_l : shints.
15-
Global Hint Rewrite -> Arith.PeanoNat.Nat.sub_add_distr : shints.
16-
Global Hint Rewrite <- Arith.PeanoNat.Nat.leb_antisym : shints.
17-
Global Hint Rewrite <- Arith.PeanoNat.Nat.ltb_antisym : shints.
18-
Global Hint Rewrite -> ZArith.BinInt.Z.add_0_r : shints.
19-
Global Hint Rewrite -> ZArith.BinInt.Z.add_1_r : shints.
20-
Global Hint Rewrite -> ZArith.BinInt.Z.sub_0_r : shints.
21-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_0_r : shints.
22-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_1_r : shints.
23-
Global Hint Rewrite -> ZArith.BinInt.Z.add_assoc : shints.
24-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_assoc : shints.
25-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_add_distr_r : shints.
26-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_add_distr_l : shints.
27-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_sub_distr_r : shints.
28-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_sub_distr_l : shints.
29-
Global Hint Rewrite -> ZArith.BinInt.Z.sub_add_distr : shints.
4+
Global Hint Rewrite -> PeanoNat.Nat.add_0_r : shints.
5+
Global Hint Rewrite -> PeanoNat.Nat.add_1_r : shints.
6+
Global Hint Rewrite -> PeanoNat.Nat.sub_0_r : shints.
7+
Global Hint Rewrite -> PeanoNat.Nat.mul_0_r : shints.
8+
Global Hint Rewrite -> PeanoNat.Nat.mul_1_r : shints.
9+
Global Hint Rewrite -> PeanoNat.Nat.add_assoc : shints.
10+
Global Hint Rewrite -> PeanoNat.Nat.mul_assoc : shints.
11+
Global Hint Rewrite -> PeanoNat.Nat.mul_add_distr_r : shints.
12+
Global Hint Rewrite -> PeanoNat.Nat.mul_add_distr_l : shints.
13+
Global Hint Rewrite -> PeanoNat.Nat.mul_sub_distr_r : shints.
14+
Global Hint Rewrite -> PeanoNat.Nat.mul_sub_distr_l : shints.
15+
Global Hint Rewrite -> PeanoNat.Nat.sub_add_distr : shints.
16+
Global Hint Rewrite <- PeanoNat.Nat.leb_antisym : shints.
17+
Global Hint Rewrite <- PeanoNat.Nat.ltb_antisym : shints.
18+
Global Hint Rewrite -> BinInt.Z.add_0_r : shints.
19+
Global Hint Rewrite -> BinInt.Z.add_1_r : shints.
20+
Global Hint Rewrite -> BinInt.Z.sub_0_r : shints.
21+
Global Hint Rewrite -> BinInt.Z.mul_0_r : shints.
22+
Global Hint Rewrite -> BinInt.Z.mul_1_r : shints.
23+
Global Hint Rewrite -> BinInt.Z.add_assoc : shints.
24+
Global Hint Rewrite -> BinInt.Z.mul_assoc : shints.
25+
Global Hint Rewrite -> BinInt.Z.mul_add_distr_r : shints.
26+
Global Hint Rewrite -> BinInt.Z.mul_add_distr_l : shints.
27+
Global Hint Rewrite -> BinInt.Z.mul_sub_distr_r : shints.
28+
Global Hint Rewrite -> BinInt.Z.mul_sub_distr_l : shints.
29+
Global Hint Rewrite -> BinInt.Z.sub_add_distr : shints.
3030
Global Hint Rewrite -> List.in_app_iff : shints.
3131
Global Hint Rewrite -> List.in_map_iff : shints.
3232
Global Hint Rewrite <- List.app_assoc : shints.
@@ -57,30 +57,30 @@ Global Hint Rewrite -> List.in_app_iff : slist.
5757
Global Hint Rewrite -> List.in_map_iff : slist.
5858
Global Hint Rewrite <- List.app_assoc : slist.
5959

60-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_0_r : sarith.
61-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_1_r : sarith.
62-
Global Hint Rewrite -> Arith.PeanoNat.Nat.sub_0_r : sarith.
63-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_0_r : sarith.
64-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_1_r : sarith.
65-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_assoc : sarith.
66-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_assoc : sarith.
67-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_add_distr_r : sarith.
68-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_add_distr_l : sarith.
69-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_sub_distr_r : sarith.
70-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_sub_distr_l : sarith.
71-
Global Hint Rewrite -> Arith.PeanoNat.Nat.sub_add_distr : sarith.
72-
Global Hint Rewrite <- Arith.PeanoNat.Nat.leb_antisym : sarith.
73-
Global Hint Rewrite <- Arith.PeanoNat.Nat.ltb_antisym : sarith.
60+
Global Hint Rewrite -> PeanoNat.Nat.add_0_r : sarith.
61+
Global Hint Rewrite -> PeanoNat.Nat.add_1_r : sarith.
62+
Global Hint Rewrite -> PeanoNat.Nat.sub_0_r : sarith.
63+
Global Hint Rewrite -> PeanoNat.Nat.mul_0_r : sarith.
64+
Global Hint Rewrite -> PeanoNat.Nat.mul_1_r : sarith.
65+
Global Hint Rewrite -> PeanoNat.Nat.add_assoc : sarith.
66+
Global Hint Rewrite -> PeanoNat.Nat.mul_assoc : sarith.
67+
Global Hint Rewrite -> PeanoNat.Nat.mul_add_distr_r : sarith.
68+
Global Hint Rewrite -> PeanoNat.Nat.mul_add_distr_l : sarith.
69+
Global Hint Rewrite -> PeanoNat.Nat.mul_sub_distr_r : sarith.
70+
Global Hint Rewrite -> PeanoNat.Nat.mul_sub_distr_l : sarith.
71+
Global Hint Rewrite -> PeanoNat.Nat.sub_add_distr : sarith.
72+
Global Hint Rewrite <- PeanoNat.Nat.leb_antisym : sarith.
73+
Global Hint Rewrite <- PeanoNat.Nat.ltb_antisym : sarith.
7474

75-
Global Hint Rewrite -> ZArith.BinInt.Z.add_0_r : szarith.
76-
Global Hint Rewrite -> ZArith.BinInt.Z.add_1_r : szarith.
77-
Global Hint Rewrite -> ZArith.BinInt.Z.sub_0_r : szarith.
78-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_0_r : szarith.
79-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_1_r : szarith.
80-
Global Hint Rewrite -> ZArith.BinInt.Z.add_assoc : szarith.
81-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_assoc : szarith.
82-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_add_distr_r : szarith.
83-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_add_distr_l : szarith.
84-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_sub_distr_r : szarith.
85-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_sub_distr_l : szarith.
86-
Global Hint Rewrite -> ZArith.BinInt.Z.sub_add_distr : szarith.
75+
Global Hint Rewrite -> BinInt.Z.add_0_r : szarith.
76+
Global Hint Rewrite -> BinInt.Z.add_1_r : szarith.
77+
Global Hint Rewrite -> BinInt.Z.sub_0_r : szarith.
78+
Global Hint Rewrite -> BinInt.Z.mul_0_r : szarith.
79+
Global Hint Rewrite -> BinInt.Z.mul_1_r : szarith.
80+
Global Hint Rewrite -> BinInt.Z.add_assoc : szarith.
81+
Global Hint Rewrite -> BinInt.Z.mul_assoc : szarith.
82+
Global Hint Rewrite -> BinInt.Z.mul_add_distr_r : szarith.
83+
Global Hint Rewrite -> BinInt.Z.mul_add_distr_l : szarith.
84+
Global Hint Rewrite -> BinInt.Z.mul_sub_distr_r : szarith.
85+
Global Hint Rewrite -> BinInt.Z.mul_sub_distr_l : szarith.
86+
Global Hint Rewrite -> BinInt.Z.sub_add_distr : szarith.

‎theories/Tactics/Reconstr.v‎

Lines changed: 22 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -12,28 +12,28 @@ Inductive ReconstrT : Set := Empty : ReconstrT | AllHyps : ReconstrT.
1212

1313
Create HintDb yhints discriminated.
1414

15-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_0_r : yhints.
16-
Global Hint Rewrite -> Arith.PeanoNat.Nat.sub_0_r : yhints.
17-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_0_r : yhints.
18-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_1_r : yhints.
19-
Global Hint Rewrite -> Arith.PeanoNat.Nat.add_assoc : yhints.
20-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_assoc : yhints.
21-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_add_distr_r : yhints.
22-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_add_distr_l : yhints.
23-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_sub_distr_r : yhints.
24-
Global Hint Rewrite -> Arith.PeanoNat.Nat.mul_sub_distr_l : yhints.
25-
Global Hint Rewrite -> Arith.PeanoNat.Nat.sub_add_distr : yhints.
26-
Global Hint Rewrite -> ZArith.BinInt.Z.add_0_r : yhints.
27-
Global Hint Rewrite -> ZArith.BinInt.Z.sub_0_r : yhints.
28-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_0_r : yhints.
29-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_1_r : yhints.
30-
Global Hint Rewrite -> ZArith.BinInt.Z.add_assoc : yhints.
31-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_assoc : yhints.
32-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_add_distr_r : yhints.
33-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_add_distr_l : yhints.
34-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_sub_distr_r : yhints.
35-
Global Hint Rewrite -> ZArith.BinInt.Z.mul_sub_distr_l : yhints.
36-
Global Hint Rewrite -> ZArith.BinInt.Z.sub_add_distr : yhints.
15+
Global Hint Rewrite -> PeanoNat.Nat.add_0_r : yhints.
16+
Global Hint Rewrite -> PeanoNat.Nat.sub_0_r : yhints.
17+
Global Hint Rewrite -> PeanoNat.Nat.mul_0_r : yhints.
18+
Global Hint Rewrite -> PeanoNat.Nat.mul_1_r : yhints.
19+
Global Hint Rewrite -> PeanoNat.Nat.add_assoc : yhints.
20+
Global Hint Rewrite -> PeanoNat.Nat.mul_assoc : yhints.
21+
Global Hint Rewrite -> PeanoNat.Nat.mul_add_distr_r : yhints.
22+
Global Hint Rewrite -> PeanoNat.Nat.mul_add_distr_l : yhints.
23+
Global Hint Rewrite -> PeanoNat.Nat.mul_sub_distr_r : yhints.
24+
Global Hint Rewrite -> PeanoNat.Nat.mul_sub_distr_l : yhints.
25+
Global Hint Rewrite -> PeanoNat.Nat.sub_add_distr : yhints.
26+
Global Hint Rewrite -> BinInt.Z.add_0_r : yhints.
27+
Global Hint Rewrite -> BinInt.Z.sub_0_r : yhints.
28+
Global Hint Rewrite -> BinInt.Z.mul_0_r : yhints.
29+
Global Hint Rewrite -> BinInt.Z.mul_1_r : yhints.
30+
Global Hint Rewrite -> BinInt.Z.add_assoc : yhints.
31+
Global Hint Rewrite -> BinInt.Z.mul_assoc : yhints.
32+
Global Hint Rewrite -> BinInt.Z.mul_add_distr_r : yhints.
33+
Global Hint Rewrite -> BinInt.Z.mul_add_distr_l : yhints.
34+
Global Hint Rewrite -> BinInt.Z.mul_sub_distr_r : yhints.
35+
Global Hint Rewrite -> BinInt.Z.mul_sub_distr_l : yhints.
36+
Global Hint Rewrite -> BinInt.Z.sub_add_distr : yhints.
3737
Global Hint Rewrite -> List.in_app_iff : yhints.
3838
Global Hint Rewrite -> List.in_map_iff : yhints.
3939
Global Hint Rewrite -> List.in_inv : yhints.

‎theories/Tactics/Tactics.v‎

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66
Declare ML Module "coq-hammer-tactics.lib".
77

88
Require Import Lia.
9-
Require Import Program.Equality.
9+
From Stdlib.Program Require Import Equality.
1010
From Hammer Require Import Tactics.Reflect.
1111

1212
Create HintDb shints discriminated.
@@ -379,11 +379,11 @@ Ltac trysolve :=
379379
eauto 2 with shints; try solve [ constructor ];
380380
match goal with
381381
| [ |- ?t = ?u ] => try solve [ try subst; congruence 8 |
382-
match type of t with nat => lia | ZArith.BinInt.Z => lia end ]
382+
match type of t with nat => lia | BinInt.Z => lia end ]
383383
| [ |- ?t <> ?u ] => try solve [ try subst; congruence 8 |
384-
match type of t with nat => lia | ZArith.BinInt.Z => lia end ]
384+
match type of t with nat => lia | BinInt.Z => lia end ]
385385
| [ |- (?t = ?u) -> False ] => try solve [ intro; try subst; congruence 8 |
386-
match type of t with nat => lia | ZArith.BinInt.Z => lia end ]
386+
match type of t with nat => lia | BinInt.Z => lia end ]
387387
| [ |- False ] => try solve [ try subst; congruence 8 ]
388388
| [ |- ?t >= ?u ] => try solve [ lia ]
389389
| [ |- ?t <= ?u ] => try solve [ lia ]
@@ -530,24 +530,24 @@ Ltac bnat_reflect :=
530530
clear H
531531
| [ H : (Nat.eqb ?A ?B) = true |- _ ] =>
532532
notHyp (A = B);
533-
assert (A = B) by (rewrite Coq.Arith.PeanoNat.Nat.eqb_eq in H; apply H);
533+
assert (A = B) by (rewrite PeanoNat.Nat.eqb_eq in H; apply H);
534534
try subst
535535
| [ H : (Nat.eqb ?A ?B) = false |- _ ] =>
536536
notHyp (A = B -> False);
537537
assert (A = B -> False) by
538-
(rewrite <- Coq.Arith.PeanoNat.Nat.eqb_eq; rewrite H; discriminate)
538+
(rewrite <- PeanoNat.Nat.eqb_eq; rewrite H; discriminate)
539539
| [ H : (Nat.leb ?A ?B) = true |- _ ] =>
540540
notHyp (A <= B);
541-
assert (A <= B) by (apply Coq.Arith.Compare_dec.leb_complete; apply H)
541+
assert (A <= B) by (apply Compare_dec.leb_complete; apply H)
542542
| [ H : (Nat.leb ?A ?B) = false |- _ ] =>
543543
notHyp (B < A);
544-
assert (B < A) by (apply Coq.Arith.Compare_dec.leb_complete_conv; apply H)
544+
assert (B < A) by (apply Compare_dec.leb_complete_conv; apply H)
545545
| [ H : (Nat.ltb ?A ?B) = true |- _ ] =>
546546
notHyp (A < B);
547-
assert (A < B) by (apply Coq.Arith.PeanoNat.Nat.ltb_lt; apply H)
547+
assert (A < B) by (apply PeanoNat.Nat.ltb_lt; apply H)
548548
| [ H : (Nat.ltb ?A ?B) = false |- _ ] =>
549549
notHyp (B <= A);
550-
assert (B <= A) by (apply Coq.Arith.PeanoNat.Nat.ltb_ge; apply H)
550+
assert (B <= A) by (apply PeanoNat.Nat.ltb_ge; apply H)
551551
| [ H : (BinNat.N.eqb ?A ?B) = true |- _ ] =>
552552
notHyp (A = B);
553553
assert (A = B) by (apply Coq.NArith.BinNat.N.eqb_eq; apply H);

0 commit comments

Comments
 (0)