From 99a29672f5c79fcc3a502a25a720f1f9dcf6fcee Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 28 Mar 2024 16:04:46 +0100 Subject: [PATCH 1/2] Adapt to math-comp/math-comp#1190 --- theories/approx.v | 6 ++--- theories/cfmap.v | 2 +- theories/chromogram.v | 2 +- theories/color.v | 2 +- theories/coloring.v | 14 +++++------ theories/contract.v | 4 +-- theories/cube.v | 4 +-- theories/dedekind.v | 58 +++++++++++++++++++++---------------------- theories/discharge.v | 10 ++++---- theories/discretize.v | 4 +-- theories/embed.v | 16 ++++++------ theories/grid.v | 42 +++++++++++++++---------------- theories/gridmap.v | 30 +++++++++++----------- theories/hubcap.v | 18 +++++++------- theories/jordan.v | 2 +- theories/kempe.v | 4 +-- theories/matte.v | 18 +++++++------- theories/patch.v | 25 ++++++++----------- theories/realprop.v | 6 ++--- theories/sew.v | 6 ++--- theories/snip.v | 18 +++++++------- theories/walkup.v | 2 +- 22 files changed, 144 insertions(+), 149 deletions(-) diff --git a/theories/approx.v b/theories/approx.v index 400a439..63d3e71 100644 --- a/theories/approx.v +++ b/theories/approx.v @@ -266,11 +266,11 @@ have [nx1 lbx1 ubx1] := approx_between Dmx Dmx1 (scale_s_dxy (i4 1%N isT)). have [ny0 lby0 uby0] := approx_between Dmy0 Dmy (scale_s_dxy (i4 2%N isT)). have [ny1 lby1 uby1] := approx_between Dmy Dmy1 (scale_s_dxy (i4 3%N isT)). exists (s1, Grect nx0 (nx1 + 1) ny0 (ny1 + 1)) => /=. - by exists (Gpoint mx my); rewrite //= !addrK -!lez_addr1 ubx0 lbx1 uby0 lby1. + by exists (Gpoint mx my); rewrite //= !addrK -!lezD1 ubx0 lbx1 uby0 lby1. have lt_approx u v mu mv: ap_s1 u mu -> ap_s1 v mv -> (mu + 1 <= mv)%R -> u < v. case=> _ ubu [lbv _] ltuv; apply/(leR_pmul2l v u es1gt0)/(ltR_le_trans ubu). by apply: leR_trans lbv; rewrite -intRD1; apply/intR_leP. -case=> x2 y2 [[mx2 my2] [Dmx2 Dmy2]] /=; rewrite -andbA -!lez_addr1 => /and4P[]. +case=> x2 y2 [[mx2 my2] [Dmx2 Dmy2]] /=; rewrite -andbA -!lezD1 => /and4P[]. move=> /(le_trans lbx0)/lt_approx-lbx /le_trans/(_ ubx1)/lt_approx-ubx. move=> /(le_trans lby0)/lt_approx-lby /le_trans/(_ uby1)/lt_approx-uby. by do 2!split; [apply/lbx | apply/ubx | apply/lby | apply/uby]. @@ -291,7 +291,7 @@ rewrite -(leR_pmul2l _ x1 sXgt0) -(leR_pmul2l x1 _ sXgt0) !sZK => lbx1 ubx1 []. rewrite -(leR_pmul2l _ y1 sXgt0) -(leR_pmul2l y1 _ sXgt0) !sZK => lby1 uby1. have [p1 Dp1] := approx_point_exists s (Point x1 y1); exists p1 => //. case: p1 Dp1 => [p1x p1y] [[ubp1x lbp1x] [ubp1y lbp1y]] /=. -rewrite -!(rwP andP) -!ltz_addr1 -!lez_addr1 -!(rwP (@intR_ltP R _ _)). +rewrite -!(rwP andP) -!ltzD1 -!lezD1 -!(rwP (@intR_ltP R _ _)). rewrite (intRD1 R p1x) (intRD1 R p1y) -/intRR; split. by split; [apply: ltR_trans lbp1x | apply: leR_lt_trans ubx1]. by split; [apply: ltR_trans lbp1y | apply: leR_lt_trans uby1]. diff --git a/theories/cfmap.v b/theories/cfmap.v index dc8b3ba..97aab01 100644 --- a/theories/cfmap.v +++ b/theories/cfmap.v @@ -507,7 +507,7 @@ HB.instance Definition _ (A : choiceType) := Choice.copy (ecp_dart A) HB.instance Definition _ (A : countType) := Countable.copy (ecp_dart A) (can_type (@ecp_cancel A)). HB.instance Definition _ (A : finType) : isFinite (ecp_dart A) := - CanFinMixin (@ecp_cancel A). + CanIsFinite (@ecp_cancel A). Lemma card_ecp (A : finType) : #|ecp_dart A| = #|A|.+2. Proof. diff --git a/theories/chromogram.v b/theories/chromogram.v index 42ee07d..ac3f861 100644 --- a/theories/chromogram.v +++ b/theories/chromogram.v @@ -72,7 +72,7 @@ Proof. by do 2!case; constructor. Qed. HB.instance Definition _ := hasDecEq.Build gram_symbol eqgsP. Definition chromogram : predArgType := seq gram_symbol. -Canonical chromogram_eqType := [eqType of chromogram]. +HB.instance Definition _ := Equality.on chromogram. Fixpoint gram_balanced d b0 (w : chromogram) {struct w} := match w, d with diff --git a/theories/color.v b/theories/color.v index 5c8a5d9..bccde5a 100644 --- a/theories/color.v +++ b/theories/color.v @@ -214,7 +214,7 @@ Proof. by case: c => // _ []. Qed. (* Boolean correctness predicate *) Definition colseq : predArgType := seq color. -Canonical colseq_eqType := [eqType of colseq]. +HB.instance Definition _ := Equality.on colseq. Definition head_color : colseq -> color := head Color0. diff --git a/theories/coloring.v b/theories/coloring.v index 9a7038d..13e01d5 100644 --- a/theories/coloring.v +++ b/theories/coloring.v @@ -241,7 +241,7 @@ have nnx: node (node x) = x. rewrite (cardD1 x) (cardD1 (node x)) (cardD1 (node (node x))) !inE. by rewrite (inj_eq nodeI) x'nx x'n2x -!cnode1r connect0. pose G' := WalkupE x; pose h' (u : G') := val u. -pose unx : G' := sub (node x) x'nx; pose G'' := WalkupE unx. +pose unx : G' := Sub (node x) x'nx; pose G'' := WalkupE unx. pose h'' (w : G'') := val w; pose h := h' (h'' _). have Ih': injective h' := val_inj; have Ih'': injective h'' := val_inj. have Ih: injective h := inj_comp Ih' Ih''. @@ -262,7 +262,7 @@ have oE_G'' w: order edge w = #|predD1 (cedge (h'' w)) unx|. rewrite /order -(card_image Ih''); apply: eq_card => u; rewrite inE /=. have [u_nx | nx'u] := altP eqP. by apply/imageP => [[wu _ u_wu]]; case/eqP: (valP wu); rewrite -[RHS]u_nx. - set wu : G'' := sub u nx'u; rewrite (mem_image Ih'' _ wu) /=. + set wu : G'' := Sub u nx'u; rewrite (mem_image Ih'' _ wu) /=. apply: etrans (eq_fconnect (glink_fp_skip_edge _) w wu) _. by rewrite /glink /= -!val_eqE /= nnx !eqxx /= orbT. exact: (fconnect_skip edgeI w wu). @@ -280,7 +280,7 @@ have [|k [kE kF]] := minimal_counter_example_is_minimal cexG _ ltG''G. have [/negPf Eu'x Eu'nx] := norP Eu'Nx; rewrite /= orbF in Eu'nx. apply/eqP; apply: eq_card => y. have [-> {y} | x'y] := eqVneq y x; last first. - pose v : G' := sub y x'y; rewrite (mem_image Ih' _ v) !inE. + pose v : G' := Sub y x'y; rewrite (mem_image Ih' _ v) !inE. case: eqP => [[ynx] | _]; last exact (same_cskip_edge Eu'Nx). by apply/esym/(contraNF _ Eu'nx) => wEy; rewrite /= -ynx. rewrite [x \in cedge _]Eu'x; apply/imageP=> [[[z x'z] _ /= zx]]. @@ -300,13 +300,13 @@ have [|k [kE kF]] := minimal_counter_example_is_minimal cexG _ ltG''G. rewrite (cardD1 x) !inE connect0 eqSS /order -(card_image Ih'). apply/eqP/esym/eq_card => y; rewrite !inE; have [-> | x'y] /= := altP eqP. by apply/imageP=> [[[z x'z] _ /esym/eqP/idPn]]. - set v : G' := sub y x'y; rewrite (mem_image Ih' _ v). + set v : G' := Sub y x'y; rewrite (mem_image Ih' _ v). by apply: (etrans (cskip_edge_merge x'Enx EuNx)); rewrite /= orbF !(cedgeC y). case: (minimal_counter_example_is_noncolorable cexG). pose a' x w := cface x (h w). have a'0P y: a' y =1 pred0 -> pred2 x (node x) y. - move=> a'y0; apply/norP => [[x'y nx'y]]; pose uy : G' := sub y x'y. - by case/idP: (a'y0 ((sub uy : _ -> G'') nx'y)); apply: connect0. + move=> a'y0; apply/norP => [[x'y nx'y]]; pose uy : G' := Sub y x'y. + by case/idP: (a'y0 ((Sub uy : _ -> G'') nx'y)); apply: connect0. have a'F y z: a' y =1 pred0 -> cface y z -> y = z. move=> a'y0 yFz; suffices: pred2 y (node y) z. by case/pred2P=> // zny; rewrite -[y]nodeK -zny -cface1 cfaceC F'eG in yFz. @@ -323,7 +323,7 @@ have k'F y z: cface y z -> k' y = k' z. rewrite /a' (same_cface yFz) in yFw; case: pickP => [w' zFw' | /(_ w)/idP//]. by apply: kFF; rewrite hF -(same_cface yFw). have k'E y: ~~ (pred2 x (node x) y) -> k' y != k' (edge y). - case/norP=> [x'y nx'y]; pose w := (sub (sub y x'y : G') : _ -> G'') nx'y. + case/norP=> [x'y nx'y]; pose w := (Sub (Sub y x'y : G') : _ -> G'') nx'y. have Dfey: (face (edge y) = h (face (edge w))). by apply: nodeI; rewrite -hN1 !edgeK. rewrite (k'F (edge y) _ (fconnect1 _ _)) /k'. diff --git a/theories/contract.v b/theories/contract.v index dfb124b..8fcf8c9 100644 --- a/theories/contract.v +++ b/theories/contract.v @@ -266,14 +266,14 @@ have D_E0 (y : G0): cedge x y = (y == x) || (y == edge x). pose G1 := WalkupF x; pose h1 (u : G1) : G0 := val u. have Ih1: injective h1 by apply: val_inj. have x'ex: edge x != x by rewrite (plain_neq geoG0). -pose uex : G1 := sub (edge x) x'ex. +pose uex : G1 := Sub (edge x) x'ex. pose G2 := WalkupF uex; pose h2 (w : G2) : G1 := val w. have Ih2: injective h2 by apply: val_inj. pose h w := h1 (h2 w); have Ih: injective h := inj_comp Ih1 Ih2. have Eh: codom h =i predC (cedge x). move=> y; rewrite inE D_E0; apply/imageP/norP => [[w _ ->] | [x'y ex'y]]. by rewrite (valP w) (valP (val w)). - by exists ((sub (sub y x'y : G1) : _ -> G2) ex'y). + by exists ((Sub (Sub y x'y : G1) : _ -> G2) ex'y). have xE'h w: cedge x (h w) = false. by apply: negPf; rewrite -[~~ _]Eh codom_f. have hN w w': cnode w w' = cnode (h w) (h w') by rewrite !fconnect_skip. diff --git a/theories/cube.v b/theories/cube.v index 472ff2d..254630c 100644 --- a/theories/cube.v +++ b/theories/cube.v @@ -40,8 +40,8 @@ HB.instance Definition _ := Countable.copy cube_tag (can_type cube_tag_codeK). Fact cube_tag_enumP : Finite.axiom cube_tag_enum. Proof. by case. Qed. HB.instance Definition _ := isFinite.Build cube_tag cube_tag_enumP. -Definition cube_dart := cube_tag * G : Type. -HB.instance Definition _ := Finite.copy cube_dart [finType of cube_dart]. +Definition cube_dart : Type := cube_tag * G. +HB.instance Definition _ := Finite.on cube_dart. Let tsI : cube_tag -> G -> cube_dart := @pair _ _. Let tsE (u : cube_dart) : G := u.2. diff --git a/theories/dedekind.v b/theories/dedekind.v index 488e7c9..af3722c 100644 --- a/theories/dedekind.v +++ b/theories/dedekind.v @@ -150,7 +150,7 @@ Qed. Fact lt_is_cut a : is_cut {b | a < b}%R. Proof. split=> [||b c /lt_trans| b /midf_lt[ltac ltcb]]; last 2 [exact]. -- by exists (a + 1)%R; rewrite ltr_addl. +- by exists (a + 1)%R; rewrite ltrDl. - by exists a; rewrite ltxx. by exists ((a + b) / 2%:R)%R. Qed. @@ -273,11 +273,11 @@ Definition opp_cut x := {a | exists2 b, (- a < b)%R & x >= b}. Fact opp_is_cut x : is_cut (opp_cut x). Proof. split=> [||a b [c lt_na_c lecx] | a [b /(@open (- a)%R)[c lt_na_c ltcb] lebx]]. -- by have [a leax] := cut_lb x; exists (1 - a)%R, a; rewrite // opprB gtr_addl. +- by have [a leax] := cut_lb x; exists (1 - a)%R, a; rewrite // opprB gtrDl. - have [a ltxa] := cut_ub x; exists (- a)%R => -[b ltab []]. by apply: ltc_trans ltab; rewrite opprK. -- by exists c; first by apply: lt_trans lt_na_c; rewrite ltr_opp2. -by exists (- c)%R; [exists b; rewrite ?opprK | rewrite ltr_oppl]. +- by exists c; first by apply: lt_trans lt_na_c; rewrite ltrN2. +by exists (- c)%R; [exists b; rewrite ?opprK | rewrite ltrNl]. Qed. Definition opp x := Cut (opp_is_cut x). @@ -299,8 +299,8 @@ Proof. by move=> IHopp IHpos x; case: (ltcP x 0) gec0_opp; auto. Qed. Lemma oppK x : - (- x) == x. Proof. split=> [a /open[b ltxb ltba] | a [b lt_na_b le_b_nx]]. - by exists (- b)%R => [|[c]]; rewrite ?ltr_opp2 ?opprK => // /(ltc_trans ltxb). -by apply/notK=> leax; case: le_b_nx; exists a; rewrite // ltr_oppl. + by exists (- b)%R => [|[c]]; rewrite ?ltrN2 ?opprK => // /(ltc_trans ltxb). +by apply/notK=> leax; case: le_b_nx; exists a; rewrite // ltrNl. Qed. Lemma eqR_opp2 x y : opp x == opp y -> x == y. @@ -355,9 +355,9 @@ split=> [|| a b [c ltxc ltyac] ltab | a [b ltxb /open[c ltyc ltcab]]]. by exists (b + a)%R, a; rewrite ?addrK. - have [[a leax] [b /leRq-leby]] := (cut_lb x, cut_lb y). exists (b + a)%R => -[c ltxc /leby]. - by rewrite ltcE ltr_subr_addr ltr_add2l => /(ltc_trans ltxc). -- by exists c => //; apply: ltc_trans ltyac _; rewrite ltr_add2r. -by exists (c + b)%R; [exists b; rewrite ?addrK | rewrite -ltr_subr_addr]. + by rewrite ltcE ltrBrDr ltrD2l => /(ltc_trans ltxc). +- by exists c => //; apply: ltc_trans ltyac _; rewrite ltrD2r. +by exists (c + b)%R; [exists b; rewrite ?addrK | rewrite -ltrBrDr]. Qed. @@ -390,24 +390,24 @@ Qed. Lemma addN x : x - x == 0. Proof. apply eqR_sym; split=> [c [a ltxa [b lt_ac_b /leRq-lebx]] | d d_gt0]. - by rewrite ltcE -(ltr_addr (- a)) ltr_oppl (lt_trans lt_ac_b) ?lebx. + by rewrite ltcE -(ltrDr (- a)) ltrNl (lt_trans lt_ac_b) ?lebx. have [[a ltxa] [b lebx]] := (cut_ub x, cut_lb x). have{a ltxa d_gt0} []: exists n, x < b + d *+ n. have ltab: (0 < a - b)%R by move/leRq in lebx; rewrite subr_gt0 lebx. pose c := ((a - b) / d)%R; have c_ge0: (0 <= c)%R by rewrite ltW ?divr_gt0. - exists `|numq c|%N; apply: ltc_le_trans ltxa _; rewrite -ler_subl_addl. + exists `|numq c|%N; apply: ltc_le_trans ltxa _; rewrite -lerBlDl. rewrite pmulrn gez0_abs -?ge_rat0 // -mulrzl numqE mulrAC. - by rewrite divfK ?gt_eqF ?ler_pmulr // ler1z -gtz0_ge1 denq_gt0. + by rewrite divfK ?gt_eqF ?ler_pMr // ler1z -gtz0_ge1 denq_gt0. elim=> [|n IHn]; rewrite ?addr0 // mulrSr => /open[a ltxa lt_a_dnd]. have [/IHn//| le_bdn_x] := classical (x < b + d *+ n). -by exists a => //; exists (b + d *+ n)%R; rewrite // opprB ltr_subl_addr -addrA. +by exists a => //; exists (b + d *+ n)%R; rewrite // opprB ltrBlDr -addrA. Qed. Lemma add0 x : 0 + x == x. Proof. split=> [a /open[b ltxb ltba] | a [b b_gt0] ltxab]. by exists (a - b)%R; [rewrite ltcE subr_gt0 | rewrite opprD opprK addNKr]. -by apply: ltc_trans ltxab _; rewrite gtr_addl oppr_lt0. +by apply: ltc_trans ltxab _; rewrite gtrDl oppr_lt0. Qed. Lemma opp0 : - 0 == 0. Proof. by rewrite -[opp 0]add0 addN. Qed. @@ -432,9 +432,9 @@ split=> [|| a b [c ltxc ltyac] ltab | a [b ltxb /open[c ltyc ltcab]]]. by exists (b * a)%R, a; rewrite ?mulfK ?gt_eqF // (abs_ge0 ltxa). - by exists 0%R => -[a _ /abs_ge0]; rewrite mul0r ltcE ltxx. - exists c => //; have c_gt0: 0 < c := abs_ge0 ltxc. - by apply: ltc_trans ltyac _; rewrite ltr_pmul2r ?invr_gt0. + by apply: ltc_trans ltyac _; rewrite ltr_pM2r ?invr_gt0. have b_gt0: 0 < b := abs_ge0 ltxb. -by exists (c * b)%R; first exists b; rewrite -?ltr_pdivl_mulr ?mulfK ?gt_eqF. +by exists (c * b)%R; first exists b; rewrite -?ltr_pdivlMr ?mulfK ?gt_eqF. Qed. Definition amul x y := Cut (amul_is_cut x y). @@ -463,7 +463,7 @@ Lemma amulC x y : `|x|*|y| == `|y|*|x|. Proof. without loss suffices: x y / `|y|*|x| <= `|x|*|y| by []. move=> b [a ltxa ltyba]; exists (b / a)%R; rewrite // invf_div mulrC divfK //. -by rewrite gt_eqF // -(mul0r a) -ltr_pdivl_mulr (abs_ge0 ltxa, abs_ge0 ltyba). +by rewrite gt_eqF // -(mul0r a) -ltr_pdivlMr (abs_ge0 ltxa, abs_ge0 ltyba). Qed. Lemma amulA x y z : `|x|*|`|y|*|z| | == `| `|x|*|y| |*|z|. @@ -537,8 +537,8 @@ have dgt0: 0 < d by move/leR0y: lty_da1; rewrite ltcE pmulr_lgt0 ?invr_gt0. have cdgt0: 0 < c - d. by move/leR0z: ltz_cda2; rewrite ltcE pmulr_lgt0 ?invr_gt0. exists a; rewrite // (ge0_abs le0yz); exists (d / a)%R; last rewrite -mulrBl. - by apply: ltc_le_trans lty_da1 _; rewrite ler_pmul2l ?lef_pinv. -by apply: ltc_le_trans ltz_cda2 _; rewrite ler_pmul2l ?lef_pinv. + by apply: ltc_le_trans lty_da1 _; rewrite ler_pM2l ?lef_pV2. +by apply: ltc_le_trans ltz_cda2 _; rewrite ler_pM2l ?lef_pV2. Qed. Lemma mul1 x : 1 * x == x. @@ -547,11 +547,11 @@ elim/opp_ind: x => [x IHx | x le0x]. by apply eqR_opp2; rewrite -IHx mulRN. rewrite ge0_mul //; split=> [b /open[a ltxa ltab] | b [a [lt1a _] ltxba]]. have a_gt0: 0 < a by apply/leRq: (a) ltxa. - by rewrite amulC; exists a; rewrite ge0_abs // ltcE ltr_pdivl_mulr ?mul1r. + by rewrite amulC; exists a; rewrite ge0_abs // ltcE ltr_pdivlMr ?mul1r. have a_gt0: 0 < a by apply: lt_trans lt1a. -have b_gt0: 0 < b by rewrite ltcE -(mul0r a) -ltr_pdivl_mulr ?(abs_ge0 ltxba). +have b_gt0: 0 < b by rewrite ltcE -(mul0r a) -ltr_pdivlMr ?(abs_ge0 ltxba). rewrite -[x]ge0_abs //; apply: ltc_trans ltxba _. -by rewrite gtr_pmulr ?invf_lt1. +by rewrite gtr_pMr ?invf_lt1. Qed. Lemma mul_monotony x y z : 0 <= x -> y <= z -> x * y <= x * z. @@ -601,15 +601,15 @@ pose E z := `|x|*|z| < 1; have E_0: E 0 by rewrite /E amulC amul0. have supE: has_sup E. split; [by exists 0 | exists a^-1%R => //]. move=> z [b ltxb [lt_z_vb _]]; apply/ltcW/(ltc_trans lt_z_vb). - by rewrite mul1r (ltf_pinv (abs_ge0 ltxb)) ?(gec_lt_trans _ ltxb) // => -[]. + by rewrite mul1r (ltf_pV2 (abs_ge0 ltxb)) ?(gec_lt_trans _ ltxb) // => -[]. have ubEy: ub E y by apply: sup_ub. have le0y: y >= 0 by apply/leRq/ubEy. rewrite ge0_mul //; split=> [b lt1b | b [c ltxc [ltybc _]]]; last first. have [d ltxd ltdc] := open ltxc. have [c_gt0 d_gt0] := (abs_ge0 ltxc, abs_ge0 ltxd). - suffices: (1 / c < b / c)%R by rewrite ltr_pmul2r ?invr_gt0. + suffices: (1 / c < b / c)%R by rewrite ltr_pM2r ?invr_gt0. apply: gec_lt_trans ltybc; apply/leRq/ubEy; exists d => //. - by rewrite !mul1r ge0_abs ltcE ?ltf_pinv // lt_gtF ?invr_gt0. + by rewrite !mul1r ge0_abs ltcE ?ltf_pV2 // lt_gtF ?invr_gt0. have lt0b: 0 < b by apply: lt_trans lt1b. pose e := (1 - b^-1)%R; have lt0e: 0 < e by rewrite ltcE subr_gt0 invf_lt1. have [c ltxc [d lt_cea_d ledx]]: x - x < a * e by rewrite addN ltcE mulr_gt0. @@ -617,13 +617,13 @@ have ltac: a < c := gec_lt_trans leax ltxc. have lt0c: 0 < c := lt_trans lt0a ltac. have lt0d: 0 < d. apply: lt_trans lt_cea_d; rewrite opprB subr_gt0 mulrBr mulr1. - by rewrite ltr_snsaddr // oppr_lt0 divr_gt0. + by rewrite ltr_nDr // oppr_lt0 divr_gt0. have le_y_vd: y <= d^-1%R. apply/sup_le_ub=> // z -[f ltxf [lt_z_vf _]]; apply/ltcW/(ltc_trans lt_z_vf). - by rewrite mul1r (ltf_pinv (abs_ge0 ltxf)) ?(gec_lt_trans _ ltxf) // => -[]. + by rewrite mul1r (ltf_pV2 (abs_ge0 ltxf)) ?(gec_lt_trans _ ltxf) // => -[]. exists c; rewrite ge0_abs //; apply: le_y_vd; rewrite ltcE. -rewrite -invf_div ltf_pinv ?rpred_div //; apply: lt_trans lt_cea_d. -by rewrite ltr_oppr -[c in (_ - c)%R]mulr1 ltr_subl_addl -mulrBr ltr_pmul2r. +rewrite -invf_div ltf_pV2 ?rpred_div //; apply: lt_trans lt_cea_d. +by rewrite ltrNr -[c in (_ - c)%R]mulr1 ltrBlDl -mulrBr ltr_pM2r. Qed. Definition structure := Real.Structure leR sup add 0 opp mul 1 inv. diff --git a/theories/discharge.v b/theories/discharge.v index 47fba5d..e62f78a 100644 --- a/theories/discharge.v +++ b/theories/discharge.v @@ -357,7 +357,7 @@ Proof. by rewrite sort_dbound1_eq; case: (sort_drules p r). Qed. Lemma dbound2_leq : dscore2 (face (face x)) <= dbound2 rt rs x. Proof. -rewrite /dbound2 -dbound1_eq ler_add2r lez_nat. +rewrite /dbound2 -dbound1_eq lerD2r lez_nat. set y := inv_face2 _; rewrite /rt /target_drules; case: rf => _ _ []. elim: the_drules => //= r dr IHdr; case Dr': (converse_part r) => [u r']. case Hyr: (exact_fitp y r). @@ -382,10 +382,10 @@ move=> ub_m x pos_x d max_m; apply: contraLR pos_x; rewrite -leqNgt => ledx. have ltm10: (m < 10)%N by rewrite -subn_gt0; case: (10 - m)%N max_m. have{max_m}: 60%:Z <= ((10 - m) * arity x)%:Z. by rewrite lez_nat (leq_trans max_m) ?leq_mul. -rewrite -leNgt -ler_subr_addr ler_subl_addl add0r => /le_trans-> //. +rewrite -leNgt -lerBrDr lerBlDl add0r => /le_trans-> //. rewrite !PoszM -!mulrzz -![_ *~ _]sumr_const -sumrB ler_sum // => y _. -rewrite -(ler_add2r m%:Z) -PoszD subnK 1?ltnW // addrAC. -by rewrite ler_subr_addr ler_add2l ler_subl_addr ler_paddr. +rewrite -(lerD2r m%:Z) -PoszD subnK 1?ltnW // addrAC. +by rewrite lerBrDr lerD2l lerBlDr ler_wpDr. Qed. Lemma source_drules_range : ~~ Pr58 nhub -> rs = [::]. @@ -401,7 +401,7 @@ Lemma dscore_cap2 (x : G) : arity x = nhub -> 0 < dscore x -> 0 < dboundK + \sum_(y in cface x) dbound2 rt rs y. Proof. -move=> nFx /lt_le_trans-> //; rewrite /dscore -dboundK_eq // ler_add2l. +move=> nFx /lt_le_trans-> //; rewrite /dscore -dboundK_eq // lerD2l. do 2!rewrite (reindex_inj faceI) -(eq_bigl _ _ (fun y => cface1r y x)) /=. by apply: ler_sum => y xFy; rewrite dbound2_leq // -(arity_cface xFy). Qed. diff --git a/theories/discretize.v b/theories/discretize.v index bcdcab0..8106e5e 100644 --- a/theories/discretize.v +++ b/theories/discretize.v @@ -86,7 +86,7 @@ Proof. have [_ [k [mr0 sm0r0]]] := fin_m0; pose mr0k : map_repr k := mr0. suffices{sm0r0} [n [mr mrP sr0mr]]: exists n, exists2 mr : map_repr n, mr_proper mr & subregion (mr_cover mr0k) (mr_cover mr). -- by exists n, mr => // z /sm0r0[i /ltP-lti ?]; apply/sr0mr; exists (sub i lti). +- by exists n, mr => // z /sm0r0[i /ltP-lti ?]; apply/sr0mr; exists (Sub i lti). elim: k @mr0k => [|k [n [mr mrP]] sr0mr]; last pose t := mr0 k. by exists 0, (fun=> mr0 0) => [|z []] []. have [mr_t | mr't] := Rclassic (cover m0 t -> mr_cover mr t). @@ -404,5 +404,3 @@ by do [exists u; do 2!split=> //]; [apply: m0tr_cl m0zu | apply: m0tr_cl m0tu]. Qed. End DiscretizeMap. - - diff --git a/theories/embed.v b/theories/embed.v index 4fd10d9..5558b1a 100644 --- a/theories/embed.v +++ b/theories/embed.v @@ -1101,9 +1101,9 @@ rewrite /embd_face; case: ifP (edge_perimeter (face (val u))) => //= _. by rewrite inE /= (canRL edgeK (e2c _)) -(fclosed1 rcN). Qed. -Let dedge u : ddart := sub (embd_edge (val u)) (embd_edge_subproof u). -Let dnode u : ddart := sub (node (val u)) (embd_node_subproof u). -Let dface u : ddart := sub (embd_face (val u)) (embd_face_subproof u). +Let dedge u : ddart := Sub (embd_edge (val u)) (embd_edge_subproof u). +Let dnode u : ddart := Sub (node (val u)) (embd_node_subproof u). +Let dface u : ddart := Sub (embd_face (val u)) (embd_face_subproof u). Fact embed_disk_subproof : cancel3 dedge dnode dface. Proof. @@ -1121,7 +1121,7 @@ Lemma embd_inj : injective embd. Proof. exact: val_inj. Qed. Lemma codom_embd : codom embd =i bc. Proof. move=> x; apply/imageP/idP => [[u _ ->] | bc_x]; first exact: (valP u). -by exists (sub x bc_x). +by exists (Sub x bc_x). Qed. Definition embd_ring : seq Gd := preim_seq embd erc. @@ -1219,9 +1219,9 @@ rewrite [_ \in _](contraR _ (embr_edge_subproof w)) ?Dew //. by rewrite (mem_image embdd_inj). Qed. -Let redge w : rdart := sub (edge (val w)) (embr_edge_subproof w). -Let rnode w : rdart := sub (embr_node (val w)) (embr_node_subproof w). -Let rface w : rdart := sub (embr_face (val w)) (embr_face_subproof w). +Let redge w : rdart := Sub (edge (val w)) (embr_edge_subproof w). +Let rnode w : rdart := Sub (embr_node (val w)) (embr_node_subproof w). +Let rface w : rdart := Sub (embr_face (val w)) (embr_face_subproof w). Fact embed_rem_subproof : cancel3 redge rnode rface. Proof. @@ -1244,7 +1244,7 @@ Lemma embr_inj : injective embr. Proof. exact: val_inj. Qed. Lemma codom_embr : codom embr =i [predC rdom']. Proof. move=> x; apply/imageP/idP=> [[w _ ->] | bG'x]; first exact: (valP w). -by exists (sub x bG'x). +by exists (Sub x bG'x). Qed. Definition embr_ring : seq Gr := preim_seq embr (rev (map embdd embd_ring)). diff --git a/theories/grid.v b/theories/grid.v index 406536b..d07d27c 100644 --- a/theories/grid.v +++ b/theories/grid.v @@ -322,7 +322,7 @@ Definition extend_grect p r := Lemma in_extend_grect p (r : grect) : subpred (predU1 p r) (extend_grect p r). Proof. case: r p => x0 x2 y0 y2 [x1 y1] [x y] /predU1P[->|] /=. - by rewrite !leIx !ltxU !lexx !ltr_addl !orbT. + by rewrite !leIx !ltxU !lexx !ltrDl !orbT. by rewrite !leIx !ltxU -andbA => /and4P[-> -> -> ->]. Qed. @@ -352,10 +352,10 @@ Proof. by case: r => x0 x1 y0 y1; rewrite size_allpairs !size_zspan. Qed. Lemma mem_zspan xmin xmax x : (x \in zspan xmin xmax) = (xmin <= x < xmax). Proof. -rewrite -[xmax in RHS](subrK xmin) -ltr_subl_addr -subr_ge0 /zspan /zwidth. +rewrite -[xmax in RHS](subrK xmin) -ltrBlDr -subr_ge0 /zspan /zwidth. case: {xmax}(xmax - xmin) => n; last by case: (x - xmin). elim: n xmin => [|n IHn] x0; first by rewrite ltNge andbN. -rewrite inE -subr_eq0 {}IHn opprD addrA ler_subr_addl ltr_subl_addl. +rewrite inE -subr_eq0 {}IHn opprD addrA lerBrDl ltrBlDl. by rewrite orb_andr eq_sym -le_eqVlt; case: eqP => // <-. Qed. @@ -376,7 +376,7 @@ Proof. rewrite /zspan /zwidth; case: {xmax}(xmax - xmin) => -[|n] //. apply/(sorted_uniq lt_trans ltxx)=> /=; set w := traject _ _ _. have: fpath (+%R^~ 1) xmin w by apply: fpath_traject. -by apply/sub_path=> x _ /eqP<-; rewrite ltr_addl. +by apply/sub_path=> x _ /eqP<-; rewrite ltrDl. Qed. Lemma enum_grect_uniq r : uniq (enum_grect r). @@ -416,18 +416,18 @@ by do 2![case/andP=> /(le_trans _)-> // /lt_le_trans-> //]. Qed. Lemma gtouch_l p : subpred (ltouch p) (gtouch p). -Proof. by case: p => x y; apply/subgrectE; rewrite !ler_add2l. Qed. +Proof. by case: p => x y; apply/subgrectE; rewrite !lerD2l. Qed. Lemma ltouch_refl q : ltouch q q. -Proof. by case: q => x y; rewrite /= !ger_addl !ltr_addl. Qed. +Proof. by case: q => x y; rewrite /= !gerDl !ltrDl. Qed. Lemma gtouch_refl p : gtouch p p. -Proof. by case: p => x y; rewrite /= !ger_addl !ltr_addl. Qed. +Proof. by case: p => x y; rewrite /= !gerDl !ltrDl. Qed. Lemma gtouch_edge d : gtouch (halfg d) (halfg (gedge d)). Proof. rewrite halfg_edge; case: (halfg d) => x y. -by case: oddgP; rewrite /= !ler_add2l !ltr_add2l. +by case: oddgP; rewrite /= !lerD2l !ltrD2l. Qed. (* Explicit computation of gtouch and ltouch enumeration. *) @@ -441,11 +441,11 @@ Definition inset r := Lemma insetP (r : grect) p : reflect (subpred (gtouch p) r) (inset r p). Proof. -case: r p => x0 x1 y0 y1 [x y]; rewrite /= -andbA -!ler_subr_addr. +case: r p => x0 x1 y0 y1 [x y]; rewrite /= -andbA -!lerBrDr. apply/(iffP and4P)=> [[lbx ubx lby uby] | r1x]. - by apply/subgrectE; rewrite !(addrA _ 1 1) !lez_addr1 -!ltr_subr_addr. -rewrite !ltr_subr_addr; have r1dx z := r1x (Gpoint (x + z) (y + z)). -have [] := (r1dx 1, r1dx (-1)); rewrite /= !ler_add2l !ltr_add2l. + by apply/subgrectE; rewrite !(addrA _ 1 1) !lezD1 -!ltrBrDr. +rewrite !ltrBrDr; have r1dx z := r1x (Gpoint (x + z) (y + z)). +have [] := (r1dx 1, r1dx (-1)); rewrite /= !lerD2l !ltrD2l. by do ![case/implyP/andP | case/andP=> ? ?]. Qed. @@ -468,7 +468,7 @@ Proof. by move <-; apply: gchop_halfg. Qed. Lemma gchop_edge d p : gchop (gedge d) p = ~~ gchop d p. Proof. rewrite /gchop halfg_edge oddg_edge; case: (halfg d) p => x0 y0 [x y] /=. -by case: oddgP; rewrite /= -!ltNge ?lez_addr1 // -ltz_addr1 addrK. +by case: oddgP; rewrite /= -!ltNge ?lezD1 // -ltzD1 addrK. Qed. Lemma gchop_face_node d : gchop (gface (gnode d)) = gchop (gface (gface d)). @@ -488,7 +488,7 @@ Lemma gchop_chop1 d : subpred (gchop d) (gchop1 d). Proof. rewrite /gchop1 /gchop !halfg_face halfg_edge !oddg_face oddg_edge ccw4. case: (halfg d) => x0 y0 [x y]. -by case: oddgP => /= d_p; rewrite ltW // -?ltr_subr_addr ltz_addr1. +by case: oddgP => /= d_p; rewrite ltW // -?ltrBrDr ltzD1. Qed. Lemma gtouch_chop1 d p : @@ -496,8 +496,8 @@ Lemma gtouch_chop1 d p : Proof. case: p => x y; rewrite /= andbT /gchop1 /gchop !(halfg_face, halfg_edge). case: (halfg d) => x0 y0; rewrite !(oddg_face, oddg_edge) !ccw4 /=. -rewrite !(addrA _ 1 1) !ltz_addr1. -by case: oddgP; rewrite /= -andbA -?ler_subr_addr; do !bool_congr. +rewrite !(addrA _ 1 1) !ltzD1. +by case: oddgP; rewrite /= -andbA -?lerBrDr; do !bool_congr. Qed. Lemma gchop1_shift d : gchop1 (gface (gedge (gface d))) = gchop1 d. @@ -524,7 +524,7 @@ Definition gchop_rect d := Lemma in_gchop_rect d : gchop_rect d =1 predI r (gchop d). Proof. rewrite /gchop_rect /gchop; case: r (halfg d) => x0 x2 y0 y2 [x1 y1] [x y] /=. -case: oddgP; rewrite /= (leUx, ltxI) ?ltz_addr1 -!andbA; do !bool_congr. +case: oddgP; rewrite /= (leUx, ltxI) ?ltzD1 -!andbA; do !bool_congr. Qed. Lemma gchop_rect_sub d : subpred (gchop_rect d) r. @@ -535,11 +535,11 @@ Lemma gchop_rect_edge d : Proof. rewrite halfg_edge => r_ed [x y]; rewrite !in_gchop_rect /= gchop_halfg. rewrite /gchop; case: r (halfg d) => [x0 x2 y0 y2] [x1 y1] /= in r_ed *. -rewrite andbT -!andbA -!lez_addr1 => /and5P[lbx ubx lby uby]. -by case: oddgP r_ed; rewrite /= ?addr0 -andbA -!lez_addr1 ?subrK; +rewrite andbT -!andbA -!lezD1 => /and5P[lbx ubx lby uby]. +by case: oddgP r_ed; rewrite /= ?addr0 -andbA -!lezD1 ?subrK; case/and4P=> lbx1 ubx1 lby1 uby1 d_xy; apply/and4P; split=> //; - rewrite ?lez_addr1 ?(le_trans _ d_xy, le_lt_trans d_xy) -?lez_addr1 //; - apply/ltW; rewrite -lez_addr1 // -ler_subr_addr. + rewrite ?lezD1 ?(le_trans _ d_xy, le_lt_trans d_xy) -?lezD1 //; + apply/ltW; rewrite -lezD1 // -lerBrDr. Qed. Definition gchop1_rect d := gchop_rect (gface (gface (gedge d))). diff --git a/theories/gridmap.v b/theories/gridmap.v index 30e224f..0bd3a06 100644 --- a/theories/gridmap.v +++ b/theories/gridmap.v @@ -81,12 +81,12 @@ Definition cmatte := Ir -> matte. Implicit Types (e : adj_index) (ab : adjbox) (cm : cmatte). #[hnf] -HB.instance Definition _ := Finite.copy adj_index [finType of adj_index]. +HB.instance Definition _ := Finite.on adj_index. Coercion pair_of_adj_index e : Ir * Ir := val e. Coercion adj_incident e := pred2 e.1 e.2. -Definition AdjIndex i j ltij : adj_index := sub (i, j) ltij. +Definition AdjIndex i j ltij : adj_index := Sub (i, j) ltij. Definition cm_proper cm := forall i j, has (cm i) (cm j) -> i = j. @@ -208,8 +208,8 @@ have [w_gt0 h_gt0]: 0 < bbw%:Z /\ 0 < bbh%:Z; last split=> //. case: bb w_gt0 h_gt0 => x0 x1 y0 y1 /=; rewrite -[x1](subrK x0) -[y1](subrK y0). rewrite /zwidth /= !addrK; case: (_ - _) (_ - _) => h []w _ _ //. pose p0 := Gpoint x0 y0; exists p0 => [x y | p]. - by rewrite addrC /= !ltr_add2r !ler_addr. -rewrite -(subrK p0 p); case: (p - p0) => x y /=; rewrite !ler_addr !ltr_add2r. + by rewrite addrC /= !ltrD2r !lerDr. +rewrite -(subrK p0 p); case: (p - p0) => x y /=; rewrite !lerDr !ltrD2r. by case: x y => x [] y /andP[] //; exists x, y; first rewrite addrC. Qed. @@ -231,11 +231,11 @@ Proof. by rewrite !gmgridE gedge2 orbC. Qed. Definition gmdart : predArgType := seq_sub gmgrid. Coercion gmval := @ssval _ _ : gmdart -> gpoint. -Definition Gmdart d : d \in gmgrid -> gmdart := sub d. +Definition Gmdart d : d \in gmgrid -> gmdart := Sub d. Implicit Types u v w : gmdart. HB.instance Definition _ := [isSub of gmdart for gmval]. -HB.instance Definition _ := Finite.copy gmdart [finType of gmdart]. +HB.instance Definition _ := Finite.on gmdart. Definition gmedge u := Gmdart (etrans (gmgrid_edge u) (valP u)). Definition gmpick u s : gmdart := foldl insubd u s. @@ -313,15 +313,15 @@ move=> d; apply/imageP/flatten_mapP=> [[/= u G'u ->] | [c ltc /mapP[z ltz ->]]]. by rewrite /c mem_iota; case: oddgP. rewrite {}/c /bbd /bbp; congr ((p0 + _) *+ 2 + _); last by case: oddgP. case: oddgP G'u; rewrite bbE ?addr0 ?ubx ?uby /= ?andbT /h1 /w1; - do ?by rewrite andbC -lez_addr1 subrK ltW // subr_ge0 -eqn0Ngt => /eqP->. - - by have [/idPn||->] := ltrgtP bbh%:Z; rewrite ?addrK // -leNgt lez_addr1. - - by have [/idPn||->] := ltrgtP bbw%:Z; rewrite ?addrK // -leNgt lez_addr1. + do ?by rewrite andbC -lezD1 subrK ltW // subr_ge0 -eqn0Ngt => /eqP->. + - by have [/idPn||->] := ltrgtP bbh%:Z; rewrite ?addrK // -leNgt lezD1. + - by have [/idPn||->] := ltrgtP bbw%:Z; rewrite ?addrK // -leNgt lezD1. rewrite -[bbd c z]gedge2; set ed := gedge (bbd c z). suffices /andP[Ged]: (ed \in gmgrid) && ~~ bb (halfg ed) by exists (Gmdart Ged). rewrite mem_iota /= -ltz_nat in ltz; rewrite !inE in ltc. rewrite gmgridE andb_orl andbN gedge2 halfg_edge halfg_add2 oddg_add2 -!addrA. by case/or4P: ltc ltz => /eqP->; rewrite !bbE !addr0 ?addrK ?ltxx => ->; - rewrite ?gtr_addl !andbT ?subr_ge0. + rewrite ?gtrDl !andbT ?subr_ge0. Qed. Lemma cface_end0g u v : cface u v = (end0g u == end0g v). @@ -351,7 +351,7 @@ have gmendP (u : gmdart): end0g u - p0 \in gmframe. rewrite -halfg_face -[gface _]gnode4 gedgeK => bbn3u; have:= IHu (face u). by rewrite inE val_insubd gmgridE bbn3u !end0g_node => ->. rewrite /end0g {}Du addrC -addrA addKr mem_enum_grect !intS !(addrC 1). - by case: oddgP; rewrite /= ?addr0 ?ltr_add2r ?ltz_addr1 ?ltW ?ubx. + by case: oddgP; rewrite /= ?addr0 ?ltrD2r ?ltzD1 ?ltW ?ubx. pose gmend u := SeqSub (gmendP u). suffices adj_gmend: fun_adjunction gmend id face predT. rewrite -(adjunction_n_comp _ (fconnect_sym _) cfaceC _ adj_gmend) //. @@ -363,10 +363,10 @@ pose c := locked Gpoint (x == bbw) (y == bbh). suffices Gu: (p0 + (Gpoint x y - oddg c)) *+ 2 + oddg c \in gmgrid. exists (Gmdart Gu); rewrite fconnect_id -val_eqE /= addrCA -addrA -opprB. by rewrite halfg_eq ?oddg_eq ?subrK. -rewrite gmgridE halfg_eq //= {}/c -lock bbE !ltr_subl_addl !subr_ge0. +rewrite gmgridE halfg_eq //= {}/c -lock bbE !ltrBlDl !subr_ge0. apply/orP; left; apply/andP; move: Gxy; rewrite mem_enum_grect /=. -rewrite !intS !ltz_add1r (le_eqVlt x) (le_eqVlt y) => /andP[Gx Gy]. -by split; [move: Gx | move: Gy]; case: eqP => // -> _; rewrite ltr_addr andbT. +rewrite !intS !ltz1D (le_eqVlt x) (le_eqVlt y) => /andP[Gx Gy]. +by split; [move: Gx | move: Gy]; case: eqP => // -> _; rewrite ltrDr andbT. Qed. Lemma fcard_gmnode : (bbw * bbh <= fcard node gmdart_map)%N. @@ -376,7 +376,7 @@ rewrite -garea_refine_rect -size_enum_grect. rewrite -[n in n.*2]muln2 doubleMr (fcard_order_set nodeI _ gm_inner_closed). rewrite cardE -(size_map val) uniq_leq_size ?enum_grect_uniq // => d. rewrite mem_enum_grect in_refine_rect => bb_d. - by apply/imageP/(ex_intro2 _ _ (sub d _)); rewrite // gmgridE bb_d. + by apply/imageP/(ex_intro2 _ _ (Sub d _)); rewrite // gmgridE bb_d. apply/subsetP=> /= u bb_u; rewrite inE. have cyc_u: fcycle node (traject node u 4). rewrite [3%N]lock /= rcons_path fpath_traject -lock /= -val_eqE. diff --git a/theories/hubcap.v b/theories/hubcap.v index 751ec62..3f116f8 100644 --- a/theories/hubcap.v +++ b/theories/hubcap.v @@ -200,8 +200,8 @@ rewrite /rs0 /rt0 /source_drules /target_drules; case: rf => rs rt _. set ru : drules := [::]; have bound_ru: dbound1 ru x = 0 by []. have{rt} [dnt rt] := sort_drulesP fit_xp rt; move: (size rt + 2) => m. have{rs fit_xp} [dns rs] := sort_drulesP fit_xp rs. -rewrite ler_subl_addl addrAC !PoszD [rhs in (_ <= rhs)%R]addrAC. -rewrite -ler_subr_addl [rhs in (_ <= rhs)%R]addrAC. +rewrite lerBlDl addrAC !PoszD [rhs in (_ <= rhs)%R]addrAC. +rewrite -lerBrDl [rhs in (_ <= rhs)%R]addrAC. case: {dns dnt b}(_ - _)%R => // [nt]; rewrite -PoszD lez_nat. elim: m nt rt => // m IHm nt [|r rt] //= in rs (ru) bound_ru p Exp *. case: ifP => [lt_rt_nt _ | _ /andP[]]. @@ -266,7 +266,7 @@ have [_ fit_p2] := andP Exp2. have{rt} [dnt2 rt2] := sort_drulesP fit_p2 rt; move: (size rt1 + _) => m. have{fit_p2} [dns2 rs2] := sort_drulesP fit_p2 rs; rewrite !PoszD => b2p. rewrite addrACA -opprD addrACA [rhs in (- rhs)%R]addrACA opprD [leLHS]addrACA. -rewrite -ler_subr_addl opprB [rhs in (_ <= rhs)%R]addrC ler_subl_addl. +rewrite -lerBrDl opprB [rhs in (_ <= rhs)%R]addrC lerBlDl. case: {dns1 dns2 dnt1 dnt2 b}(_ + b)%R b2p => // nt; rewrite lez_nat. move: @x2 rt2 rs2 ru2 p2 b1ru2 Exp2 => /=. elim: m rt1 => // m IHm [|r rt1]/= in nt x1 i nFx1 ub_i rs1 ru1 p1 b1ru1 Exp1 *. @@ -389,7 +389,7 @@ have{v'0} db2v: {in cface x1, forall y1, db2 v y1 = b y1 2}. suffices{db2v}: ~~ (0 < b0 *+ 2 - 1 + sum_db2 v)%R. apply: contra => /(dscore_cap2 rf geoG nFx); rewrite -/rs0 -/rt0 -/b0. rewrite [sum_db2 _](eq_bigr _ db2v) sumrMnl (eq_bigl _ _ (same_cface x1Fx)). - by rewrite addrAC subr_gt0 -mulrnDl -!lez_add1r (ler_muln2r 2 1%:Z). + by rewrite addrAC subr_gt0 -mulrnDl -!lez1D (lerMn2r 2 1). pose vb w := forall i, nth 0 w i <= nth 0 v i. have vb_inc w i : vb (incr_nth w i) -> nth 0 w i < nth 0 v i /\ vb w. move=> vb_w; split=> [|j]; first by have:= vb_w i; rewrite nth_incr_nth eqxx. @@ -404,24 +404,24 @@ have db2_inc w i (v_i := nth 0 v i) (w' := incr_nth w i) : by do [rewrite -/v_i; case: eqP w_i => [->|_] [|[|?]]] in lt_wvi ub_wi *. apply: eq_bigr => y /andP[x1Fy x1i'y]; congr (_ *+ _)%R; rewrite nth_incr_nth. by have [Di | //] := i =P _; rewrite Di iter_findex ?eqxx in x1i'y. -have: vb v by []; rewrite /v -ltr_subl_addl sub0r -leNgt; clearbody v. +have: vb v by []; rewrite /v -ltrBlDl sub0r -leNgt; clearbody v. elim: hc {b0}(_ - 1)%R hc_v hc_p => /= [|i b1 hc IHhc|j i b1 hc IHhc] b0. - by rewrite -leNgt -oppr_ge0 [sum_db2 _]big1 // => y _; rewrite /db2 nth_nil. - case/andP=> /eqP-Dvi v_hc /andP[p_b1 p_hc] vb_hci. have /vb_inc[_ vb_hc] := vb_hci. have [ltin | leni] := ltnP i nhub; last by rewrite nth_default ?Ev in Dvi. - rewrite {}db2_inc ?Dvi {vb_hci}//= -ler_subr_addl -opprD addrC. + rewrite {}db2_inc ?Dvi {vb_hci}//= -lerBrDl -opprD addrC. apply: {IHhc vb_hc v_hc p_hc}(le_trans (IHhc _ v_hc p_hc vb_hc)). - rewrite ler_opp2 ler_add2r ler_pmuln2r //. + rewrite lerN2 lerD2r ler_pMn2r //. by apply: check_dbound2P p_b1; rewrite ?arity_iter_face ?fit_hubcap_rot. set vj := nth 0 v j => /and3P[/eqP-Dvi vj_le2] v_hc /andP[p_b1 p_hc] vb_hcij. have /vb_inc[_ vb_hcj] := vb_hcij; have /vb_inc[vj_gt vb_hc] := vb_hcj. have{vj_gt} vj_gt0: 0 < vj by apply: leq_trans vj_gt. have [ltin | ?] := ltnP i nhub; last by rewrite Dvi nth_default ?Ev in vj_gt0. have [ltjn | ?] := ltnP j nhub; last by rewrite [vj]nth_default ?Ev in vj_gt0. -rewrite !{}db2_inc -?Dvi {vb_hcij vb_hcj}//= addrA -ler_subr_addl -opprD -/vj. +rewrite !{}db2_inc -?Dvi {vb_hcij vb_hcj}//= addrA -lerBrDl -opprD -/vj. apply: {IHhc v_hc p_hc vb_hc}(le_trans (IHhc _ v_hc p_hc vb_hc)). -rewrite ler_opp2 addrC ler_add2r -mulrnDl ler_pmuln2r //. +rewrite lerN2 addrC lerD2r -mulrnDl ler_pMn2r //. rewrite addrC -(iter_hub_subn i ltjn) //. apply: check_2dbound2P p_b1; rewrite ?arity_iter_face ?hub_subn_hub //. by rewrite fit_hubcap_rot. diff --git a/theories/jordan.v b/theories/jordan.v index 79f537e..c816d8e 100644 --- a/theories/jordan.v +++ b/theories/jordan.v @@ -68,7 +68,7 @@ have IHe z := IHm (WalkupE z) (ltG'm z) (planar_WalkupE z planarG). have IHn z := IHm (WalkupN z) (ltG'm z) (planar_WalkupN z planarG). have{m IHm ltG'm} IHf z := IHm (WalkupF z) (ltG'm z) (planar_WalkupF z planarG). have injG z : injective (val : WalkupE z -> G) := val_inj. -pose ofG (z x : G) : x != z -> WalkupE z := sub x. +pose ofG (z x : G) : x != z -> WalkupE z := Sub x. have uniqG z := map_inj_uniq (injG z); have mem2G z := mem2_map (injG z). have clink_eq := sameP clinkP pred2P. pose map_cpath f x p := {q | (f q.1, map f q.2) = (x : G, p) & cpath q.1 q.2}. diff --git a/theories/kempe.v b/theories/kempe.v index ca5dfde..90a4e61 100644 --- a/theories/kempe.v +++ b/theories/kempe.v @@ -195,12 +195,12 @@ have defNz y: cnode z y = (y \in z :: p) by apply/fconnect_cycle/mem_head. case Dp: p cycNr => [|nz p1]; first by rewrite /= n'id. rewrite (cycle_path z) /= => /and3P[/eqP/(canRL nodeK)-Lp1 /eqP-Dnz nzNp1]. set fz := face z in Dfz; set ez := edge z in Lp1; pose nez := node ez. -pose ez' : WalkupN z := sub ez (negbT (e'id _)). +pose ez' : WalkupN z := Sub ez (negbT (e'id _)). have eez': edge ez' = ez' by apply: val_inj; rewrite /= ee eqxx. pose H := WalkupE ez'; pose h (u : H) : G := sval (sval u). have{n leGn} /IHn-IH_H: #|H| < n by rewrite ltnW // -!card_S_Walkup. have invh x: x != z -> x != ez -> {u | h u = x}. - by move=> z'x ez'x; apply: exist (sub (sub x _ : WalkupN z) _) _. + by move=> z'x ez'x; apply: exist (Sub (Sub x _ : WalkupN z) _) _. have h_eqE u v: (h u == h v) = (u == v) by []. have Ih: injective h by move=> u v /val_inj/val_inj. have z'h u: (h u == z) = false by apply/negbTE/(valP (val u)). diff --git a/theories/matte.v b/theories/matte.v index 93f4275..8385021 100644 --- a/theories/matte.v +++ b/theories/matte.v @@ -297,7 +297,7 @@ Lemma end0g_equad d : ~~ has (equad (gface d)) m -> m (end0g d) = false. Proof. move/hasPn/(_ _)/contraTF; apply; rewrite !(inE, in_gchop_rect) /gchop. rewrite !halfg_face !oddg_face /end0g; case: (halfg d) => x y. -by case: oddgP; rewrite /= !lter_add2 /= ?ler_addl ?ger_addl. +by case: oddgP; rewrite /= !lterD2 /= ?lerDl ?gerDl. Qed. Lemma mring_equad d : @@ -307,7 +307,7 @@ move=> m'fd; apply/mapP => -[d1 m_d1 Dp]. rewrite in_mring inE (contraTF (hasPn m'fd _)) {m'fd}// in m_d1. rewrite !(inE, in_gchop_rect) /gchop !halfg_face !oddg_face /end0g. rewrite -{Dp}(canLR (addrK _) Dp) -addrA; case: (halfg d) => x y. -by do 2!case: oddgP; rewrite /= !lter_add2 ?ger_addl ?ler_addl. +by do 2!case: oddgP; rewrite /= !lterD2 ?gerDl ?lerDl. Qed. Section Extend1. @@ -367,7 +367,7 @@ apply/allP=> _ /trajectP[i lti3 ->]; set p := halfg _. have [_] := andP ext1d; apply/contra=> m_p; apply/hasP; exists p => {m_p}//. rewrite in_gchop_rect /= /gchop {}/p -iterSr halfg_edge halfg_iter_face. case: (halfg d) => x y; rewrite oddg_iter_face. -by case: oddgP i lti3 => -[|[|[]]] //=; rewrite ?lter_add2 ?ler_addl ?ger_addl. +by case: oddgP i lti3 => -[|[|[]]] //=; rewrite ?lterD2 ?lerDl ?gerDl. Qed. Lemma ext1_mring_def : ext1_mring =i gborder (ext_mdisk d). @@ -465,7 +465,7 @@ apply/allP=> _ /trajectP[i lti2 ->]; rewrite -!iterSr. have [_ _ /hasPn/(_ _)/contraL] := and3P ext2d; apply. rewrite halfg_edge halfg_iter_face oddg_iter_face !(inE, in_gchop_rect). rewrite /gchop halfg_face oddg_face; case: (halfg d) => x y. -by case: oddgP i lti2 => -[|[]] //= _; rewrite !lter_add2 ?ler_addl ?ger_addl. +by case: oddgP i lti2 => -[|[]] //= _; rewrite !lterD2 ?lerDl ?gerDl. Qed. Lemma ext2_mring_def : ext2_mring =i gborder (ext_mdisk d). @@ -580,7 +580,7 @@ have{IHn} IHp d: halfg d = p -> has (predD r0 (gchop1 d)) m -> extends_in r p. case/andP: m0q => r0q /(hasPn r01'm); apply: contra => d_q. by rewrite in_gchop1_rect /= r0q gchop_chop1. set ed := gedge d; case Ded: (halfg ed) => [x y]. - case Dr0: r0 => [x0 x1 y0 y1] /=; rewrite -!ler_subr_addr !ltr_subr_addr. + case Dr0: r0 => [x0 x1 y0 y1] /=; rewrite -!lerBrDr !ltrBrDr. have r0efd i: r0 (halfg (gedge (iter i gface (gedge ed)))). by rewrite (insetP r0p) // -Dp -(halfg_iter_face i) gedge2 gtouch_edge. have /= (d2 := gedge (gface (gface ed))): gchop_rect r0 d2 (halfg d2). @@ -607,8 +607,8 @@ have m_nd4 q: r0 q -> has (equad (nd q)) m -> q \in m. apply/esym/eqP; rewrite -[_ == _]/(_ && _) !eq_le -andbA; apply/and4P. move: q4q1; rewrite !(inE, in_gchop_rect) /gchop halfg_face -[halfg _]halfgK. rewrite h_nd oddg_face o_nd ccw4; case: (halfg q) q1 => x y [x1 y1] /=. - rewrite -!(ltz_addr1 (_ %/ _)%Z) !ltz_divLR ?lez_divRL // !mulrDl !mulz2. - by case: oddgP; rewrite /= ?addr0 ?addrK !(addrA _ 1 1) !ltz_addr1; + rewrite -!(ltzD1 (_ %/ _)%Z) !ltz_divLR ?lez_divRL // !mulrDl !mulz2. + by case: oddgP; rewrite /= ?addr0 ?addrK !(addrA _ 1 1) !ltzD1; do ![case/andP | move-> | clear 1]. have gchop1F3E d: gchop1 (iter 3 gface (gedge d)) = gchop1 (gface d). by rewrite -gchop1_shift gface4 gedge2. @@ -657,7 +657,7 @@ have [m_nd | m'nd] := boolP (gnode p \in m). have nd4'm: ~~ has (equad (nd (gnode p))) m by apply: contra m'nd => /m_nd4->. have r0_n2p: r0 (gnode (gnode p)). rewrite -[gnode _]addrA oddg_node (insetP r0p) //. - by case: oddgP; case: (p) => x y; rewrite /= !lter_add2. + by case: oddgP; case: (p) => x y; rewrite /= !lterD2. have m_n2p: gnode (gnode p) \in m. have [q m_q p9q] := hasP m_p; apply/m_nd4/hasP=> //; exists q => //. have ep_q: gchop (gedge (nd p)) q. @@ -740,7 +740,7 @@ have ext_along d: {xm : matte | ext_m_r xm & forall c, xmE xm (oddg d) c}. by apply/hasP; exists q; rewrite ?in_refine_matte ?in_refine_rect 1?insetW. have xr_qd: inset xr (q - oddg d). rewrite -in_refine_rect refine_inset in r_p; apply/(insetP r_p). - by case: oddgP (q) => -[x y] /=; rewrite !lter_add2. + by case: oddgP (q) => -[x y] /=; rewrite !lterD2. have[xm1 xm1P xrm_xm1 xm1c1] := coarse_extends_in xrExmh xr_xm xr_qd. exists xm1 => [|c]. split=> p1 xm1p1; first by rewrite (in_extension xm1P) ?in_refine_matte. diff --git a/theories/patch.v b/theories/patch.v index 56ff47d..709f04e 100644 --- a/theories/patch.v +++ b/theories/patch.v @@ -1,5 +1,6 @@ (* (c) Copyright 2006-2018 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) +From HB Require Import structures. From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. From mathcomp Require Import fintype path fingraph. From fourcolor Require Import hypermap geometry jordan color coloring. @@ -546,9 +547,7 @@ Section PatchGcomp. Variables (G : hypermap) (z : G). Definition gcompd_dart := {x | gcomp z x}. -Canonical gcompd_eqType := [eqType of gcompd_dart]. -Canonical gcompd_choiceType := [choiceType of gcompd_dart]. -Canonical gcompd_finType := [finType of gcompd_dart]. +HB.instance Definition _ := Finite.on gcompd_dart. Implicit Type u : gcompd_dart. Fact gcompd_edge_subproof u : gcomp z (edge (val u)). @@ -560,9 +559,9 @@ Proof. exact: connect_trans (valP u) (connect1 (glinkN _)). Qed. Fact gcompd_face_subproof u : gcomp z (face (val u)). Proof. exact: connect_trans (valP u) (connect1 (glinkF _)). Qed. -Definition gcompd_edge u : gcompd_dart := sub _ (gcompd_edge_subproof u). -Definition gcompd_node u : gcompd_dart := sub _ (gcompd_node_subproof u). -Definition gcompd_face u : gcompd_dart := sub _ (gcompd_face_subproof u). +Definition gcompd_edge u : gcompd_dart := Sub _ (gcompd_edge_subproof u). +Definition gcompd_node u : gcompd_dart := Sub _ (gcompd_node_subproof u). +Definition gcompd_face u : gcompd_dart := Sub _ (gcompd_face_subproof u). Fact gcompd_subproof : cancel3 gcompd_edge gcompd_node gcompd_face. Proof. by move=> u; apply/val_inj/edgeK. Qed. @@ -573,13 +572,11 @@ Definition gcompd (u : gcomp_disk) := val u. Lemma inj_gcompd : injective gcompd. Proof. exact: val_inj. Qed. Lemma codom_gcompd : codom gcompd =i gcomp z. Proof. -by move=> x; apply/imageP/idP => [[[y zGy] _ -> //] | zGx]; exists (sub x zGx). +by move=> x; apply/imageP/idP => [[[y zGy] _ -> //] | zGx]; exists (Sub x zGx). Qed. Definition gcompr_dart := {x | ~~ gcomp z x}. -Canonical gcompr_eqType := [eqType of gcompr_dart]. -Canonical gcompr_choiceType := [choiceType of gcompr_dart]. -Canonical gcompr_finType := [finType of gcompr_dart]. +HB.instance Definition _ := Finite.on gcompr_dart. Implicit Type v : gcompr_dart. Local Notation glink1r gstep := (same_connect_r glinkC (connect1 gstep)). @@ -594,9 +591,9 @@ Proof. by rewrite /= -(glink1r (glinkN _)) (valP v). Qed. Fact gcompr_face_subproof v : predC (gcomp z) (face (val v)). Proof. by rewrite /= -(glink1r (glinkF _)) (valP v). Qed. -Definition gcompr_edge v : gcompr_dart := sub _ (gcompr_edge_subproof v). -Definition gcompr_node v : gcompr_dart := sub _ (gcompr_node_subproof v). -Definition gcompr_face v : gcompr_dart := sub _ (gcompr_face_subproof v). +Definition gcompr_edge v : gcompr_dart := Sub _ (gcompr_edge_subproof v). +Definition gcompr_node v : gcompr_dart := Sub _ (gcompr_node_subproof v). +Definition gcompr_face v : gcompr_dart := Sub _ (gcompr_face_subproof v). Fact gcompr_subproof : cancel3 gcompr_edge gcompr_node gcompr_face. Proof. by move=> v; apply/val_inj/edgeK. Qed. @@ -607,7 +604,7 @@ Lemma inj_gcompr : injective gcompr. Proof. exact: val_inj. Qed. Lemma codom_gcompr : codom gcompr =i predC (gcomp z). Proof. move=> x; apply/imageP/idP => [[[y z'Gy] _ ->] // | z'Gx]. -by exists ((sub _ : _ -> gcomp_rem) z'Gx). +by exists ((Sub _ : _ -> gcomp_rem) z'Gx). Qed. Lemma patch_gcomp : patch gcompd gcompr [::] [::]. diff --git a/theories/realprop.v b/theories/realprop.v index bfcbdaa..ed9a2dc 100644 --- a/theories/realprop.v +++ b/theories/realprop.v @@ -684,7 +684,7 @@ by case: (m2 - m1)%R => n; split; rewrite // -oppR0 leR_opp2 => /ltR0Sn. Qed. Lemma intR_ltP m1 m2 : reflect (m1 < m2) (m1 + 1 <= m2)%R. -Proof. by rewrite lez_addr1 ltNge; apply: (iffP idP) => /intR_leP. Qed. +Proof. by rewrite lezD1 ltNge; apply: (iffP idP) => /intR_leP. Qed. (* Embedding the rationals. *) @@ -702,7 +702,7 @@ Qed. Lemma ratR_leP a1 a2 : reflect (a1 <= a2) (a1 <= a2)%R. Proof. have [[r1 {3}-> Dr1] [r2 {3}-> Dr2]] := (ratR_eq a1, ratR_eq a2). -rewrite ler_pdivl_mulr ?ltr0Sn // mulrAC ler_pdivr_mulr ?ltr0Sn //. +rewrite ler_pdivlMr ?ltr0Sn // mulrAC ler_pdivrMr ?ltr0Sn //. rewrite -!intrM ler_int /=; apply: (equivP (intR_leP _ _)). by rewrite !intRM -Dr1 -Dr2 mulRAC !leR_pmul2r. Qed. @@ -822,7 +822,7 @@ Proof. move=> [m1x x_m1] [m2x x_m2]. wlog suffices: m1 m2 m1x {x_m1 m2x} x_m2 / (m1 <= m2)%R. by move=> IH; apply/eqP; rewrite eq_le !IH. -rewrite -(ler_add2r 1); apply/intR_ltP. +rewrite -(lerD2r 1); apply/intR_ltP. by rewrite intRD1; apply: leR_lt_trans x_m2. Qed. diff --git a/theories/sew.v b/theories/sew.v index ff38371..a6fa53c 100644 --- a/theories/sew.v +++ b/theories/sew.v @@ -123,7 +123,7 @@ Definition sew_tag_decode b := if b then SewDisk else SewRest. Fact sew_tag_subproof : cancel sew_tag_code sew_tag_decode. Proof. by case. Qed. HB.instance Definition _ := Countable.copy sew_tag (can_type sew_tag_subproof). #[non_forgetful_inheritance] -HB.instance Definition _ : isFinite sew_tag := CanFinMixin sew_tag_subproof. +HB.instance Definition _ : isFinite sew_tag := CanIsFinite sew_tag_subproof. Definition sew_dart_at i : finType := match i with @@ -132,12 +132,12 @@ Definition sew_dart_at i : finType := end. Definition sew_dart := {i : sew_tag & sew_dart_at i}. -HB.instance Definition _ := Finite.copy sew_dart [finType of sew_dart]. +HB.instance Definition _ := Finite.on sew_dart. Definition sewd xd : sew_dart := @Tagged _ SewDisk sew_dart_at xd. Definition sewr_r xr b'xr : sew_dart := - @Tagged _ SewRest sew_dart_at (sub xr b'xr). + @Tagged _ SewRest sew_dart_at (Sub xr b'xr). Definition sewr xr := match in_bGr xr with diff --git a/theories/snip.v b/theories/snip.v index ce788a8..8362e02 100644 --- a/theories/snip.v +++ b/theories/snip.v @@ -276,9 +276,9 @@ Qed. Fact dnode_subproof (u : ddart) : node (val u) \in diskN. Proof. by rewrite -(fclosed1 diskN_node) (valP u). Qed. -Let dedge u := (sub _ : _ -> ddart) (dedge_subproof u). -Let dnode u := (sub _ : _ -> ddart) (dnode_subproof u). -Let dface u := (sub _ : _ -> ddart) (dface_subproof u). +Let dedge u := (Sub _ : _ -> ddart) (dedge_subproof u). +Let dnode u := (Sub _ : _ -> ddart) (dnode_subproof u). +Let dface u := (Sub _ : _ -> ddart) (dface_subproof u). Fact snipd_subproof : cancel3 dedge dnode dface. Proof. @@ -298,7 +298,7 @@ Lemma inj_snipd : injective snipd. Proof. exact: val_inj. Qed. Lemma codom_snipd : codom snipd =i diskN. Proof. move=> z; apply/imageP/idP => [[[y dNy] /= _ -> //] | dNz]. -by exists (sub z dNz). +by exists (Sub z dNz). Qed. Definition snipd_ring := preim_seq snipd r. @@ -333,7 +333,7 @@ have homFd' u v : have dNy: y \in diskN. rewrite (fclosed1 diskN_node) diskN_E (fclosed1 diskE_edge) orbC. by rewrite -Dy faceK inE /= r'u (valP u). - apply: connect_trans {IHp yFp Lp}(IHp (sub y _) _ yFp Lp). + apply: connect_trans {IHp yFp Lp}(IHp (Sub y _) _ yFp Lp). by rewrite connect1 //= -val_eqE /= /snipd_face (negPf r'u) Dy. apply/hasP => [[w b_w yFw]]; case/hasP: b'u; exists w => //. apply: connect_trans yFw. @@ -390,9 +390,9 @@ apply: contra (valP u) => /andP[_ /= dNfu]; rewrite -[val u]faceK. by rewrite -(fclosed1 diskE_edge) !inE r'nfu -(fclosed1 diskN_node). Qed. -Let redge u := (sub _ : _ -> rdart) (redge_subproof u). -Let rnode u := (sub _ : _ -> rdart) (rnode_subproof u). -Let rface u := (sub _ : _ -> rdart) (rface_subproof u). +Let redge u := (Sub _ : _ -> rdart) (redge_subproof u). +Let rnode u := (Sub _ : _ -> rdart) (rnode_subproof u). +Let rface u := (Sub _ : _ -> rdart) (rface_subproof u). Fact snipr_subproof : cancel3 redge rnode rface. Proof. @@ -409,7 +409,7 @@ Lemma inj_snipr : injective snipr. Proof. apply: val_inj. Qed. Lemma codom_snipr : codom snipr =i [predC diskE]. Proof. move=> z; apply/imageP/idP => [[[y dE'y] _ /= -> //] | dE'z]. -by exists (sub z dE'z). +by exists (Sub z dE'z). Qed. Definition snipr_ring : seq snip_rem := preim_seq snipr (rev r). diff --git a/theories/walkup.v b/theories/walkup.v index d4f13f3..381f636 100644 --- a/theories/walkup.v +++ b/theories/walkup.v @@ -51,7 +51,7 @@ Implicit Types x y : G. Let tG' : predArgType := {x | x != z}. -Let inG' x neq_xz : tG' := sub x neq_xz. +Let inG' x neq_xz : tG' := Sub x neq_xz. Let z'G' (u : tG') : (val u == z) = false. Proof. exact: negPf (valP u). Qed. From 57b46dca7d3503e4615b6164a2f5e1245414d55f Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Thu, 28 Mar 2024 16:14:31 +0100 Subject: [PATCH 2/2] Update CI --- .github/workflows/docker-action.yml | 5 +++++ README.md | 4 ++-- coq-fourcolor.opam | 4 ++-- meta.yml | 14 ++++++++++++-- 4 files changed, 21 insertions(+), 6 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 2bb498a..d2a09b6 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -23,6 +23,11 @@ jobs: - 'mathcomp/mathcomp:2.0.0-coq-8.18' - 'mathcomp/mathcomp:2.1.0-coq-8.16' - 'mathcomp/mathcomp:2.1.0-coq-8.18' + - 'mathcomp/mathcomp:2.2.0-coq-8.16' + - 'mathcomp/mathcomp:2.2.0-coq-8.19' + - 'mathcomp/mathcomp:2.2.0-coq-dev' + - 'mathcomp/mathcomp-dev:coq-8.17' + - 'mathcomp/mathcomp-dev:coq-8.19' - 'mathcomp/mathcomp-dev:coq-dev' fail-fast: false steps: diff --git a/README.md b/README.md index 998b537..96a426f 100644 --- a/README.md +++ b/README.md @@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener [![Code of Conduct][conduct-shield]][conduct-link] [![Zulip][zulip-shield]][zulip-link] -[docker-action-shield]: https://github.com/coq-community/fourcolor/workflows/Docker%20CI/badge.svg?branch=master -[docker-action-link]: https://github.com/coq-community/fourcolor/actions?query=workflow:"Docker%20CI" +[docker-action-shield]: https://github.com/coq-community/fourcolor/actions/workflows/docker-action.yml/badge.svg?branch=master +[docker-action-link]: https://github.com/coq-community/fourcolor/actions/workflows/docker-action.yml [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md diff --git a/coq-fourcolor.opam b/coq-fourcolor.opam index 350b024..a65cefe 100644 --- a/coq-fourcolor.opam +++ b/coq-fourcolor.opam @@ -20,8 +20,8 @@ basic plane topology definitions, and a theory of combinatorial hypermaps.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "coq" {(>= "8.16" & < "8.19~") | (= "dev")} - "coq-mathcomp-ssreflect" {(>= "2.0.0" & < "2.2~") | (= "dev")} + "coq" {(>= "8.16" & < "8.20~") | (= "dev")} + "coq-mathcomp-ssreflect" {(>= "2.0.0" & < "2.3~") | (= "dev")} "coq-mathcomp-algebra" ] diff --git a/meta.yml b/meta.yml index e6a4484..0341cfb 100644 --- a/meta.yml +++ b/meta.yml @@ -35,7 +35,7 @@ license: supported_coq_versions: text: 8.16 or later - opam: '{(>= "8.16" & < "8.19~") | (= "dev")}' + opam: '{(>= "8.16" & < "8.20~") | (= "dev")}' tested_coq_opam_versions: - version: '2.0.0-coq-8.16' @@ -46,6 +46,16 @@ tested_coq_opam_versions: repo: 'mathcomp/mathcomp' - version: '2.1.0-coq-8.18' repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-8.16' + repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-8.19' + repo: 'mathcomp/mathcomp' +- version: '2.2.0-coq-dev' + repo: 'mathcomp/mathcomp' +- version: 'coq-8.17' + repo: 'mathcomp/mathcomp-dev' +- version: 'coq-8.19' + repo: 'mathcomp/mathcomp-dev' - version: 'coq-dev' repo: 'mathcomp/mathcomp-dev' @@ -56,7 +66,7 @@ ci_cron_schedule: '0 5 * * *' dependencies: - opam: name: coq-mathcomp-ssreflect - version: '{(>= "2.0.0" & < "2.2~") | (= "dev")}' + version: '{(>= "2.0.0" & < "2.3~") | (= "dev")}' description: |- [MathComp ssreflect 2.0 or later](https://math-comp.github.io) - opam: