diff --git a/_CoqProject b/_CoqProject index cfec3ed..915278b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -42,7 +42,6 @@ theories/z3irrational.v theories/z3seq_props.v theories/rho_computations.v theories/multinomial.v -theories/floor.v theories/hanson_elem_arith.v theories/hanson_elem_analysis.v theories/hanson.v diff --git a/theories/floor.v b/theories/floor.v deleted file mode 100644 index ae87d0b..0000000 --- a/theories/floor.v +++ /dev/null @@ -1,101 +0,0 @@ -From mathcomp Require Import all_ssreflect all_algebra. - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import Order.TTheory GRing.Theory Num.Theory. - -Local Open Scope ring_scope. - -(* reminder: Posz k = k, Negz k = (-(k+1)) *) -Definition floorQ (r : rat) := (numq r %/ denq r)%Z. - -Lemma floorQ_spec (r : rat) : (floorQ r)%:Q <= r < (floorQ r)%:Q + 1. -Proof. -rewrite -[r in _ <= r < _]divq_num_den ler_pdivlMr ?ltr_pdivrMr ?ltr0z //. -by rewrite -rat1 -intrD -!intrM ler_int ltr_int lez_floor ?ltz_ceil. -Qed. - -Lemma floorQ_epslt1 (r : rat) : 0 <= r - (floorQ r)%:Q < 1. -Proof. by rewrite subr_ge0 ltrBlDl floorQ_spec. Qed. - -Lemma floorQ_grows (r1 r2 : rat) : r1 <= r2 -> floorQ r1 <= floorQ r2. -Proof. -move => Hr12. -suff: (floorQ r1)%:Q < (floorQ r2 + 1)%:Q by rewrite ltr_int ltzD1. -rewrite intrD; case/andP: (floorQ_spec r2) => _; apply: le_lt_trans. -by apply: le_trans Hr12; case/andP: (floorQ_spec r1). -Qed. - -Lemma floorQ_unique (r : rat) (m : int) : m%:Q <= r < (m + 1)%:Q -> m = floorQ r. -Proof. -have /andP[Hfloor1 Hfloor2] := floorQ_spec r. -case/andP => Hm1 Hm2. -move: (le_lt_trans Hm1 Hfloor2) (le_lt_trans Hfloor1 Hm2). -rewrite -[n in _ + n]rat1 -intrD !ltr_int !ltzD1 => ? ?. -by apply/eqP; rewrite eq_le; apply/andP. -Qed. - -Lemma floorQ_int (m : int) : m = floorQ m%:Q. -Proof. by apply: floorQ_unique; rewrite ltr_int ltzD1 !lexx. Qed. - -Lemma floorQ_ge0 (r : rat) : 0 <= r -> 0 <= floorQ r. -Proof. by move=> Hrge0; rewrite [0]floorQ_int floorQ_grows. Qed. - -Lemma floorQ_ge1 (r : rat) : 1 <= r -> 1 <= floorQ r. -Proof. by move=> Hrge0; rewrite [1]floorQ_int floorQ_grows. Qed. - -Lemma floor_addEpsilon (m : int) (epsilon : rat) : - 0 <= epsilon < 1 -> floorQ (m%:Q + epsilon) = m. -Proof. -move=> /andP[Heps1 Heps2]. -by apply/esym/floorQ_unique; rewrite lerDl Heps1 intrD ltrD2l. -Qed. - -Lemma floorQ_div (q : rat) (m : nat) : - floorQ (q / m.+1%:Q) = floorQ ((floorQ q)%:Q / m.+1%:Q). -Proof. -apply/floorQ_unique; move: (floorQ_spec q) (floorQ_spec (q / m.+1%:Q)). -rewrite !ler_pdivlMr ?ltr_pdivrMr ?ltr0z // intrD -intrM ler_int. -move=> /andP[_ Hq] /andP[Hdiv /le_lt_trans ->] //. -by rewrite -ltzD1 -(ltr_int rat) intrD (le_lt_trans Hdiv). -Qed. - -(* Lemma floorQ_div_pos (q : rat) (m : nat) : *) -(* (m > 0)%N -> *) -(* floorQ (q / m%:Q) = floorQ ((floorQ q)%:Q / m%:Q). *) -(* Proof. *) - -(* Lemma foo (n m : int) : m%:Q / n%:Q = m%:Q + n%:Q. *) -(* case: (divqP m n). *) - -Lemma floorQ_divn (m : nat) (n : nat) : - floorQ (m%:Q / n.+1%:Q) = floorQ (m %/ n.+1)%N%:Q. -Proof. -apply/esym/floorQ_unique. -rewrite -floorQ_int ler_pdivlMr ?ltr_pdivrMr ?ltr0z //. -rewrite -!natrM ler_nat ltr_nat mulnDl mul1n. -by rewrite [m in (_ <= m < _)%N](divn_eq m n.+1) leq_addr ltn_add2l ltn_mod. -Qed. - -(* Lemma floorQ_divn_pos (m n : nat) : (n > 0)%N -> floorQ (m%:Q / n%:Q) = floorQ (m %/ n)%N%:Q. *) -(* Proof. *) -(* by case: n => [|n] // H ; apply: floorQ_divn. *) -(* Qed. *) - -Lemma helper1 n1 n2 n3 : - (n2 > 0)%N -> (n3 > 0)%N -> - ((n1 %/ n2) %/ n3)%N = floorQ (n1%:Q / (n2 * n3)%N%:Q) :> int. -Proof. -case: n2 =>[|n2] //; case: n3 => [|n3] // => Hpos2 Hpos3. -by rewrite -divnMA mulSn addSn floorQ_divn -floorQ_int. -Qed. - -(* Lemma helper2 n1 n2 n3 : *) -(* (n2 > 0)%N -> (n3 > 0)%N -> *) -(* floorQ ((n1 %/ n2) %/ n3)%N%:Q = floorQ ((n1 %/ n3) %/ (n2)%N)%:Q :> int. *) -(* Proof. *) -(* move => Hn2 Hn3. *) -(* by rewrite helper1 // mulnC -helper1 //. *) -(* Qed. *) diff --git a/theories/hanson.v b/theories/hanson.v index 73b1d83..ade66c6 100644 --- a/theories/hanson.v +++ b/theories/hanson.v @@ -1,6 +1,6 @@ Require Import ZArith. -From mathcomp Require Import all_ssreflect all_algebra all_field. -Require Import extra_mathcomp tactics binomialz floor arithmetics posnum. +From mathcomp Require Import all_ssreflect all_algebra all_field archimedean. +Require Import extra_mathcomp tactics binomialz arithmetics posnum. Require Import rat_of_Z hanson_elem_arith hanson_elem_analysis. Set Implicit Arguments. @@ -522,13 +522,10 @@ suff [K [Kpos KP]] : exists K : nat, exists K; split => // -[| n]; first by rewrite expn0 muln1 iter_lcmn0. case: n => [| n]; first by rewrite iter_lcmn1 muln_gt0 Kpos. by apply/leq_trans/KP/n_between_a => //; apply/lcm_leq_Cnk. -suff [K [Kpos KP]] : exists K : rat, +suff [K [/ltW/trunc_itv/andP[_ Kpos] KP]] : exists K : rat, (0 < K) /\ forall n k, cond n k -> (C n k.+1)%:R <= K * 3%:R ^ n. - move: (floorQ K) (floorQ_ge0 (ltW Kpos)) (floorQ_spec K). - case=> // k _ /andP [_ leKSn]; exists k.+1; split=> // n m {}/KP KP. - suff: (C n m.+1)%:R <= (k%:Q + 1) * 3%:R ^ n. - by rewrite -[_ + 1%:R]natrD -[_ ^ n]natrX -natrM ler_nat addn1. - exact/le_trans/ler_wpM2r/ltW/leKSn/exprz_ge0. + exists (Num.trunc K).+1; split=> // n m {}/KP. + by rewrite -(ler_nat rat) natrM natrX => /le_trans-> //; apply/ler_wpM2r/ltW. move mE: 10%N%:Q => m. (* FIXME *) have lt0m : 0 < m by rewrite -mE. have le0m : 0 <= m by exact: ltW. diff --git a/theories/hanson_elem_arith.v b/theories/hanson_elem_arith.v index 97b6fd6..4bb5073 100644 --- a/theories/hanson_elem_arith.v +++ b/theories/hanson_elem_arith.v @@ -1,5 +1,5 @@ From mathcomp Require Import all_ssreflect all_algebra. -Require Import extra_mathcomp tactics floor arithmetics multinomial. +Require Import extra_mathcomp tactics arithmetics multinomial. Set Implicit Arguments. Unset Strict Implicit.