Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

A shorter proof of w_upper_bounded #19

Merged
merged 1 commit into from
Oct 27, 2023
Merged

A shorter proof of w_upper_bounded #19

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
33 changes: 11 additions & 22 deletions theories/hanson.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -317,22 +317,18 @@ have -> : w_seq 4 = a' 0 * a' 1 * a' 2 * a' 3.
by rewrite /w_seq !big_ord_recr /= big_ord0 mul1r.
have a'0_ubP : a' 0 <= a'0_ub%:C.
have ge0a'0 : 0 <= a'0_ub%:C by rewrite ler0q divr_ge0.
rewrite root_le_x // a0 -rmorphXn ler_rat exprMn exprVn.
by rewrite lter_pdivlMr; ring_lia.
by rewrite root_le_x // a0 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia.
have a'1_ubP : a' 1 <= a'1_ub%:C.
have ge0a'1 : 0 <= a'1_ub%:C by rewrite ler0q divr_ge0.
rewrite root_le_x // a1 -rmorphXn ler_rat exprMn exprVn.
by rewrite lter_pdivlMr; ring_lia.
by rewrite root_le_x // a1 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia.
have a'2_ubP : a' 2 <= a'2_ub%:C.
have ge0a'2 : 0 <= a'2_ub%:C by rewrite ler0q divr_ge0.
have ge0a2 : 0 <= (a 2)%:Q%:C by rewrite ler0q.
rewrite root_le_x // a2 -rmorphXn ler_rat exprMn exprVn.
by rewrite lter_pdivlMr; ring_lia.
by rewrite root_le_x // a2 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia.
have a'3_ubP : a' 3 <= a'3_ub%:C.
have ge0a'3 : 0 <= a'3_ub%:C by rewrite ler0q divr_ge0.
have ge0a3 : 0 <= (a 3)%:Q%:C by rewrite ler0q.
rewrite root_le_x // a3 -rmorphXn ler_rat exprMn exprVn.
by rewrite lter_pdivlMr; ring_lia.
by rewrite root_le_x // a3 -rmorphXn ler_rat expr_div_n ler_pdivlMr; ring_lia.
have a'4_ubP : a' 4 <= a'4_ub%:C.
have ge0a'1 : 0 <= a'4_ub%:C by rewrite ler0q divr_ge0.
have ge0a4 : 0 <= (a 4)%:Q%:C by rewrite ler0q ler0z.
Expand All @@ -349,33 +345,26 @@ have a'4_ubP : a' 4 <= a'4_ub%:C.
rewrite 8!big_ord_recl big_ord0 !expr1n !mul1r /= /bump !add1n.
set lhs := (X in _ <= X).
suff -> : lhs = rat_of_Z 34077892883014859211 / rat_of_Z 12800000000000000.
have ->: 1807%:~R = rat_of_Z 1807 by rewrite rat_of_ZEdef; congr _%:~R.
by rewrite lter_pdivlMr // -subr_ge0 -rmorphM -rmorphB rat_of_Z_ZposW.
by rewrite lter_pdivlMr; ring_lia.
rewrite {}/lhs bin0 mulr1n bin1 expr0 expr1.
have -> : t ^+ 7 *+ 'C(1807, 7) = t ^+ 7 * rat_of_Z 12337390971384003811.
rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=.
rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul.
by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field.
by field.
have -> : t ^+ 6 *+ 'C(1807, 6) = t ^+ 6 * rat_of_Z 47952102609488077.
rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=.
rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul.
by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field.
by field.
have -> : t ^+ 5 *+ 'C(1807, 5) = t ^+ 5 * rat_of_Z 159662938766331.
rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=.
rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul.
by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field.
by field.
have -> : t ^+ 4 *+ 'C(1807, 4) = t ^+ 4 * rat_of_Z 442770212885.
rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=.
rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul.
by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field.
by field.
have -> : t ^+ 3 *+ 'C(1807, 3) = t ^+ 3 * rat_of_Z 981752135.
rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=.
rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul.
by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field.
by field.
have -> : t ^+ 2 *+ 'C(1807, 2) = t ^+ 2 * rat_of_Z 1631721.
rewrite -mulr_natr pmulrn -binz_nat_nat binzE_ffact -ffactnn ffactE /=.
rewrite -!rat_of_Z_of_nat !Nat2Z.inj_mul.
by do !(set x := Z.of_nat _; compute in x; rewrite {}/x); field.
by field.
by rewrite /t; field.
by rewrite 4!rmorphM rmorphXn /=; do 4!rewrite ler_pM ?mulr_ge0 //.
Qed.
Expand Down
Loading