From 4e265aeba1226ed0e760936e4db2733aee8bded7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 4 Dec 2019 07:47:22 +0900 Subject: [PATCH] compatibility with mathcomp 1.10.0 --- .travis.yml | 4 ++-- opam | 4 ++-- theories/complex.v | 2 +- theories/polyrcf.v | 34 ++++++++++++++++++---------------- 4 files changed, 23 insertions(+), 21 deletions(-) diff --git a/.travis.yml b/.travis.yml index 71ded31..307e5ac 100644 --- a/.travis.yml +++ b/.travis.yml @@ -14,13 +14,13 @@ env: - NJOBS="2" - CONTRIB_NAME="real-closed" matrix: - - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.7" - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.8" - DOCKERIMAGE="mathcomp/mathcomp:1.8.0-coq-8.9" - - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.7" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.8" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.9" - DOCKERIMAGE="mathcomp/mathcomp:1.9.0-coq-8.10" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.9" + - DOCKERIMAGE="mathcomp/mathcomp:1.10.0-coq-8.10" install: | # Prepare the COQ container diff --git a/opam b/opam index 200b961..3fe8afb 100644 --- a/opam +++ b/opam @@ -11,8 +11,8 @@ build: [ make "-j" "%{jobs}%" ] install: [ make "install" ] depends: [ "coq" { (>= "8.7" & < "8.11~") } - "coq-mathcomp-field" { (>= "1.8.0" & < "1.10.0~") } - "coq-mathcomp-bigenough" {(>= "1.0.0" & < "1.1.0~")} + "coq-mathcomp-field" {(>= "1.8.0" & <= "1.10.0")} + "coq-mathcomp-bigenough" {(>= "1.0.0" & < "1.1~")} ] tags: [ "keyword:real closed field" "keyword:small scale reflection" "keyword:mathematical components" "date:2019-05-23" "logpath:mathcomp"] diff --git a/theories/complex.v b/theories/complex.v index 820ef01..77e44dc 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -1117,7 +1117,7 @@ have [] := @Lemma4 _ _ 1%:M _ [::L1; L2] (erefl _). do ![move: (_ *m _ *m _)] => t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12. rewrite [X in X + _ + _]addrC [X in X + _ = _]addrACA. rewrite [X in _ = (_ + _ + X) + _]addrC [X in _ = X + _]addrACA. - rewrite [X in _ + (_ + _ + X)]addrC [X in _ + X = _]addrACA. + rewrite [X in _ + (_ + _ + X) = _]addrC [X in _ + X = _]addrACA. rewrite [X in _ = _ + (X + _)]addrC [X in _ = _ + X]addrACA. rewrite [X in X = _]addrACA [X in _ = X]addrACA; congr (_ + _). by rewrite addrC [X in X + _ = _]addrACA [X in _ + X = _]addrACA. diff --git a/theories/polyrcf.v b/theories/polyrcf.v index 279ff51..1ad4222 100644 --- a/theories/polyrcf.v +++ b/theories/polyrcf.v @@ -951,12 +951,12 @@ case pr1 : (root p r1); case/monotonic_rootN => hrootsl; last 2 first. by rewrite -[s]cat0s; apply: (cat_roots_on hr1)=> //; rewrite pr1. - case: hrootsl=> r hr; exists (r::s); constructor=> //=. by rewrite -cat1s; apply: (cat_roots_on hr1)=> //; rewrite pr1. - rewrite path_min_sorted // => y; rewrite -hroot; case/andP=> hy _. - rewrite (@ltr_trans _ r1) ?(itvP hy) //. + rewrite path_min_sorted //; first [move=> y | apply/allP => y]. + rewrite -hroot; case/andP=> hy _; rewrite (@ltr_trans _ r1) ?(itvP hy) //. by rewrite (itvP (roots_on_in hr (mem_head _ _))). - exists (r1::s); constructor=> //=; last first. - rewrite path_min_sorted=> // y; rewrite -hroot. - by case/andP; move/itvP->. + rewrite path_min_sorted //; first [move=> y | apply/allP => y]. + by rewrite -hroot; case/andP; move/itvP->. move=> x; rewrite in_cons; case exr1: (x == r1)=> /=. by rewrite (eqP exr1) pr1 andbT. rewrite -hroot; case px: root; rewrite ?(andbT, andbF) //. @@ -966,7 +966,8 @@ case pr1 : (root p r1); case/monotonic_rootN => hrootsl; last 2 first. - case: hrootsl => r0 hrootsl. move/min_roots_on:hrootsl; case=> // hr0 har0 pr0 hr0r1. exists [:: r0, r1 & s]; constructor=> //=; last first. - rewrite (itvP hr0) /= path_min_sorted // => y. + rewrite (itvP hr0) /=. + rewrite path_min_sorted //; first [move=> y | apply/allP => y]. by rewrite -hroot; case/andP; move/itvP->. move=> y; rewrite !in_cons (itv_splitU2 hr1) (itv_splitU2 hr0). case eyr0: (y == r0); rewrite ?(orbT, orbF, orTb, orFb). @@ -999,8 +1000,9 @@ Hint Resolve sorted_roots. Lemma path_roots p a b : path <%R a (roots p a b). Proof. -case: rootsP=> //= p0 hp sp; rewrite path_min_sorted //. -by move=> y; rewrite -hp; case/andP; move/itvP->. +case: rootsP=> //= p0 hp sp. +rewrite path_min_sorted //; first [move=> y | apply/allP => y]. +by rewrite -hp; case/andP; move/itvP->. Qed. Hint Resolve path_roots. @@ -1139,7 +1141,7 @@ case/and3P=> hx hax; rewrite (eqP hax) in rax sax. case: rootsP p0=> // p0 rxb sxb _. case/andP=> px0 hxb; rewrite (eqP hxb) in rxb sxb. rewrite [_ :: _](@roots_uniq p a b) //; last first. - rewrite /= path_min_sorted // => y. + rewrite /= path_min_sorted //; first [move=> y | apply/allP => y]. by rewrite -(eqP hxb); move/roots_in; move/itvP->. move=> y; rewrite (itv_splitU2 hx) !andb_orl in_cons. case hy: (y == x); first by rewrite (eqP hy) px0 orbT. @@ -1171,9 +1173,9 @@ case/and3P=> hx hax; rewrite (eqP hax) in rax sax. case: rootsP p0=> // p0 rxb sxb _. case/andP=> px0 hxb; rewrite (eqP hxb) in rxb sxb. rewrite [rcons _ _](@roots_uniq p a b) //; last first. - rewrite -[rcons _ _]revK rev_sorted rev_rcons /= path_min_sorted. - by rewrite -rev_sorted revK. - move=> y; rewrite mem_rev; rewrite -(eqP hxb). + rewrite -[rcons _ _]revK rev_sorted rev_rcons /=. + rewrite path_min_sorted; [by rewrite -rev_sorted revK|]. + first [move=> y | apply/allP => y]; rewrite mem_rev; rewrite -(eqP hxb). by move/roots_in; move/itvP->. move=> y; rewrite (itv_splitU2 hx) mem_rcons in_cons !andb_orl. case hy: (y == x); first by rewrite (eqP hy) px0 orbT. @@ -1388,15 +1390,15 @@ Qed. Lemma gdcop_eq0 p q : (gdcop p q == 0) = (q == 0) && (p != 0). Proof. case: (eqVneq q 0) => [-> | q0]. - rewrite gdcop0 /= eqxx /=. - by case: (eqVneq p 0) => [-> | pn0]; rewrite ?(negPf pn0) eqxx ?oner_eq0. + rewrite gdcop0 /=. + by have [|] := (boolP (p == 0)) => [p0| pn0] /=; rewrite ?eqxx ?oner_eq0. rewrite /gdcop; move: {-1}(size q) (leqnn (size q))=> k hk. -case: (eqVneq p 0) => [-> | p0]. - rewrite eqxx andbF; apply: negPf. +case (eqVneq p 0) => [-> | p0]. + rewrite ?eqxx andbF; apply: negPf. elim: k q q0 {hk} => [|k ihk] q q0 /=; first by rewrite eqxx oner_eq0. case: ifP => _ //. by apply: ihk; rewrite gcdp0 divpp ?q0 // polyC_eq0; apply/lc_expn_scalp_neq0. -rewrite p0 (negPf q0) /=; apply: negPf. +rewrite ?(negbTE q0) andFb; apply: negPf. elim: k q q0 hk => [|k ihk] /= q q0 hk. by move: hk q0; rewrite leqn0 size_poly_eq0; move->. case: ifP=> cpq; first by rewrite (negPf q0).