Skip to content

Commit

Permalink
Merge pull request #14 from coq-community/fix-pzero
Browse files Browse the repository at this point in the history
fix problems with =Pzero after Coq lexing changes
  • Loading branch information
palmskog authored Aug 9, 2022
2 parents edb4131 + 09628e6 commit fe0c2f3
Show file tree
Hide file tree
Showing 8 changed files with 12 additions and 12 deletions.
2 changes: 1 addition & 1 deletion theories/numbers/ssetq1.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 2 additions & 2 deletions theories/ordinals/sset12.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.


Expand Down Expand Up @@ -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 <oj -> g \0o i <o g \0o j.
have pa: forall i j, i <o j -> g \0o i <o g \0o j.
move => 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).
Expand Down
2 changes: 1 addition & 1 deletion theories/ordinals/sset13b.v
Original file line number Diff line number Diff line change
Expand Up @@ -1256,7 +1256,7 @@ Qed.

Definition oprod2_comm_P4 x y :=
exists z gamma c1 c2,
[/\ cnfp_nz z, \0o <ooexp z \0c, ordinalp gamma &
[/\ cnfp_nz z, \0o <o oexp z \0c, ordinalp gamma &
[/\ natp c1, natp c2,
x = cnf_val z,
cnf_degree z = gamma *o c1 &
Expand Down
4 changes: 2 additions & 2 deletions theories/ordinals/sset13c.v
Original file line number Diff line number Diff line change
Expand Up @@ -83,7 +83,7 @@ Lemma Vr_oor x e: ~inc e (cnf_exponents x) -> 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)).
Expand All @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion theories/ordinals/sset16b.v
Original file line number Diff line number Diff line change
Expand Up @@ -275,7 +275,7 @@ Qed.
Lemma nds_k_of_prop f:
f \0c = \1c -> f \1c = \1c ->
(forall n, natp n -> \1c <c n ->
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.
Expand Down
2 changes: 1 addition & 1 deletion theories/schutte/ssete9.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion theories/sets/sset7.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
6 changes: 3 additions & 3 deletions theories/sets/sset9.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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))).
Expand Down Expand Up @@ -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 <c (csucc p) -> (fun i=> i +c (p -ci)) i = p).
have fim: (forall i, i <c (csucc p) -> (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)).
Expand Down

0 comments on commit fe0c2f3

Please sign in to comment.