From 09628e65ad7edf94d1758503b330b8184b42ff9a Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Tue, 9 Aug 2022 18:36:57 +0200 Subject: [PATCH] fix problems with notations after Coq lexing changes --- theories/numbers/ssetq1.v | 2 +- theories/ordinals/sset12.v | 4 ++-- theories/ordinals/sset13b.v | 2 +- theories/ordinals/sset13c.v | 4 ++-- theories/ordinals/sset16b.v | 2 +- theories/schutte/ssete9.v | 2 +- theories/sets/sset7.v | 2 +- theories/sets/sset9.v | 6 +++--- 8 files changed, 12 insertions(+), 12 deletions(-) diff --git a/theories/numbers/ssetq1.v b/theories/numbers/ssetq1.v index 32e5cbd..00023b2 100644 --- a/theories/numbers/ssetq1.v +++ b/theories/numbers/ssetq1.v @@ -2190,7 +2190,7 @@ Qed. End BQdiffProps4. Lemma BQdiv_div_simp a b c: ratp a -> ratp b -> ratp c -> b <> \0q -> - (a /q b) /q (c /q b) = a /qc. + (a /q b) /q (c /q b) = a /q c. Proof. move => aq bq cq bnz. move: (QS_inv bq) (QS_inv cq) => biq ciq. diff --git a/theories/ordinals/sset12.v b/theories/ordinals/sset12.v index ca3158a..21d6e0e 100644 --- a/theories/ordinals/sset12.v +++ b/theories/ordinals/sset12.v @@ -635,7 +635,7 @@ move => oa ob; split. - by right. - move => h; case:(limit_nonsucc' (osum_limit oa ov) h). case; first by move => [-> osa]; rewrite (osum0r oa). -move => [c oc ->]; rewrite - (osum2_succ oa oc); exists (a+oc); fprops. +move => [c oc ->]; rewrite - (osum2_succ oa oc); exists (a +o c); fprops. Qed. @@ -4622,7 +4622,7 @@ Qed. Lemma all_der_p13 : f \0o <> \0o -> normal_ofs (g \0o). Proof. move => fz. -have pa: forall i j, i g \0o i g \0o i i j ij;move:(ij)=> [[oi oj _] _]. apply/(all_der_p10 OS0 OS0 oi oj); split => //. + move => _; apply: ord_ne0_pos; first by apply:(OS_all_der OS0 oj). diff --git a/theories/ordinals/sset13b.v b/theories/ordinals/sset13b.v index 4f3051c..7bb0c96 100644 --- a/theories/ordinals/sset13b.v +++ b/theories/ordinals/sset13b.v @@ -1256,7 +1256,7 @@ Qed. Definition oprod2_comm_P4 x y := exists z gamma c1 c2, - [/\ cnfp_nz z, \0o Vr x e = \0c. Proof. by move => h; rewrite /Vr (Vg_out_of_range h). Qed. Lemma cnf_nat_sum_p2 x y : cnfp x -> cnfp y -> forall e, - Vr (x +#fy) e = (Vr x e) +c Vr y e. + Vr (x +#f y) e = (Vr x e) +c Vr y e. Proof. move => ox oy e. move:(cnf_sort_correct (cnf_nat_sum_range ox oy)). @@ -107,7 +107,7 @@ Qed. Lemma cnf_nat_sum_p3 x y z : cnfp x -> cnfp y -> cnfp z -> - (forall e, Vr z e = (Vr x e) +c Vr y e) -> z = x +#fy. + (forall e, Vr z e = (Vr x e) +c Vr y e) -> z = x +#f y. Proof. move => ox oy oz hz. move:(cnfp_nat_sum ox oy) (cnf_nat_sum_p2 ox oy); set t := cnf_nat_sum x y. diff --git a/theories/ordinals/sset16b.v b/theories/ordinals/sset16b.v index 897e1d9..aeed119 100644 --- a/theories/ordinals/sset16b.v +++ b/theories/ordinals/sset16b.v @@ -275,7 +275,7 @@ Qed. Lemma nds_k_of_prop f: f \0c = \1c -> f \1c = \1c -> (forall n, natp n -> \1c - f n = ndsC (nds_k_of n) *c f (n -cnds_k_of n)) -> + f n = ndsC (nds_k_of n) *c f (n -c nds_k_of n)) -> forall n, natp n -> f n = nds_sol n. Proof. move => f0 f1 hb. diff --git a/theories/schutte/ssete9.v b/theories/schutte/ssete9.v index ed568b3..857aeab 100644 --- a/theories/schutte/ssete9.v +++ b/theories/schutte/ssete9.v @@ -2204,7 +2204,7 @@ Qed. Lemma nf_revCE u v: T1bad <> T1omega * u + \F v. Proof. -case: (altP (u=Pzero)); first by move => ->; case v. +case: (altP (u =P zero)); first by move => ->; case v. move/mul_omega_limit;set w:= (T1omega * u). case: v; first by rewrite T1addn0 => sa sb; move: sa; rewrite - sb. by move => v; case w => // a n b; case a. diff --git a/theories/sets/sset7.v b/theories/sets/sset7.v index 28b21fa..cb9ad16 100644 --- a/theories/sets/sset7.v +++ b/theories/sets/sset7.v @@ -712,7 +712,7 @@ Proof. split. move=> [or or' [otr otr' [f [t [sx iso]]]]];split => //. move: (isomorphism_worder_sub (ordinal_o_wor or') sx) =>[]. - set g := iso_seg_fun _ _ => sw isg; exists (g \cof ), (target g); split => //. + set g := iso_seg_fun _ _ => sw isg; exists (g \co f), (target g); split => //. exact: (compose_order_is iso isg). move=> [or or' [f [t [[sx sxp] oi]]]]; split => //; split; fprops. by exists f, t. diff --git a/theories/sets/sset9.v b/theories/sets/sset9.v index 54c3eb1..cc5eaf6 100644 --- a/theories/sets/sset9.v +++ b/theories/sets/sset9.v @@ -2685,7 +2685,7 @@ move=> [q1N r1N [aeq r1p]]. rewrite aeq csumA - cprodDr. set q2:= (a +c q). have q2N: natp q2 by apply: NS_sum. -have dp: (cdivision_prop ((B *c q2) +cr) B q2 r) by split. +have dp: (cdivision_prop ((B *c q2) +c r) B q2 r) by split. by move: (cquorem_pr (NS_sum (NS_prod BN q2N) r1N) BN q2N r1N dp) => [_]. Qed. @@ -4124,7 +4124,7 @@ Proof. move=> h. move:(cleR (CS_sum2 a b)). move:(NS_sum (proj31 h)(proj32 h)). -move: {1 3}(a+cb) => n nN; move: n nN a b h; apply:Nat_induction. +move: {1 3}(a +c b) => n nN; move: n nN a b h; apply:Nat_induction. move => a b [aN bN cab] /cle0 /csum_nz [az bz]. set H := cdivides_zero NS0. by rewrite az bz in cab;move: (card1_nz(esym (cab \0c H H))). @@ -7980,7 +7980,7 @@ suff eq: (sn +c sn = aux). by rewrite csum_nn -nsp [RHS] even_half. rewrite /aux cprodC /sn nsp. rewrite nsp in nN. -have fim: (forall i, i (fun i=> i +c (p -ci)) i = p). +have fim: (forall i, i (fun i=> i +c (p -c i)) i = p). by move=> i /(cltSleP pN) => ilp; apply: cdiff_pr. rewrite - (fct_sum_const1 nN fim). rewrite - (sum_of_sums (fun i => i) (fun i=> (p -c i)) (csucc p)).