Skip to content

Commit a6f7a07

Browse files
palmskogpalmskog
authored
Merge pull request #11 from coq-community/fix-8.11
port to 8.11
2 parents 1c03d0b + 19ed36c commit a6f7a07

19 files changed

+131
-100
lines changed

‎.gitignore‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,9 @@
33
*.aux
44
*.d
55
*.vo
6+
*.vos
7+
*.vok
8+
_build
69
Makefile.coq
710
Makefile.coq.conf
811
result

‎.travis.yml‎

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -46,6 +46,15 @@ jobs:
4646
include:
4747

4848
# Test supported versions of Coq via Nix
49+
- env:
50+
- COQ=https://github.com/coq/coq-on-cachix/tarball/master
51+
<<: *NIX
52+
- env:
53+
- COQ=8.12
54+
<<: *NIX
55+
- env:
56+
- COQ=8.11
57+
<<: *NIX
4958
- env:
5059
- COQ=8.10
5160
<<: *NIX
@@ -61,7 +70,7 @@ jobs:
6170

6271
# Test supported versions of Coq via OPAM
6372
- env:
64-
- COQ_IMAGE=coqorg/coq:8.10
73+
- COQ_IMAGE=coqorg/coq:dev
6574
- PACKAGE=coq-qarith-stern-brocot.dev
6675
- NJOBS=2
6776
<<: *OPAM

‎Q_order.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -117,7 +117,7 @@ Inductive Qgt : Q -> Q -> Prop :=
117117
| Qgt_pos_zero : forall x' : Qpositive, Qgt (Qpos x') Zero
118118
| Qgt_pos_neg : forall x' y' : Qpositive, Qgt (Qpos x') (Qneg y')
119119
| Qgt_zero_neg : forall x' : Qpositive, Qgt Zero (Qneg x').
120-
Hint Resolve Qgt_pos_pos Qgt_neg_neg Qgt_pos_zero Qgt_pos_neg Qgt_zero_neg.
120+
Hint Resolve Qgt_pos_pos Qgt_neg_neg Qgt_pos_zero Qgt_pos_neg Qgt_zero_neg : core.
121121

122122
Theorem Qgt_total : forall x y : Q, Qgt x y \/ x = y \/ Qgt y x.
123123
intros x y; case y; case x; auto.

‎Q_ordered_field_properties.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -338,7 +338,7 @@ Qed.
338338

339339
Hint Resolve Qinv_pos Qinv_resp_nonzero Qminus_Qeq Qeq_Qminus
340340
Qlt_not_eq' Qinv_neg Qle_Qopp_pos Qlt_Qopp_pos
341-
Qlt_Qopp_neg Qopp_Qone_Qlt_Qone.
341+
Qlt_Qopp_neg Qopp_Qone_Qlt_Qone : core.
342342

343343
Lemma Qle_mult_nonneg_pos: forall x y : Q, Zero <= x -> Zero < y -> Zero <= x * y.
344344
Proof.

‎Qhomographic_sign_properties.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1580,15 +1580,15 @@ Proof.
15801580
end ].
15811581
case (not_Zeq_inf (Z.sgn (a + b)) 0 Hab); intro Hab';
15821582
[ right; split; [ apply Zsgn_11; assumption | apply Zsgn_12 ];
1583-
generalize (Zsgn_1 (c + d)); intros [[Hcd| Hcd]| Hcd];
1583+
generalize (Zsgn_1' (c + d)); intros [[Hcd| Hcd]| Hcd];
15841584
[ apply False_ind;
15851585
apply (Qhomographic_signok_1 c d H_Qhomographic_sg_denom_nonzero);
15861586
apply Zsgn_2
15871587
| rewrite Hcd; constructor
15881588
| apply False_ind; apply Habcd; rewrite Hcd; apply Zsgn_8;
15891589
apply Zsgn_11 ]; assumption
15901590
| left; split; [ apply Zsgn_12; assumption | apply Zsgn_11 ];
1591-
generalize (Zsgn_1 (c + d)); intros [[Hcd| Hcd]| Hcd];
1591+
generalize (Zsgn_1' (c + d)); intros [[Hcd| Hcd]| Hcd];
15921592
[ apply False_ind;
15931593
apply (Qhomographic_signok_1 c d H_Qhomographic_sg_denom_nonzero);
15941594
apply Zsgn_2

‎Qpositive.v‎

Lines changed: 51 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -357,53 +357,57 @@ change
357357
(dL (Qpositive_c (S p) (S q2) (S n0)) =
358358
dL (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *.
359359
apply f_equal with (f := dL).
360-
apply Hrec with d; auto with *.
361-
rewrite <- Heqp'2; assumption.
362-
rewrite <- Heq4; rewrite <- Heq2; rewrite (mult_comm (S d)).
363-
rewrite mult_minus_distr_r.
364-
repeat rewrite <- (mult_comm (S d)).
365-
rewrite <- Heqd2; rewrite <- Heqd1.
366-
simpl in |- *; auto.
367-
apply mult_S_le_reg_l with d.
368-
rewrite <- Heqd2; rewrite <- Heqd1.
369-
apply le_n_S.
370-
apply minus_O_le; assumption.
371-
intros p2 Heqp2.
372-
CaseEq (p' - q').
373-
intros Heqm'; cut (S p - S q = 0).
374-
simpl in |- *; rewrite Heqp2; intros Dummy; discriminate Dummy.
375-
rewrite Heqd2; rewrite Heqd1.
376-
repeat rewrite (mult_comm (S d)).
377-
rewrite <- mult_minus_distr_r.
378-
rewrite Heqm'; simpl in |- *; auto.
379-
intros p'2.
380-
generalize Hle2; case n'.
381-
generalize Heqd1 Heqd2; case p'; case q'.
382-
simpl in |- *; intros H'1 H'2 H'3 H'4; discriminate H'4.
383-
intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy;
384-
discriminate Dummy.
385-
intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy1 Dummy2;
386-
discriminate Dummy2.
387-
simpl in |- *; intros n n1 H'1 H'2; rewrite <- plus_n_Sm; intros H'3;
388-
inversion H'3.
389-
inversion H0.
390-
intros n''.
391-
intros Hle3 Heq4.
392-
CaseEq q'.
393-
intros Heq5; generalize Heqd2; rewrite Heq5; simpl in |- *.
394-
rewrite <- (mult_comm 0); simpl in |- *; intros Dummy; discriminate Dummy.
395-
intros q'2 Heqq'2.
396-
change
397-
(nR (Qpositive_c (S p2) (S q) (S n0)) =
398-
nR (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *.
399-
apply f_equal with (f := nR).
400-
apply Hrec with d; auto with *.
401-
rewrite <- Heq4; rewrite <- Heqp2; rewrite (mult_comm (S d)).
402-
rewrite mult_minus_distr_r.
403-
repeat rewrite <- (mult_comm (S d)).
404-
rewrite <- Heqd2; rewrite <- Heqd1.
405-
simpl in |- *; auto.
406-
rewrite <- Heqq'2; assumption.
360+
apply Hrec with d.
361+
- rewrite <- Heqp'2; assumption.
362+
- rewrite <- Heq4; rewrite <- Heq2; rewrite (mult_comm (S d)).
363+
rewrite mult_minus_distr_r.
364+
repeat rewrite <- (mult_comm (S d)).
365+
rewrite <- Heqd2; rewrite <- Heqd1.
366+
simpl in |- *; auto.
367+
- auto with zarith.
368+
- auto with zarith.
369+
- apply mult_S_le_reg_l with d.
370+
rewrite <- Heqd2; rewrite <- Heqd1.
371+
apply le_n_S.
372+
apply minus_O_le; assumption.
373+
- intros p2 Heqp2.
374+
CaseEq (p' - q').
375+
intros Heqm'; cut (S p - S q = 0).
376+
simpl in |- *; rewrite Heqp2; intros Dummy; discriminate Dummy.
377+
rewrite Heqd2; rewrite Heqd1.
378+
repeat rewrite (mult_comm (S d)).
379+
rewrite <- mult_minus_distr_r.
380+
rewrite Heqm'; simpl in |- *; auto.
381+
intros p'2.
382+
generalize Hle2; case n'.
383+
generalize Heqd1 Heqd2; case p'; case q'.
384+
simpl in |- *; intros H'1 H'2 H'3 H'4; discriminate H'4.
385+
intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy;
386+
discriminate Dummy.
387+
intros x; rewrite <- (mult_comm 0); simpl in |- *; intros Dummy1 Dummy2;
388+
discriminate Dummy2.
389+
simpl in |- *; intros n n1 H'1 H'2; rewrite <- plus_n_Sm; intros H'3;
390+
inversion H'3.
391+
inversion H0.
392+
intros n''.
393+
intros Hle3 Heq4.
394+
CaseEq q'.
395+
intros Heq5; generalize Heqd2; rewrite Heq5; simpl in |- *.
396+
rewrite <- (mult_comm 0); simpl in |- *; intros Dummy; discriminate Dummy.
397+
intros q'2 Heqq'2.
398+
change
399+
(nR (Qpositive_c (S p2) (S q) (S n0)) =
400+
nR (Qpositive_c (S p'2) (S q'2) (S n''))) in |- *.
401+
apply f_equal with (f := nR).
402+
apply Hrec with d.
403+
* rewrite <- Heq4; rewrite <- Heqp2; rewrite (mult_comm (S d)).
404+
rewrite mult_minus_distr_r.
405+
repeat rewrite <- (mult_comm (S d)).
406+
rewrite <- Heqd2; rewrite <- Heqd1.
407+
simpl in |- *; auto.
408+
* rewrite <- Heqq'2; assumption.
409+
* auto with zarith.
410+
* auto with zarith.
407411
Qed.
408412

409413
Theorem construct_correct4 :

‎Qquadratic.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -507,7 +507,7 @@ case (Qquadratic_sign_sign_dec a b c d e f g h p1 p2 H_qsign).
507507

508508
(* still l1=1 -> Q *)
509509
case
510-
(Zsgn_1
510+
(Zsgn_1'
511511
(qnew_a a b c d e f g h p1 p2 H_qsign +
512512
qnew_b a b c d e f g h p1 p2 H_qsign +
513513
qnew_c a b c d e f g h p1 p2 H_qsign +
@@ -598,7 +598,7 @@ case (Qquadratic_sign_sign_dec a b c d e f g h p1 p2 H_qsign).
598598

599599
(* still l1= -1 -> Q *)
600600
case
601-
(Zsgn_1
601+
(Zsgn_1'
602602
(qnew_a a b c d e f g h p1 p2 H_qsign +
603603
qnew_b a b c d e f g h p1 p2 H_qsign +
604604
qnew_c a b c d e f g h p1 p2 H_qsign +

‎Qquadratic_sign.v‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1553,15 +1553,15 @@ Proof.
15531553
case (three_integers_dec_inf f g h); intro Hfgh;
15541554
[ rewrite Qquadratic_sign_nRdL_nRdL_1;
15551555
try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
1556-
apply Zsgn_1
1556+
apply Zsgn_1'
15571557
| case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
15581558
[ rewrite Qquadratic_sign_nRdL_nRdL_2;
15591559
try solve [ discriminate | assumption ];
1560-
apply Zsgn_1
1560+
apply Zsgn_1'
15611561
| case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
15621562
[ rewrite Qquadratic_sign_nRdL_nRdL_3;
15631563
try solve [ discriminate | assumption ];
1564-
rewrite <- Zsgn_25; apply Zsgn_1
1564+
rewrite <- Zsgn_25; apply Zsgn_1'
15651565
| match goal with
15661566
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
15671567
rewrite
@@ -1599,11 +1599,11 @@ Proof.
15991599
| case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
16001600
[ rewrite Qquadratic_sign_nRdL_nRdL_5;
16011601
try solve [ discriminate | assumption ];
1602-
apply Zsgn_1
1602+
apply Zsgn_1'
16031603
| case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
16041604
[ rewrite Qquadratic_sign_nRdL_nRdL_6;
16051605
try solve [ discriminate | assumption ];
1606-
rewrite <- Zsgn_25; apply Zsgn_1
1606+
rewrite <- Zsgn_25; apply Zsgn_1'
16071607
| match goal with
16081608
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
16091609
rewrite
@@ -1690,15 +1690,15 @@ Proof.
16901690
case (three_integers_dec_inf f g h); intro Hfgh;
16911691
[ rewrite Qquadratic_sign_nRdL_nRdL_1;
16921692
try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
1693-
apply Zsgn_1
1693+
apply Zsgn_1'
16941694
| case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
16951695
[ rewrite Qquadratic_sign_nRdL_nRdL_2;
16961696
try solve [ discriminate | assumption ];
1697-
apply Zsgn_1
1697+
apply Zsgn_1'
16981698
| case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
16991699
[ rewrite Qquadratic_sign_nRdL_nRdL_3;
17001700
try solve [ discriminate | assumption ];
1701-
rewrite <- Zsgn_25; apply Zsgn_1
1701+
rewrite <- Zsgn_25; apply Zsgn_1'
17021702
| match goal with
17031703
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
17041704
rewrite
@@ -1736,11 +1736,11 @@ Proof.
17361736
| case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
17371737
[ rewrite Qquadratic_sign_nRdL_nRdL_5;
17381738
try solve [ discriminate | assumption ];
1739-
apply Zsgn_1
1739+
apply Zsgn_1'
17401740
| case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
17411741
[ rewrite Qquadratic_sign_nRdL_nRdL_6;
17421742
try solve [ discriminate | assumption ];
1743-
rewrite <- Zsgn_25; apply Zsgn_1
1743+
rewrite <- Zsgn_25; apply Zsgn_1'
17441744
| match goal with
17451745
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
17461746
rewrite
@@ -1851,15 +1851,15 @@ Proof.
18511851
case (three_integers_dec_inf f g h); intro Hfgh;
18521852
[ rewrite Qquadratic_sign_nRdL_nRdL_1;
18531853
try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
1854-
apply Zsgn_1
1854+
apply Zsgn_1'
18551855
| case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
18561856
[ rewrite Qquadratic_sign_nRdL_nRdL_2;
18571857
try solve [ discriminate | assumption ];
1858-
apply Zsgn_1
1858+
apply Zsgn_1'
18591859
| case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
18601860
[ rewrite Qquadratic_sign_nRdL_nRdL_3;
18611861
try solve [ discriminate | assumption ];
1862-
rewrite <- Zsgn_25; apply Zsgn_1
1862+
rewrite <- Zsgn_25; apply Zsgn_1'
18631863
| match goal with
18641864
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
18651865
rewrite
@@ -1897,11 +1897,11 @@ Proof.
18971897
| case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
18981898
[ rewrite Qquadratic_sign_nRdL_nRdL_5;
18991899
try solve [ discriminate | assumption ];
1900-
apply Zsgn_1
1900+
apply Zsgn_1'
19011901
| case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
19021902
[ rewrite Qquadratic_sign_nRdL_nRdL_6;
19031903
try solve [ discriminate | assumption ];
1904-
rewrite <- Zsgn_25; apply Zsgn_1
1904+
rewrite <- Zsgn_25; apply Zsgn_1'
19051905
| match goal with
19061906
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
19071907
rewrite
@@ -1988,15 +1988,15 @@ Proof.
19881988
case (three_integers_dec_inf f g h); intro Hfgh;
19891989
[ rewrite Qquadratic_sign_nRdL_nRdL_1;
19901990
try solve [ discriminate | assumption ]; rewrite <- Zsgn_15;
1991-
apply Zsgn_1
1991+
apply Zsgn_1'
19921992
| case (Z_lt_dec 2 (outside_square e f g h)); intro Ho2;
19931993
[ rewrite Qquadratic_sign_nRdL_nRdL_2;
19941994
try solve [ discriminate | assumption ];
1995-
apply Zsgn_1
1995+
apply Zsgn_1'
19961996
| case (Z_lt_dec (outside_square e f g h) (-2)); intro Ho2';
19971997
[ rewrite Qquadratic_sign_nRdL_nRdL_3;
19981998
try solve [ discriminate | assumption ];
1999-
rewrite <- Zsgn_25; apply Zsgn_1
1999+
rewrite <- Zsgn_25; apply Zsgn_1'
20002000
| match goal with
20012001
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
20022002
rewrite
@@ -2034,11 +2034,11 @@ Proof.
20342034
| case (Z_lt_dec 2 (outside_square a b c d)); intro Ho1;
20352035
[ rewrite Qquadratic_sign_nRdL_nRdL_5;
20362036
try solve [ discriminate | assumption ];
2037-
apply Zsgn_1
2037+
apply Zsgn_1'
20382038
| case (Z_lt_dec (outside_square a b c d) (-2)); intro Ho1';
20392039
[ rewrite Qquadratic_sign_nRdL_nRdL_6;
20402040
try solve [ discriminate | assumption ];
2041-
rewrite <- Zsgn_25; apply Zsgn_1
2041+
rewrite <- Zsgn_25; apply Zsgn_1'
20422042
| match goal with
20432043
| id1:(?X1 ?X2 ?X3 ?X4 ?X5 (nR ?X6) (nR ?X7)) |- ?X8 =>
20442044
rewrite

‎README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ field operations on them in two different ways: strict and lazy.
3434
- Coq-community maintainer(s):
3535
- Hugo Herbelin ([**@herbelin**](https://github.com/herbelin))
3636
- License: [GNU Lesser General Public License v2.1 or later](LICENSE)
37-
- Compatible Coq versions: 8.7 to 8.10
37+
- Compatible Coq versions: 8.7 and later
3838
- Additional dependencies: none
3939
- Coq namespace: `QArithSternBrocot`
4040
- Related publication(s):

‎R_addenda.v‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,8 @@ Require Import Fourier.
1414
Require Import Euclid.
1515
Require Import Omega.
1616

17+
Open Scope R_scope.
18+
1719
Lemma Rlt_stepl:forall x y z, Rlt x y -> x=z -> Rlt z y.
1820
Proof.
1921
intros x y z H_lt H_eq; subst; assumption.
@@ -111,7 +113,7 @@ Definition Ropp_resp_nonzero:=RIneq.Ropp_neq_0_compat.
111113

112114
Hint Resolve Rlt_Ropp_pos Rinv_pos R1_neq_R0 Rle_mult_nonneg_nonneg
113115
Rlt_mult_pos_pos Rlt_mult_neg_neg Rlt_not_eq' Rlt_not_eq
114-
Rmult_resp_nonzero Rinv_resp_nonzero Ropp_resp_nonzero.
116+
Rmult_resp_nonzero Rinv_resp_nonzero Ropp_resp_nonzero : core.
115117

116118
Lemma Rmult_mult_nonneg: forall r, 0<=r*r.
117119
Proof.
@@ -386,7 +388,7 @@ Proof.
386388
intros n; apply lt_INR_0; auto with arith.
387389
Qed.
388390

389-
Hint Resolve not_O_S_INR pos_S_INR pos_INR.
391+
Hint Resolve not_O_S_INR pos_S_INR pos_INR : core.
390392

391393

392394
Lemma Req_Rdiv_Rone:forall x y, y<>0 -> x=y -> x/y =1.

0 commit comments

Comments
 (0)