From b4f975c9095b354e7f85cc30ec597fccce06f87e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 17 Oct 2018 11:33:07 +0200 Subject: [PATCH 01/13] WIP: eudoxus reals --- eudoxus.v | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 eudoxus.v diff --git a/eudoxus.v b/eudoxus.v new file mode 100644 index 0000000000..e69de29bb2 From 6eabce0de0f7357b266315e7e41d6aefd845c58b Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 17 Oct 2018 18:15:28 +0200 Subject: [PATCH 02/13] Def. of the eudoxus reals + zmod structure + mul def + basic properties on mul --- eudoxus.v | 317 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 317 insertions(+) diff --git a/eudoxus.v b/eudoxus.v index e69de29bb2..bd767334a7 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -0,0 +1,317 @@ +(* -------------------------------------------------------------------- *) +From mathcomp Require Import all_ssreflect all_algebra. +(* ------- *) Require Import boolp classical_sets. + +(* For gen_choiceType *) +(* ------- *) Require Import topology. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Import GRing.Theory Num.Def Num.Theory. + +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. +Local Open Scope quotient_scope. + +(* -------------------------------------------------------------------- *) +Reserved Notation "\- f" (at level 40, left associativity). + +Section LiftedZmod. +Variables (U : Type) (V : zmodType). +Definition opp_fun_head t (f : U -> V) x := let: tt := t in - f x. +End LiftedZmod. + +Local Notation "\- f" := (opp_fun_head tt f) : ring_scope. + +(* -------------------------------------------------------------------- *) +Lemma equiv_refl_eq {T : Type} (e : equiv_rel T) (x y : T) : + x = y -> e x y. +Proof. by move=> ->; apply: equiv_refl. Qed. + +(* -------------------------------------------------------------------- *) +Local Reserved Notation "n %:E" (at level 2, left associativity, format "n %:E"). +Local Reserved Notation "f ~ g" (at level 60, no associativity). +Local Reserved Notation "~%E" (at level 0). + +(* -------------------------------------------------------------------- *) +Delimit Scope eudoxus_scope with E. + +(* -------------------------------------------------------------------- *) +Definition is_qzendo (f : int -> int) := + exists k : int, forall m n : int, `|f (m + n) - (f m + f n)| < k. + +Definition qzEndo := + [qualify a f : int -> int | `[]]. + +Fact qzendo_key : pred_key qzEndo. Proof. by []. Qed. +Canonical qzendo_keyed := KeyedQualifier qzendo_key. + +Record qzendo := QZEndo { qzendof :> int -> int; _ : qzendof \is a qzEndo }. + +Canonical qzendo_subType := Eval hnf in [subType for qzendof]. + +Definition qzendo_eqMixin := Eval hnf in [eqMixin of qzendo by <:]. +Canonical qzendo_eqType := Eval hnf in EqType qzendo qzendo_eqMixin. +Definition qzendo_choiceMixin := [choiceMixin of qzendo by <:]. +Canonical qzendo_choiceType := Eval hnf in ChoiceType qzendo qzendo_choiceMixin. + +(* -------------------------------------------------------------------- *) +Lemma is_qzendoP (f : int -> int) : + reflect + (exists k : int, forall m n : int, `|f (m + n) - (f m + f n)| < k) + (f \is a qzEndo). +Proof. by apply/asboolP. Qed. + +(* -------------------------------------------------------------------- *) +Definition qzendoC (z : int) := fun x : int => x * z. + +Local Notation "z %:E" := (qzendoC z). + +Lemma qzendoC_is_additive z : additive (qzendoC z). +Proof. by move=> n m; rewrite /qzendoC; rewrite -mulrBl. Qed. + +Canonical qzendoC_additive z := Additive (qzendoC_is_additive z). + +(* -------------------------------------------------------------------- *) +Section QZEndoMorph. +Implicit Types f g : int -> int. + +Lemma additive_is_qzendo (f : {additive int -> int}): + GRing.Additive.apply f \is a qzEndo. +Proof. +apply/is_qzendoP; exists 1 => n m. +by rewrite [f (_ + _)]raddfD opprD addrACA !subrr normr0. +Qed. + +Lemma is_qzendoC c : c%:E \is a qzEndo. +Proof. by apply: additive_is_qzendo. Qed. + +Lemma is_qzendoD f g : + f \is a qzEndo -> g \is a qzEndo -> f \+ g \is a qzEndo. +Proof. +move=> /is_qzendoP[kf bdf] /is_qzendoP[kg bdg]. +apply/is_qzendoP; exists (kf + kg) => n m /=. +rewrite addrACA opprD addrACA. +by apply/(ler_lt_trans (ler_norm_add _ _))/ltr_add. +Qed. + +Lemma is_qzendoN f : f \is a qzEndo -> \- f \is a qzEndo. +Proof. +case/is_qzendoP=> kf bdf; apply/is_qzendoP; exists kf. +by move=> n m /=; rewrite -!opprD normrN. +Qed. + +Lemma is_qzendoM f g : + f \is a qzEndo -> g \is a qzEndo -> f \o g \is a qzEndo. +Proof. +case/is_qzendoP=> kf bdf; case/is_qzendoP=> kg bdg. +pose M : int := \sum_(0 <= i < `|kg|) (`|f i| + `|f (- i%:Z)|). +apply/is_qzendoP; exists (M + kf *+ 2) => m n /=. +rewrite -[X in `|X - _|](subrK (f (g m + g n))). +rewrite -[X in `|X|]addrA (ler_lt_trans (ler_norm_add _ _)) //. +rewrite mulr2n addrA ltr_add //. +rewrite -[X in `|X|](subrK (f (g (m + n) - (g m + g n)))). +rewrite [X in _ < X]addrC (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. ++ by rewrite addrAC -{1}[g (m + n)](subrK (g m + g n)) -addrA -opprD. +rewrite {}/M; set k := g _ - _; rewrite (bigD1_seq `|k|%N) /=; first last. ++ by apply/iota_uniq. ++ rewrite mem_index_iota /k /= -ltz_nat !abszE. + by apply/(ltr_le_trans (bdg _ _))/ler_norm. +rewrite !abszE ler_paddr ?sumr_ge0 //; case: (ger0P k) => _. ++ by apply/ler_addl. ++ by rewrite opprK; apply/ler_addr. +Qed. + +End QZEndoMorph. + +(* -------------------------------------------------------------------- *) +Section QZEqv. + +Definition qzeqv (f g : qzendo) := + `[]. + +Local Notation "~%E" := qzeqv. +Local Notation "f ~ g" := (qzeqv f g). + +Lemma qzeqvP (f g : qzendo) : + reflect + (exists k : int, forall n : int, `|f n - g n| < k) + (f ~ g). +Proof. by apply: asboolP. Qed. + +Lemma qzeqv_is_equiv : equiv_class_of ~%E. +Proof. split. ++ by move=> f; apply/qzeqvP; exists 1 => n; rewrite subrr normr0. ++ suff sym f g: f ~ g -> g ~ f by move=> f g; apply/idP/idP => /sym. + by case/qzeqvP=> [k hk]; apply/qzeqvP; exists k=> n; rewrite distrC. ++ move=> f g h /qzeqvP[k1 h1] /qzeqvP[k2 h2]. + apply/qzeqvP; exists (k1 + k2) => n. + apply/(ler_lt_trans _ (ltr_add (h1 n) (h2 n))). + apply/(ler_trans _ (ler_norm_add _ _)). + by rewrite [f n - _]addrC addrACA addNr addr0. +Qed. + +Lemma qzeqv_refl_eq (f g : qzendo) : f =1 g -> f ~ g. +Proof. +move=> eq_fg; apply/qzeqvP; exists 1 => n. +by rewrite eq_fg subrr normr0. +Qed. + +Canonical qzeqv_equiv := EquivRelPack qzeqv_is_equiv. +Canonical qzeqv_encModRel := defaultEncModRel ~%E. + +Definition eudoxus := {eq_quot ~%E}. + +Canonical eudoxus_quotType := [quotType of eudoxus]. +Canonical eudoxus_eqType := [eqType of eudoxus]. +Canonical eudoxus_choiceType := [choiceType of eudoxus]. +Canonical eudoxus_eqQuotType := [eqQuotType ~%E of eudoxus]. + +End QZEqv. + +Local Notation "~%E" := qzeqv. +Local Notation "f ~ g" := (qzeqv f g). + +(* -------------------------------------------------------------------- *) +Definition edxoppf (f : qzendo) : qzendo := + QZEndo (is_qzendoN (valP f)). + +Definition edxaddf (f g : qzendo) : qzendo := + QZEndo (is_qzendoD (valP f) (valP g)). + +Definition edxmulf (f g : qzendo) : qzendo := + QZEndo (is_qzendoM (valP f) (valP g)). + +Definition edxopp := lift_op1 eudoxus edxoppf. +Definition edxadd := lift_op2 eudoxus edxaddf. +Definition edxmul := lift_op2 eudoxus edxmulf. + +(* -------------------------------------------------------------------- *) +Definition to_eudoxus := + lift_embed eudoxus (fun z : int => QZEndo (is_qzendoC z)). + +Canonical to_eudoxus_pi_morph := PiEmbed to_eudoxus. + +(* -------------------------------------------------------------------- *) +Lemma pi_edxopp : {morph \pi_eudoxus : f / edxoppf f >-> edxopp f}. +Proof. +move=> f; unlock edxopp; apply/eqmodP/qzeqvP; rewrite /edxoppf /=. +set g := repr _; have: f ~ g by apply/eqmodP; rewrite reprK. +by case/qzeqvP=> k hk; exists k => n; rewrite -opprD normrN. +Qed. + +Canonical pi_edxopp_morph := PiMorph1 pi_edxopp. + +(* -------------------------------------------------------------------- *) +Lemma pi_edxadd : {morph \pi_eudoxus : f g / edxaddf f g >-> edxadd f g}. +Proof. +move=> f g; unlock edxadd; apply/eqmodP/qzeqvP; rewrite /edxaddf /=. +set f' := repr (_ f); set g' := repr (_ g). +have: g ~ g' by apply/eqmodP; rewrite reprK. +have: f ~ f' by apply/eqmodP; rewrite reprK. +move=> /qzeqvP[k1 h1] /qzeqvP[k2 h2]; exists (k1 + k2) => n. +rewrite opprD addrACA (ler_lt_trans _ (ltr_add (h1 n) (h2 n))) //. +by apply/ler_norm_add. +Qed. + +Canonical pi_edxadd_morph := PiMorph2 pi_edxadd. + +(* -------------------------------------------------------------------- *) +Lemma pi_edxmul : {morph \pi_eudoxus : f g / edxmulf f g >-> edxmul f g}. +Proof. +move=> f g; unlock edxmul; apply/eqmodP => /=. +set f' := repr (_ f); set g' := repr (_ g). +apply/(@equiv_trans _ _ (edxmulf f' g)); apply/qzeqvP=> /=. ++ have: f ~ f' by apply/eqmodP; rewrite reprK. + by case/qzeqvP=> [k hk]; exists k. +have /qzeqvP[k hk]: g ~ g' by apply/eqmodP; rewrite reprK. +pose M : int := \sum_(0 <= j < `|k|) (`|f' j| + `|f' (- j%:Z)|). +case/is_qzendoP: (valP f') => /= kf hkf; exists (kf + M) => n. +rewrite -[X in `|X|](subrK (f' (g n - g' n))). +rewrite (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. ++ by rewrite addrAC -addrA -opprD -{1}[g n](subrK (g' n)). +rewrite {}/M (bigD1_seq `|g n - g' n|%N) /=; first last. ++ by apply/iota_uniq. ++ rewrite mem_index_iota /= -ltz_nat abszE. + by apply/(ltr_le_trans (hk _))/ler_norm. +rewrite ler_paddr ?sumr_ge0 // !abszE; case: (ger0P (g n - g' n)) => _. ++ by rewrite ler_addl. ++ by rewrite opprK ler_addr. +Qed. + +Canonical pi_edxmul_morph := PiMorph2 pi_edxmul. + +(* -------------------------------------------------------------------- *) +Section EudoxusZModType. +Local Notation "n %:R" := (to_eudoxus n) : eudoxus_scope. +Local Notation "- f" := (edxopp f ) : eudoxus_scope. +Local Notation "f + g" := (edxadd f g ) : eudoxus_scope. + +(* -------------------------------------------------------------------- *) +Lemma edxzmod : + [/\ associative edxadd + , commutative edxadd + , left_id (0%:R)%E edxadd + & left_inverse (0%:R)%E edxopp edxadd]. +Proof. split. ++ elim/quotW=> f; elim/quotW=> g; elim/quotW=> h /=. + rewrite !piE; apply/eqmodP/qzeqv_refl_eq => n /=. + by rewrite addrA. ++ elim/quotW=> f; elim/quotW=> g; rewrite !piE. + by apply/eqmodP/qzeqv_refl_eq => n /=; rewrite addrC. ++ elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. + by move=> n /=; rewrite /qzendoC mulr0 add0r. ++ elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. + by move=> n /=; rewrite addNr /qzendoC mulr0. +Qed. + +Let edxaddA := let: And4 h _ _ _ := edxzmod in h. +Let edxaddC := let: And4 _ h _ _ := edxzmod in h. +Let edxadd0l := let: And4 _ _ h _ := edxzmod in h. +Let edxaddNl := let: And4 _ _ _ h := edxzmod in h. + +Definition eudoxus_zmodMixin := + ZmodMixin edxaddA edxaddC edxadd0l edxaddNl. +Canonical eudoxus_zmodType := + Eval hnf in ZmodType eudoxus eudoxus_zmodMixin. +End EudoxusZModType. + +(* -------------------------------------------------------------------- *) +Section EudoxusComRingType. +Local Notation "n %:R" := (to_eudoxus n) : eudoxus_scope. +Local Notation "f * g" := (edxmul f g ) : eudoxus_scope. + +Lemma edxcomring : + [/\ associative edxmul + , commutative edxmul + , left_id (1%:R)%E edxmul + , left_distributive edxmul +%R + & (1%:R)%E != 0 ]. +Proof. split. ++ elim/quotW=> f; elim/quotW=> g; elim/quotW=> h. + by rewrite !piE /=; apply/eqmodP/qzeqv_refl_eq. ++ admit. ++ elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. + by move=> n /=; rewrite /qzendoC mulr1. ++ admit. ++ apply/eqP; rewrite !piE => /eqmodP/qzeqvP /= [k hk]. + have := (hk 0); rewrite /qzendoC normr0 => /ltrW ge0k. + move/(_ (k+1)): hk; rewrite /qzendoC !(mulr0, mulr1). + rewrite subr0 ger0_norm ?ler_paddr //. + by apply/negP; rewrite -lerNgt ler_addl. +Admitted. + +Let edxmulA := let: And5 h _ _ _ _ := edxcomring in h. +Let edxmulC := let: And5 _ h _ _ _ := edxcomring in h. +Let edxmul1l := let: And5 _ _ h _ _ := edxcomring in h. +Let edxmulDl := let: And5 _ _ _ h _ := edxcomring in h. +Let edxmul10 := let: And5 _ _ _ _ h := edxcomring in h. + +Definition eudoxus_ringMixin := + ComRingMixin edxmulA edxmulC edxmul1l edxmulDl edxmul10. + +Canonical eudoxus_ringType := Eval hnf in RingType eudoxus eudoxus_ringMixin. +Canonical comRingType := Eval hnf in ComRingType eudoxus edxmulC. +End EudoxusComRingType. From a1a5f586d2ea14be203b8a7a941839faa00de941 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 18 Oct 2018 14:35:50 +0200 Subject: [PATCH 03/13] Eudoxus reals: ring structure + refactoring --- eudoxus.v | 284 +++++++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 230 insertions(+), 54 deletions(-) diff --git a/eudoxus.v b/eudoxus.v index bd767334a7..f2e6e85c6e 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -1,4 +1,4 @@ -(* -------------------------------------------------------------------- *) +(* ==================================================================== *) From mathcomp Require Import all_ssreflect all_algebra. (* ------- *) Require Import boolp classical_sets. @@ -38,77 +38,81 @@ Local Reserved Notation "~%E" (at level 0). (* -------------------------------------------------------------------- *) Delimit Scope eudoxus_scope with E. -(* -------------------------------------------------------------------- *) -Definition is_qzendo (f : int -> int) := - exists k : int, forall m n : int, `|f (m + n) - (f m + f n)| < k. +(* ==================================================================== *) +Definition is_qzendo (k : int) (f : int -> int) := + forall m n, `|f (m + n) - (f m + f n)| < k. -Definition qzEndo := - [qualify a f : int -> int | `[]]. +Definition qzendo (k : int) := + [qualify a f : int -> int | `[]]. -Fact qzendo_key : pred_key qzEndo. Proof. by []. Qed. -Canonical qzendo_keyed := KeyedQualifier qzendo_key. +Fact qzendo_key k : pred_key (qzendo k). Proof. by []. Qed. +Canonical qzendo_keyed k := KeyedQualifier (qzendo_key k). -Record qzendo := QZEndo { qzendof :> int -> int; _ : qzendof \is a qzEndo }. +Notation "k .-qzendo" := (qzendo k) + (at level 1, format "k .-qzendo") : form_scope. -Canonical qzendo_subType := Eval hnf in [subType for qzendof]. +(* -------------------------------------------------------------------- *) +Definition qzendoC (z : int) := fun x : int => x * z. + +Local Notation "z %:E" := (qzendoC z). + +(* ==================================================================== *) +Section QzEndoTheory. -Definition qzendo_eqMixin := Eval hnf in [eqMixin of qzendo by <:]. -Canonical qzendo_eqType := Eval hnf in EqType qzendo qzendo_eqMixin. -Definition qzendo_choiceMixin := [choiceMixin of qzendo by <:]. -Canonical qzendo_choiceType := Eval hnf in ChoiceType qzendo qzendo_choiceMixin. +Implicit Types (k kf kg : int) (f g : int -> int). (* -------------------------------------------------------------------- *) -Lemma is_qzendoP (f : int -> int) : +Lemma is_qzendoP k f : reflect - (exists k : int, forall m n : int, `|f (m + n) - (f m + f n)| < k) - (f \is a qzEndo). + (forall m n : int, `|f (m + n) - (f m + f n)| < k) + (f \is a k.-qzendo). Proof. by apply/asboolP. Qed. -(* -------------------------------------------------------------------- *) -Definition qzendoC (z : int) := fun x : int => x * z. +Lemma is_qzendo_gt0 k f : f \is a k.-qzendo -> 0 < k. +Proof. by move/is_qzendoP => /(_ 0 0) /(ler_lt_trans _); apply. Qed. -Local Notation "z %:E" := (qzendoC z). +Lemma is_qzendo_ge0 k f : f \is a k.-qzendo -> 0 <= k. +Proof. by move=> h; apply/ltrW/(is_qzendo_gt0 h). Qed. Lemma qzendoC_is_additive z : additive (qzendoC z). Proof. by move=> n m; rewrite /qzendoC; rewrite -mulrBl. Qed. Canonical qzendoC_additive z := Additive (qzendoC_is_additive z). -(* -------------------------------------------------------------------- *) -Section QZEndoMorph. -Implicit Types f g : int -> int. - Lemma additive_is_qzendo (f : {additive int -> int}): - GRing.Additive.apply f \is a qzEndo. + GRing.Additive.apply f \is a 1.-qzendo. Proof. -apply/is_qzendoP; exists 1 => n m. -by rewrite [f (_ + _)]raddfD opprD addrACA !subrr normr0. +apply/is_qzendoP => m n; rewrite [f (_ + _)]raddfD. +by rewrite opprD addrACA !subrr normr0. Qed. -Lemma is_qzendoC c : c%:E \is a qzEndo. +Lemma is_qzendoC c : c%:E \is a 1.-qzendo. Proof. by apply: additive_is_qzendo. Qed. -Lemma is_qzendoD f g : - f \is a qzEndo -> g \is a qzEndo -> f \+ g \is a qzEndo. +Lemma is_qzendoD kf kg f g : + f \is a kf.-qzendo + -> g \is a kg.-qzendo + -> f \+ g \is a (kf + kg).-qzendo. Proof. -move=> /is_qzendoP[kf bdf] /is_qzendoP[kg bdg]. -apply/is_qzendoP; exists (kf + kg) => n m /=. -rewrite addrACA opprD addrACA. +move=> /is_qzendoP bdf /is_qzendoP bdg. +apply/is_qzendoP => n m; rewrite addrACA opprD addrACA. by apply/(ler_lt_trans (ler_norm_add _ _))/ltr_add. Qed. -Lemma is_qzendoN f : f \is a qzEndo -> \- f \is a qzEndo. +Lemma is_qzendoN k f : f \is a k.-qzendo -> \- f \is a k.-qzendo. Proof. -case/is_qzendoP=> kf bdf; apply/is_qzendoP; exists kf. +move/is_qzendoP=> bdf; apply/is_qzendoP. by move=> n m /=; rewrite -!opprD normrN. Qed. -Lemma is_qzendoM f g : - f \is a qzEndo -> g \is a qzEndo -> f \o g \is a qzEndo. +Lemma is_qzendoM kf kg f g : + f \is a kf.-qzendo + -> g \is a kg.-qzendo + -> exists k, f \o g \is a k.-qzendo. Proof. -case/is_qzendoP=> kf bdf; case/is_qzendoP=> kg bdg. +move/is_qzendoP=> bdf; move/is_qzendoP=> bdg. pose M : int := \sum_(0 <= i < `|kg|) (`|f i| + `|f (- i%:Z)|). -apply/is_qzendoP; exists (M + kf *+ 2) => m n /=. +exists (M + kf *+ 2); apply/is_qzendoP => m n /=. rewrite -[X in `|X - _|](subrK (f (g m + g n))). rewrite -[X in `|X|]addrA (ler_lt_trans (ler_norm_add _ _)) //. rewrite mulr2n addrA ltr_add //. @@ -124,18 +128,148 @@ rewrite !abszE ler_paddr ?sumr_ge0 //; case: (ger0P k) => _. + by rewrite opprK; apply/ler_addr. Qed. -End QZEndoMorph. +End QzEndoTheory. + +(* ==================================================================== *) +Section QZEndoBd. +Implicit Types (k : int) (f : int -> int). + +Local Lemma qzendo_crossbdL k f : + f \is a k.-qzendo -> forall m n : int, + `|f (m * n) - m * f n| < (`|m| + 1) * k. +Proof. +move=> hf m n; elim/int_rec: m => [|m|m]. +* rewrite !mul0r subr0 mul1r; move/is_qzendoP/(_ 0 0): hf. + by rewrite addr0 opprD addrA subrr add0r normrN. +* rewrite -![`|_%:Z|]abszE !absz_nat => ihm. + rewrite [in X in _ < X]intS -addrA mulrDl mul1r. + have /is_qzendoP/(_ n (m%:Z * n)) lek := hf. + apply/(ler_lt_trans _ (ltr_add lek ihm)). + apply/(ler_trans _ (ler_norm_add _ _)). + rewrite opprD addrA addrACA !addrA addrK. + by rewrite intS !mulrDl !mul1r -addrA -opprD. +* rewrite !normrN -![`|_%:Z|]abszE !absz_nat !mulNr !opprK. + move=> ihm; rewrite [in X in _ < X]intS mulrDl mul1r [1+_]addrC. + have /is_qzendoP/(_ n (- (m.+1%:Z * n))) lek := hf. + apply/(ler_lt_trans _ (ltr_add ihm lek)). + apply/(ler_trans _ (ler_norm_sub _ _)). + rewrite !opprD !opprK !addrA [X in `|X + _ + _|]addrAC. + rewrite [X in n - X * n]intS mulrDl mul1r. + rewrite opprD addrA subrr add0r subrr add0r. + by rewrite addrC intS [1+_]addrC mulrDl mul1r. +Qed. + +Lemma qzendo_crossbd k f : + f \is a k.-qzendo -> forall m n : int, + `|m * f n - n * f m| < (`|m| + `|n| + 2%:R) * k. +Proof. +move=> hf m n; rewrite (natrD _ 1 1) addrACA mulrDl. +have hL := qzendo_crossbdL hf m n. +have hR := qzendo_crossbdL hf n m. +apply/(ler_lt_trans _ (ltr_add hL hR)). +apply/(ler_trans _ (ler_norm_sub _ _)). +rewrite opprB [n * m]mulrC [in X in _ <= X]addrC. +by rewrite !addrA subrK distrC. +Qed. + +Lemma qzendo_sublin k f : + f \is a k.-qzendo -> + exists A B : int, forall m : int, `|f m| < A * `|m| + B. +Proof. +move=> hf; exists (k + `|f 1|); exists (3%:R * k) => m. +have := qzendo_crossbd hf m 1; rewrite mul1r normr1 distrC. +rewrite -addrA -(natrD _ 1 2) -[(1+2)%N]/3 => h. +rewrite mulrDl addrAC [k*_]mulrC -mulrDl. +set M : int := `|f 1| * _; move: h; rewrite -(ltr_add2r M). +move/(ler_lt_trans _); apply; rewrite {}/M. +rewrite -normrM (ler_trans _ (ler_norm_add _ _)) //. +by rewrite [f 1 * _]mulrC subrK. +Qed. + +End QZEndoBd. + +(* ==================================================================== *) +Definition is_eqzendo (f : int -> int) := + exists k, f \is a k.-qzendo. + +Definition eqzendo := + [qualify a f : int -> int | `[]]. + +Fact eqzendo_key : pred_key eqzendo. Proof. by []. Qed. +Canonical eqzendo_keyed := KeyedQualifier eqzendo_key. + +(* ==================================================================== *) +Section EQzEndoTheory. + +Implicit Types (k kf kg : int) (f g : int -> int). + +(* -------------------------------------------------------------------- *) +Lemma is_eqzendoP f : + reflect (exists k, f \is a k.-qzendo) (f \is a eqzendo). +Proof. by apply/asboolP. Qed. + +(* -------------------------------------------------------------------- *) +Lemma is_eqzendoPP f : + reflect + (exists k : int, forall m n : int, `|f (m + n) - (f m + f n)| < k) + (f \is a eqzendo). +Proof. +by apply: (iffP (is_eqzendoP f)) => -[k h]; exists k; apply/is_qzendoP. +Qed. + +(* -------------------------------------------------------------------- *) +Lemma qzendo_eqzendo k f : + f \is a k.-qzendo -> f \is a eqzendo. +Proof. by move=> h; apply/is_eqzendoP; exists k. Qed. + +Lemma is_eqzendoC c : c%:E \is a eqzendo. +Proof. by apply: (qzendo_eqzendo (is_qzendoC _)). Qed. + +Lemma is_eqzendoD f g : + f \is a eqzendo + -> g \is a eqzendo + -> f \+ g \is a eqzendo. +Proof. +move=> /is_eqzendoP[kf hf] /is_eqzendoP[kg hg]. +by apply/(qzendo_eqzendo (is_qzendoD hf hg)). +Qed. + +Lemma is_eqzendoN f : f \is a eqzendo -> \- f \is a eqzendo. +Proof. +by move=> /is_eqzendoP[kf hf]; apply/(qzendo_eqzendo (is_qzendoN hf)). +Qed. + +Lemma is_eqzendoM f g : + f \is a eqzendo + -> g \is a eqzendo + -> f \o g \is a eqzendo. +Proof. +move=> /is_eqzendoP[kf hf] /is_eqzendoP[kg hg]. +by apply/is_eqzendoP/(is_qzendoM hf hg). +Qed. + +End EQzEndoTheory. + +(* ==================================================================== *) +Record qzEndo := QZEndo { qzendof :> int -> int; _ : qzendof \is a eqzendo }. + +Canonical qzendo_subType := Eval hnf in [subType for qzendof]. + +Definition qzendo_eqMixin := Eval hnf in [eqMixin of qzEndo by <:]. +Canonical qzendo_eqType := Eval hnf in EqType qzEndo qzendo_eqMixin. +Definition qzendo_choiceMixin := [choiceMixin of qzEndo by <:]. +Canonical qzendo_choiceType := Eval hnf in ChoiceType qzEndo qzendo_choiceMixin. (* -------------------------------------------------------------------- *) Section QZEqv. -Definition qzeqv (f g : qzendo) := +Definition qzeqv (f g : qzEndo) := `[]. Local Notation "~%E" := qzeqv. Local Notation "f ~ g" := (qzeqv f g). -Lemma qzeqvP (f g : qzendo) : +Lemma qzeqvP (f g : qzEndo) : reflect (exists k : int, forall n : int, `|f n - g n| < k) (f ~ g). @@ -153,7 +287,7 @@ Proof. split. by rewrite [f n - _]addrC addrACA addNr addr0. Qed. -Lemma qzeqv_refl_eq (f g : qzendo) : f =1 g -> f ~ g. +Lemma qzeqv_refl_eq (f g : qzEndo) : f =1 g -> f ~ g. Proof. move=> eq_fg; apply/qzeqvP; exists 1 => n. by rewrite eq_fg subrr normr0. @@ -175,14 +309,14 @@ Local Notation "~%E" := qzeqv. Local Notation "f ~ g" := (qzeqv f g). (* -------------------------------------------------------------------- *) -Definition edxoppf (f : qzendo) : qzendo := - QZEndo (is_qzendoN (valP f)). +Definition edxoppf (f : qzEndo) : qzEndo := + QZEndo (is_eqzendoN (valP f)). -Definition edxaddf (f g : qzendo) : qzendo := - QZEndo (is_qzendoD (valP f) (valP g)). +Definition edxaddf (f g : qzEndo) : qzEndo := + QZEndo (is_eqzendoD (valP f) (valP g)). -Definition edxmulf (f g : qzendo) : qzendo := - QZEndo (is_qzendoM (valP f) (valP g)). +Definition edxmulf (f g : qzEndo) : qzEndo := + QZEndo (is_eqzendoM (valP f) (valP g)). Definition edxopp := lift_op1 eudoxus edxoppf. Definition edxadd := lift_op2 eudoxus edxaddf. @@ -190,7 +324,7 @@ Definition edxmul := lift_op2 eudoxus edxmulf. (* -------------------------------------------------------------------- *) Definition to_eudoxus := - lift_embed eudoxus (fun z : int => QZEndo (is_qzendoC z)). + lift_embed eudoxus (fun z : int => QZEndo (is_eqzendoC z)). Canonical to_eudoxus_pi_morph := PiEmbed to_eudoxus. @@ -228,7 +362,7 @@ apply/(@equiv_trans _ _ (edxmulf f' g)); apply/qzeqvP=> /=. by case/qzeqvP=> [k hk]; exists k. have /qzeqvP[k hk]: g ~ g' by apply/eqmodP; rewrite reprK. pose M : int := \sum_(0 <= j < `|k|) (`|f' j| + `|f' (- j%:Z)|). -case/is_qzendoP: (valP f') => /= kf hkf; exists (kf + M) => n. +case/is_eqzendoPP: (valP f') => /= kf hkf; exists (kf + M) => n. rewrite -[X in `|X|](subrK (f' (g n - g' n))). rewrite (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. + by rewrite addrAC -addrA -opprD -{1}[g n](subrK (g' n)). @@ -292,16 +426,58 @@ Lemma edxcomring : Proof. split. + elim/quotW=> f; elim/quotW=> g; elim/quotW=> h. by rewrite !piE /=; apply/eqmodP/qzeqv_refl_eq. -+ admit. ++ elim/quotW=> f; elim/quotW=> g; rewrite !piE. + case/is_eqzendoP: (valP f) => /= kf hf. + case/is_eqzendoP: (valP g) => /= kg hg. + have [Af [Bf subf]] := qzendo_sublin hf. + have [Ag [Bg subg]] := qzendo_sublin hg. + pose M := (6%:R + (Af + Bf) + (Ag + Bg)) * maxr kf kg. + apply/eqmodP/qzeqvP; exists (maxr M (1 + `|f (g 0) - g (f 0)|)). + move=> n; case: (n =P 0) => /= [->|/eqP nz_n]. + * by rewrite ltr_maxr ltz_add1r lerr orbT. + rewrite ltr_maxr; apply/orP; left; rewrite {}/M. + rewrite -(@ltr_pmul2l _ `|n|) ?normr_gt0 //. + have /= h1 := qzendo_crossbd hf n (g n). + have /= h2 := qzendo_crossbd hg (f n) n. + have {h1 h2} /(ler_lt_trans (ler_norm_add _ _)) := ltr_add h1 h2. + rewrite [g n * _]mulrC ![in X in X < _]addrA subrK -mulrBr normrM. + move/ltr_le_trans; apply; set M := maxr _ _. + set x1 := (X in X * _ + _); set x2 := (X in _ + X * _). + have h1: x1 * kf <= (`|n| * (Ag + 1) + (Bg + 2%:R)) * M. + * apply/ler_pmul; rewrite ?addr_ge0 ?(is_qzendo_ge0 hf) //; last first. + - by rewrite /M ler_maxr lerr orTb. + rewrite {}/x1 !addrA !ler_add2r mulrDr mulr1. + by rewrite addrAC [X in X<=_]addrC ler_add2r mulrC 1?ltrW. + have h2: x2 * kg <= (`|n| * (Af + 1) + (Bf + 2%:R)) * M. + * apply/ler_pmul; rewrite ?addr_ge0 ?(is_qzendo_ge0 hg) //; last first. + - by rewrite /M ler_maxr lerr orbT. + rewrite {}/x2 !addrA !ler_add2r mulrDr mulr1. + by rewrite addrAC ler_add2r mulrC 1?ltrW. + apply/(ler_trans (ler_add h1 h2)); rewrite -mulrDl mulrA. + apply/ler_wpmul2r; first by rewrite ler_maxr (is_qzendo_ge0 hf). + rewrite addrACA -mulrDr => {M h1 h2 x1 x2}. + set M := (X in _ + X <= _); set N := (X in `|n| * X). + apply/(@ler_trans _ (`|n| * (N + M))). + * rewrite mulrDr ler_add2l ler_pemull // ?addr_ge0 //. + - move/(_ 0): subg; rewrite normr0 mulr0 add0r. + by move/(ler_lt_trans _)/(ltrW); apply. + - move/(_ 0): subf; rewrite normr0 mulr0 add0r. + by move/(ler_lt_trans _)/(ltrW); apply. + by rewrite -gtz0_ge1 normr_gt0. + apply/ler_wpmul2l => //; rewrite {}/N {}/M. + rewrite [X in X + _ <= _]addrACA [X in _ + X <= _]addrACA. + rewrite [X in X <= _]addrACA addrC [X in _ + X]addrACA. + by rewrite [X in _ + X <= _]addrC -!addrA. + elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. by move=> n /=; rewrite /qzendoC mulr1. -+ admit. ++ elim/quotW=> f; elim/quotW=> g; elim/quotW=> h. + by rewrite !piE /=; apply/eqmodP/qzeqv_refl_eq. + apply/eqP; rewrite !piE => /eqmodP/qzeqvP /= [k hk]. have := (hk 0); rewrite /qzendoC normr0 => /ltrW ge0k. move/(_ (k+1)): hk; rewrite /qzendoC !(mulr0, mulr1). rewrite subr0 ger0_norm ?ler_paddr //. by apply/negP; rewrite -lerNgt ler_addl. -Admitted. +Qed. Let edxmulA := let: And5 h _ _ _ _ := edxcomring in h. Let edxmulC := let: And5 _ h _ _ _ := edxcomring in h. From c184a930adfeb226ca9d75364338348c793edde2 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 18 Oct 2018 14:36:09 +0200 Subject: [PATCH 04/13] _CoqProject --- _CoqProject | 1 + 1 file changed, 1 insertion(+) diff --git a/_CoqProject b/_CoqProject index 7a4f3889f1..c883fa83dc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -13,6 +13,7 @@ hierarchy.v forms.v derive.v summability.v +eudoxus.v altreals/xfinmap.v altreals/discrete.v altreals/realseq.v From 5e0684f94b0fef9002576990b2ef83ebf3fddb43 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 18 Oct 2018 21:44:27 +0200 Subject: [PATCH 05/13] NumMixin from a "being positive" predicate --- eudoxus.v | 70 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 70 insertions(+) diff --git a/eudoxus.v b/eudoxus.v index f2e6e85c6e..9a20f8f72d 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -15,6 +15,76 @@ Local Open Scope ring_scope. Local Open Scope classical_set_scope. Local Open Scope quotient_scope. +(* -------------------------------------------------------------------- *) +Section PosNumMixin. +Context {F : idomainType} (p : pred F). + +Hypothesis p_N0 : 0 \notin p. +Hypothesis p_1 : 1 \in p. +Hypothesis p_total : forall x, x != 0 -> (x \in p) || (-x \in p). +Hypothesis p_add : {in p &, forall u v, u + v \in p}. +Hypothesis p_mul : {in p &, forall u v, u * v \in p}. + +Definition lt (x y : F) := (y - x) \in p. +Definition le (x y : F) := (x == y) || (lt x y). +Definition norm (x : F) := if x \notin p then -x else x. + +Local Lemma le0D x y : le 0 x -> le 0 y -> le 0 (x + y). +Proof. +rewrite /le /lt !subr0 => /orP[/eqP<-|px]; first by rewrite add0r. +case/orP => [/eqP<-|py]; first by rewrite addr0 px orbT. +by rewrite (p_add px py) orbT. +Qed. + +Local Lemma le0M x y : le 0 x -> le 0 y -> le 0 (x * y). +Proof. +rewrite /le /lt !subr0 => /orP[/eqP<-|px]; first by rewrite mul0r eqxx. +case/orP=> [/eqP<-|py]; first by rewrite mulr0 eqxx. +by rewrite (p_mul px py) orbT. +Qed. + +Local Lemma le_anti x : le 0 x -> le x 0 -> x = 0. +Proof. +rewrite /le /lt subr0 sub0r => /orP[/eqP<-//|px] /orP[/eqP<-//|pxN]. +by apply/contraNeq: p_N0 => _; rewrite -[0](subrr x) p_add. +Qed. + +Local Lemma sub_ge0 x y : le 0 (y - x) = le x y. +Proof. by rewrite /le /lt subr0 [0==_]eq_sym subr_eq0 eq_sym. Qed. + +Local Lemma le_total x : le 0 x || le x 0. +Proof. +rewrite /le /lt [0==_]eq_sym orbCA !orbA orbb subr0 sub0r. +by case: eqP => //= /eqP /p_total. +Qed. + +Local Lemma normN x : norm (- x) = norm x. +Proof. +have h v : v != 0 -> (v \in p) = (-v \notin p). +* move=> nz_v; apply/idP/idP => [pv|Npv]. + - by apply/contra: p_N0 => /(p_add pv); rewrite subrr. + - by have := p_total nz_v; rewrite (negbTE Npv) orbF. +rewrite /norm !if_neg opprK; case: (x =P 0) => [->|/eqP nz_x]. +* by rewrite oppr0 (negbTE p_N0). +by apply/esym; rewrite h // if_neg. +Qed. + +Local Lemma ge0_norm x : le 0 x -> norm x = x. +Proof. +rewrite /norm /le /lt subr0. +by case/orP=> [/eqP<-|->//]; rewrite p_N0 oppr0. +Qed. + +Local Lemma lt_def x y : lt x y = (y != x) && le x y. +Proof. +rewrite /le /lt eq_sym; case: eqP=> //= ->. +by rewrite subrr (negbTE p_N0). +Qed. + +Definition PosNumMixin := + RealLeMixin le0D le0M le_anti sub_ge0 le_total normN ge0_norm lt_def. +End PosNumMixin. + (* -------------------------------------------------------------------- *) Reserved Notation "\- f" (at level 40, left associativity). From f61be6687119dde837c793f381ce49f219b14e36 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 23 Oct 2018 19:20:03 +0200 Subject: [PATCH 06/13] core lemma for eudoxus reals classification wrt 0 --- eudoxus.v | 163 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 159 insertions(+), 4 deletions(-) diff --git a/eudoxus.v b/eudoxus.v index 9a20f8f72d..f52fcf84bd 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -8,6 +8,7 @@ From mathcomp Require Import all_ssreflect all_algebra. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Unset SsrOldRewriteGoalsOrder. Import GRing.Theory Num.Def Num.Theory. @@ -189,10 +190,10 @@ rewrite mulr2n addrA ltr_add //. rewrite -[X in `|X|](subrK (f (g (m + n) - (g m + g n)))). rewrite [X in _ < X]addrC (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. + by rewrite addrAC -{1}[g (m + n)](subrK (g m + g n)) -addrA -opprD. -rewrite {}/M; set k := g _ - _; rewrite (bigD1_seq `|k|%N) /=; first last. -+ by apply/iota_uniq. +rewrite {}/M; set k := g _ - _; rewrite (bigD1_seq `|k|%N) /=. + rewrite mem_index_iota /k /= -ltz_nat !abszE. by apply/(ltr_le_trans (bdg _ _))/ler_norm. ++ by apply/iota_uniq. rewrite !abszE ler_paddr ?sumr_ge0 //; case: (ger0P k) => _. + by apply/ler_addl. + by rewrite opprK; apply/ler_addr. @@ -318,6 +319,29 @@ move=> /is_eqzendoP[kf hf] /is_eqzendoP[kg hg]. by apply/is_eqzendoP/(is_qzendoM hf hg). Qed. +Lemma eqzendo_suplin f (D : int) : + 0 < D + -> f \is a eqzendo + -> (forall k : int, exists2 n : int, 0 < n & k < f n) + -> exists2 N : int, 0 < N & forall m : int, 0 < m -> f (m * N) > (m + 1) * D. +Proof. +move=> ge0_D edf infp; case/is_eqzendoPP: edf => C edfC. +pose E : int := C + D; case: (infp (2%:R * E)) => N gt0_n gt_E_fN. +exists N => //; case=> // k gt0_k; apply/(@ltr_trans _ ((k%:Z + 1) * E)). ++ rewrite ltr_pmul2l; first by rewrite addrC ltz_add1r. + by rewrite ltr_addr (ler_lt_trans _ (edfC 0 0)). +case: k gt0_k => // k _; rewrite [_+1]addrC -intS. +elim: k => [|k ihk]; first by rewrite mul1r. +move: k.+1 ihk => {k} k ihk; have := edfC (k%:Z * N) N. +rewrite ltr_norml => /andP[h _]; move: h. +rewrite ltr_subr_addl (_ : k%:Z * N + N = (k.+1)%:Z * N). ++ by rewrite intS mulrDl mul1r addrC. +move/(ltr_trans _); apply; rewrite intS mulrDl mul1r addrC -addrA. +apply: ltr_add => //; rewrite ltr_subr_addl. +apply: (ltr_trans _ gt_E_fN); rewrite mulr_natl mulr2n. +by rewrite ltr_add2r /E ltr_addl. +Qed. + End EQzEndoTheory. (* ==================================================================== *) @@ -436,10 +460,10 @@ case/is_eqzendoPP: (valP f') => /= kf hkf; exists (kf + M) => n. rewrite -[X in `|X|](subrK (f' (g n - g' n))). rewrite (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. + by rewrite addrAC -addrA -opprD -{1}[g n](subrK (g' n)). -rewrite {}/M (bigD1_seq `|g n - g' n|%N) /=; first last. -+ by apply/iota_uniq. +rewrite {}/M (bigD1_seq `|g n - g' n|%N) /=. + rewrite mem_index_iota /= -ltz_nat abszE. by apply/(ltr_le_trans (hk _))/ler_norm. ++ by apply/iota_uniq. rewrite ler_paddr ?sumr_ge0 // !abszE; case: (ger0P (g n - g' n)) => _. + by rewrite ler_addl. + by rewrite opprK ler_addr. @@ -561,3 +585,134 @@ Definition eudoxus_ringMixin := Canonical eudoxus_ringType := Eval hnf in RingType eudoxus eudoxus_ringMixin. Canonical comRingType := Eval hnf in ComRingType eudoxus edxmulC. End EudoxusComRingType. + +(* ==================================================================== *) +Section EudoxusFieldType. + +Parameter (edxinv : eudoxus -> eudoxus). + +Lemma edxfield : + (forall x, x != 0 -> edxinv x * x = 1) + /\ (edxinv 0 = 0). +Proof. Admitted. + +Definition eudoxus_fieldUnitMixin := + FieldUnitMixin edxfield.1 edxfield.2. +Canonical eudoxus_unitRing := + Eval hnf in UnitRingType eudoxus eudoxus_fieldUnitMixin. +Canonical eudoxus_comUnitRing := + Eval hnf in [comUnitRingType of eudoxus]. + +Local Fact eudoxus_field_axiom : GRing.Field.mixin_of eudoxus_unitRing. +Proof. exact. Qed. + +Definition RatFieldIdomainMixin := + FieldIdomainMixin eudoxus_field_axiom. +Canonical eudoxus_iDomain := + Eval hnf in IdomainType eudoxus (FieldIdomainMixin eudoxus_field_axiom). +Canonical eudoxus_fieldType := + Eval hnf in FieldType eudoxus eudoxus_field_axiom. + +End EudoxusFieldType. + +(* ==================================================================== *) +Section EudoxusPos. +Definition edxposf (f : qzEndo) := + forall c : int, 0 < c -> exists N : int, + forall n : int, N < n -> c < f n. + +Local Lemma edxposf_spec (f : int -> int) C : + 0 < C + -> f \is a eqzendo + -> (forall k : int, exists2 n : int, 0 < n & k < f n) + -> exists N : int, forall p : int, N < p -> C < f p. +Proof. +move=> ge0_D edf posf; case/is_eqzendoPP: {+}edf => D edfD. +have [|M gt0_M slf] := eqzendo_suplin _ (D := D) edf posf. ++ by apply: (ler_lt_trans _ (edfD 0 0)). +pose g (p : int) := f (p - (p %% M)%Z). +pose E : int := \sum_(0 <= i < `|M|) `|f i|. +have bd_fBg p : `|f p - g p| < E + D. ++ rewrite /g {1 2}[p](divz_eq _ M) addrK (addrC E D). + rewrite -[X in `|X|](subrK (f (p %% M)%Z)). + apply/(ler_lt_trans (ler_norm_add _ _))/ltr_le_add. + * by rewrite -addrA -opprD. + rewrite /E (bigD1_seq (absz (p %% M)%Z)) /=. + * rewrite mem_index_iota /= -ltz_nat !abszE ger0_norm. + - by rewrite modz_ge0 //gtr_eqF. + by rewrite gtr0_norm // ltz_pmod. + * by apply: iota_uniq. + * rewrite abszE [`|(_ %% _)%Z|]ger0_norm ?modz_ge0 ?gtr_eqF //. + by rewrite ler_addl sumr_ge0. +pose n : int := ((E + D + C) %/ D)%Z; exists (n * M) => p ltp. +have := bd_fBg p; rewrite ltr_norml => /andP[h _]; move: h. +rewrite ltr_subr_addl => /(ltr_trans _); apply. +rewrite ltr_subr_addl /g {1}[p](divz_eq _ M) addrK. +apply/(ler_lt_trans _ (slf _ _)); last first. ++ suff ltMp: M < p. + - rewrite -(ltr_pmul2r gt0_M) mul0r -[X in _ int) : f \is a eqzendo -> + [\/ exists C : int, forall n, `|f n| < C + , forall C : int, 0 < C -> exists N : int, forall p : int, N < p -> C < f p + | forall C : int, 0 < C -> exists N : int, forall p : int, N < p -> f p < -C]. +Proof. +move=> edzf; pose P := exists C : int, forall n : int, `|f n| < C. +case/asboolP: {+}P => [hP|hNP]; first by constructor 1. +pose Qpos := forall k : int, exists2 n : int, 0 < n & k < f n. +pose Qneg := forall k : int, exists2 n : int, 0 < n & f n < k. +case/asboolP: {+}Qpos => [hQpos|hNQpos]. ++ by constructor 2 => C gt0_C; apply: edxposf_spec. +case/asboolP: {+}Qneg => [hQneg|hNQneg]. ++ constructor 3 => c gt0_C; case: (edxposf_spec (f := \- f) gt0_C). + * by apply/is_eqzendoN. + * move=> k; case: (hQneg (-k))=> n gt0_n h. + by exists n => //=; rewrite ltr_oppr. + by move=> N hN; exists N => p /hN /=; rewrite ltr_oppr. +have: exists2 c : int, 0 < c & forall n : int, 0 < n -> f n < c. ++ move/asboolPn/existsp_asboolPn: hNQpos => [c hc]. + exists (maxr 0 c + 1); first by rewrite ltz_addr1 ler_maxr lerr. + move=> n gt0_n; rewrite ltz_addr1 ler_maxr -(rwP orP); right. + by rewrite lerNgt -(rwP negP) => h; apply/hc; exists n. +have: exists2 c : int, 0 < c & forall n : int, 0 < n -> - c < f n. ++ move/asboolPn/existsp_asboolPn: hNQneg => [c hc]. + exists (maxr (1 - c) 1); first by rewrite ltr_maxr ltr01 orbT. + move=> n gt0_n; rewrite ltr_oppl ltr_maxr -(rwP orP); left. + rewrite ltr_oppl opprB ltr_subl_addr ltz_addr1. + by rewrite lerNgt -(rwP negP) => h; apply/hc; exists n. +case=> [cN gt0_cN hN] [cP gt0_cP hP]. +have: exists2 C : int, 0 < C & forall n : int, 0 < n -> `|f n| < C. ++ exists (maxr cP cN); first by rewrite ltr_maxr gt0_cP. + move=> n gt0_n; rewrite ltr_norml ltr_oppl !ltr_maxr. + by rewrite hP //= andbT [X in _ || X]ltr_oppl hN // orbT. +case=> C gt0_C hC; case/is_eqzendoPP: edzf=> D hD. +have gt0_D: 0 < D by apply/(ler_lt_trans _ (hD 0 0)). +absurd False => //; apply/hNP; exists (C + D + `|f 1|). +move=> n; case: (ltrP 0 n) => [gt0_n|le0_n]. ++ rewrite -addrA (ltr_trans (hC _ gt0_n)) // ltr_addl. + by rewrite (ltr_le_trans gt0_D) // ler_addl. +have: `|f (1 - n)| < C by apply: hC; rewrite subr_gt0. +rewrite -addrA -(ltr_add2r (D + `|f 1|)) => /(ler_lt_trans _); apply. +rewrite addrCA; have := hD (1 - n) n; rewrite subrK. +rewrite -(ltr_add2r (`|f (1 - n)| + `|f 1|)). +move/ltrW/(ler_trans _); apply. set x := (X in _ <= X + _). +have := ler_norm_sub (f (1 - n)) (f 1); rewrite -(ler_add2l x). +move/(ler_trans _); apply; apply/(ler_trans _ (ler_norm_add _ _)). +rewrite [X in _ <= `|X|]addrC !addrA subrK. +by rewrite opprD addrCA addKr normrN. +Qed. + +End EudoxusPos. From 57da9d76a1175fbf101859d7c86019deb0e6aef8 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Tue, 23 Oct 2018 21:53:12 +0200 Subject: [PATCH 07/13] Completed proof that eudoxus reals form an ordered num domain --- eudoxus.v | 117 ++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 104 insertions(+), 13 deletions(-) diff --git a/eudoxus.v b/eudoxus.v index f52fcf84bd..f543d8babe 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -21,7 +21,6 @@ Section PosNumMixin. Context {F : idomainType} (p : pred F). Hypothesis p_N0 : 0 \notin p. -Hypothesis p_1 : 1 \in p. Hypothesis p_total : forall x, x != 0 -> (x \in p) || (-x \in p). Hypothesis p_add : {in p &, forall u v, u + v \in p}. Hypothesis p_mul : {in p &, forall u v, u * v \in p}. @@ -617,17 +616,16 @@ End EudoxusFieldType. (* ==================================================================== *) Section EudoxusPos. -Definition edxposf (f : qzEndo) := - forall c : int, 0 < c -> exists N : int, - forall n : int, N < n -> c < f n. - -Local Lemma edxposf_spec (f : int -> int) C : - 0 < C - -> f \is a eqzendo +Local Lemma edxposf_spec (f : int -> int) (C : int) : + f \is a eqzendo -> (forall k : int, exists2 n : int, 0 < n & k < f n) -> exists N : int, forall p : int, N < p -> C < f p. Proof. -move=> ge0_D edf posf; case/is_eqzendoPP: {+}edf => D edfD. +move=> edf posf; wlog: C / 0 < C => [wlog|]. ++ case: (ltrP 0 C) => [gt0_C|le0_C]; first by apply: wlog. + case: (wlog 1) => // N hN; exists N => p /hN. + by move/(ler_lt_trans _); apply; apply/(ler_trans le0_C). +move=> gt0_C; case/is_eqzendoPP: {+}edf => D edfD. have [|M gt0_M slf] := eqzendo_suplin _ (D := D) edf posf. + by apply: (ler_lt_trans _ (edfD 0 0)). pose g (p : int) := f (p - (p %% M)%Z). @@ -665,19 +663,29 @@ rewrite -divz_eq -[X in _ <= X]addrA ler_addl addrC subr_ge0. by rewrite ltrW // ltz_pmod // (ler_lt_trans _ (edfD 0 0)). Qed. +(* -------------------------------------------------------------------- *) +Local Lemma edxzero_spec (f : qzEndo) : + (exists C : int, forall n, `|f n| < C) + -> f ~ QZEndo (is_eqzendoC 0). +Proof. +case=> C hfC; apply/qzeqvP; rewrite /qzendoC. +by exists C => n /=; rewrite mulr0 subr0. +Qed. + +(* -------------------------------------------------------------------- *) Local Lemma edxcmp0_spec (f : int -> int) : f \is a eqzendo -> [\/ exists C : int, forall n, `|f n| < C - , forall C : int, 0 < C -> exists N : int, forall p : int, N < p -> C < f p - | forall C : int, 0 < C -> exists N : int, forall p : int, N < p -> f p < -C]. + , forall C : int, exists N : int, forall p : int, N < p -> C < f p + | forall C : int, exists N : int, forall p : int, N < p -> f p < -C]. Proof. move=> edzf; pose P := exists C : int, forall n : int, `|f n| < C. case/asboolP: {+}P => [hP|hNP]; first by constructor 1. pose Qpos := forall k : int, exists2 n : int, 0 < n & k < f n. pose Qneg := forall k : int, exists2 n : int, 0 < n & f n < k. case/asboolP: {+}Qpos => [hQpos|hNQpos]. -+ by constructor 2 => C gt0_C; apply: edxposf_spec. ++ by constructor 2 => C; apply: edxposf_spec. case/asboolP: {+}Qneg => [hQneg|hNQneg]. -+ constructor 3 => c gt0_C; case: (edxposf_spec (f := \- f) gt0_C). ++ constructor 3 => C; case: (edxposf_spec (f := \- f) C). * by apply/is_eqzendoN. * move=> k; case: (hQneg (-k))=> n gt0_n h. by exists n => //=; rewrite ltr_oppr. @@ -715,4 +723,87 @@ rewrite [X in _ <= `|X|]addrC !addrA subrK. by rewrite opprD addrCA addKr normrN. Qed. +(* -------------------------------------------------------------------- *) +Definition edxposf (f : qzEndo) := + `[]. + +Definition edxpos := lift_fun1 eudoxus edxposf. + +(* -------------------------------------------------------------------- *) +Lemma edxposfP (f : qzEndo) : + reflect + (forall k : int, exists2 n : int, 0 < n & k < f n) + (edxposf f). +Proof. by apply/asboolP. Qed. + +(* -------------------------------------------------------------------- *) +Local Lemma pi_edxpos_r (f g : qzEndo) : f ~ g -> edxposf f -> edxposf g. +Proof. +case/qzeqvP=> C bdC /edxposfP /edxposf_spec h. +apply/edxposfP => k; case/(_ (C + k) (valP _)): h. +move=> N hN; exists (maxr 0 N + 1); first by rewrite ltz_addr1 ler_maxr. +set p : int := maxr _ _ + _; have := bdC p; rewrite distrC. +rewrite ltr_norml => /andP[h _]; move: h. +rewrite ltr_subr_addl => /(ltr_trans _); apply. +rewrite ltr_subr_addl; apply: hN; rewrite ltz_addr1. +by rewrite ler_maxr lerr orbT. +Qed. + +(* -------------------------------------------------------------------- *) +Lemma pi_edxpos : {mono \pi_eudoxus : f / edxposf f >-> edxpos f}. +Proof. +move=> f; unlock edxpos; apply/idP/idP; apply: pi_edxpos_r; + by apply/eqmodP; rewrite reprK. +Qed. + +Canonical pi_edxpos_morph := PiMono1 pi_edxpos. + +(* -------------------------------------------------------------------- *) +Lemma edxpos_order : + [/\ 0 \notin edxpos + , (forall x : eudoxus, x != 0 -> (x \in edxpos) || (-x \in edxpos)) + , {in edxpos &, forall u v : eudoxus, u + v \in edxpos} + & {in edxpos &, forall u v : eudoxus, u * v \in edxpos} ]. +Proof. split. ++ rewrite !piE; apply/edxposfP => /(_ 1) [n _] /=. + by rewrite /qzendoC mulr0. ++ elim/quotW=> f; rewrite !piE /= => h. + case: (edxcmp0_spec (valP f)) => /= [|hf|hNf]; first last. + + apply/orP; right; apply/edxposfP => /= k; case: (hNf k). + move=> N hN; exists (`|N| + 1); first by rewrite ltz_addr1. + by rewrite ltr_oppr hN // ltz_addr1 ler_norm. + + apply/orP; left; apply/edxposfP => /= k; case: (hf k). + move=> N hN; exists (`|N| + 1); first by rewrite ltz_addr1. + by rewrite hN // ltz_addr1 ler_norm. + by move/edxzero_spec; rewrite (negbTE h). ++ elim/quotW=> f; elim/quotW=> g; rewrite !piE /=. + move=> /edxposfP hf /edxposfP hg; apply/edxposfP => k. + case/(edxposf_spec `|k| (valP _)): hf => /= kf hkf. + case/(edxposf_spec `|k| (valP _)): hg => /= kg hkg. + exists (maxr 0 (maxr kf kg) + 1); first by rewrite ltz_addr1 ler_maxr. + apply/(@ler_lt_trans _ (`|k| + `|k|)). + * by apply/(ler_trans (ler_norm _))/ler_addr. + by rewrite ltr_add ?(hkf, hkg) // ltz_addr1 !ler_maxr lerr !orbT. ++ elim/quotW=> f; elim/quotW=> g; rewrite !piE /=. + move=> /edxposfP hf /edxposfP hg; apply/edxposfP => k. + case/(edxposf_spec `|k | (valP _)): hf => /= kf hkf. + case/(edxposf_spec `|kf| (valP _)): hg => /= kg hkg. + exists (`|kg| + 1); first by rewrite ltz_addr1. + apply/(ler_lt_trans (ler_norm _))/hkf. + apply/(ler_lt_trans (ler_norm _))/hkg. + by rewrite ltz_addr1 ler_norm. +Qed. + +(* -------------------------------------------------------------------- *) +Let edxpos_N0 := let: And4 h _ _ _ := edxpos_order in h. +Let edxpos_total := let: And4 _ h _ _ := edxpos_order in h. +Let edxpos_add := let: And4 _ _ h _ := edxpos_order in h. +Let edxpos_mul := let: And4 _ _ _ h := edxpos_order in h. + +(* -------------------------------------------------------------------- *) +Definition eudoxus_numMixin := + PosNumMixin edxpos_N0 edxpos_total edxpos_add edxpos_mul. + +Canonical eudoxus_numType := + Eval hnf in NumDomainType eudoxus eudoxus_numMixin. End EudoxusPos. From 956ed96a37da71e029cde74a954a667a9fe87a8d Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 25 Oct 2018 12:37:58 +0200 Subject: [PATCH 08/13] eudoxus reals: prove the Archimedean property --- eudoxus.v | 110 +++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 76 insertions(+), 34 deletions(-) diff --git a/eudoxus.v b/eudoxus.v index f543d8babe..f4db2c02d4 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -583,36 +583,15 @@ Definition eudoxus_ringMixin := Canonical eudoxus_ringType := Eval hnf in RingType eudoxus eudoxus_ringMixin. Canonical comRingType := Eval hnf in ComRingType eudoxus edxmulC. -End EudoxusComRingType. - -(* ==================================================================== *) -Section EudoxusFieldType. - -Parameter (edxinv : eudoxus -> eudoxus). - -Lemma edxfield : - (forall x, x != 0 -> edxinv x * x = 1) - /\ (edxinv 0 = 0). -Proof. Admitted. - -Definition eudoxus_fieldUnitMixin := - FieldUnitMixin edxfield.1 edxfield.2. -Canonical eudoxus_unitRing := - Eval hnf in UnitRingType eudoxus eudoxus_fieldUnitMixin. -Canonical eudoxus_comUnitRing := - Eval hnf in [comUnitRingType of eudoxus]. -Local Fact eudoxus_field_axiom : GRing.Field.mixin_of eudoxus_unitRing. -Proof. exact. Qed. - -Definition RatFieldIdomainMixin := - FieldIdomainMixin eudoxus_field_axiom. -Canonical eudoxus_iDomain := - Eval hnf in IdomainType eudoxus (FieldIdomainMixin eudoxus_field_axiom). -Canonical eudoxus_fieldType := - Eval hnf in FieldType eudoxus eudoxus_field_axiom. +Lemma edxnatrE n : n%:R = \pi_eudoxus (QZEndo (is_eqzendoC n)) :> eudoxus. +Proof. +rewrite !piE; elim: n => [|n ihn]; first by rewrite mulr0n !piE. +rewrite mulrS ihn !piE; apply/eqmodP/qzeqv_refl_eq => /=. +by move=> k; rewrite /qzendoC /= -mulrDr intS. +Qed. -End EudoxusFieldType. +End EudoxusComRingType. (* ==================================================================== *) Section EudoxusPos. @@ -793,17 +772,80 @@ Proof. split. apply/(ler_lt_trans (ler_norm _))/hkg. by rewrite ltz_addr1 ler_norm. Qed. +End EudoxusPos. -(* -------------------------------------------------------------------- *) +(* ==================================================================== *) +Section EudoxusFieldType. + +Parameter (edxinv : eudoxus -> eudoxus). + +Lemma edxfield : + (forall x, x != 0 -> edxinv x * x = 1) + /\ (edxinv 0 = 0). +Proof. Admitted. + +Definition eudoxus_fieldUnitMixin := + FieldUnitMixin edxfield.1 edxfield.2. +Canonical eudoxus_unitRing := + Eval hnf in UnitRingType eudoxus eudoxus_fieldUnitMixin. +Canonical eudoxus_comUnitRing := + Eval hnf in [comUnitRingType of eudoxus]. + +Local Fact eudoxus_field_axiom : GRing.Field.mixin_of eudoxus_unitRing. +Proof. exact. Qed. + +Definition RatFieldIdomainMixin := + FieldIdomainMixin eudoxus_field_axiom. +Canonical eudoxus_iDomain := + Eval hnf in IdomainType eudoxus (FieldIdomainMixin eudoxus_field_axiom). +Canonical eudoxus_fieldType := + Eval hnf in FieldType eudoxus eudoxus_field_axiom. + +End EudoxusFieldType. + +(* ==================================================================== *) +Section EudoxusNum. Let edxpos_N0 := let: And4 h _ _ _ := edxpos_order in h. Let edxpos_total := let: And4 _ h _ _ := edxpos_order in h. Let edxpos_add := let: And4 _ _ h _ := edxpos_order in h. Let edxpos_mul := let: And4 _ _ _ h := edxpos_order in h. -(* -------------------------------------------------------------------- *) -Definition eudoxus_numMixin := +Definition eudoxus_numDomainMixin := PosNumMixin edxpos_N0 edxpos_total edxpos_add edxpos_mul. -Canonical eudoxus_numType := - Eval hnf in NumDomainType eudoxus eudoxus_numMixin. -End EudoxusPos. +Canonical eudoxus_numDomainType := + Eval hnf in NumDomainType eudoxus eudoxus_numDomainMixin. +Canonical eudoxus_numFieldType := + Eval hnf in [numFieldType of eudoxus]. +Canonical eudoxus_realDomainType := + Eval hnf in RealDomainType eudoxus (le_total edxpos_total). +Canonical eudoxus_realFieldType := + Eval hnf in [realFieldType of eudoxus]. + +Fact edx_ltrE (f g : eudoxus) : (f < g) = ((g - f) \in edxpos). +Proof. by []. Qed. + +Fact eudoxus_archimedean : + Num.archimedean_axiom [numDomainType of eudoxus]. +Proof. +suff: forall f : eudoxus, exists ub : nat, f < ub%:R. ++ by move=> wlog f; case: ler0P. +elim/quotW=> /= f; have /is_eqzendoP[C /qzendo_sublin] /= := valP f. +case=> [A] [B] ltf; exists `|A|%N.+1; rewrite edx_ltrE /=. +rewrite edxnatrE !piE; apply/edxposfP => /=; rewrite /qzendoC => k. +have {ltf} ltf (m : int) : 0 < m -> f m < `|A| * m + B. ++ move=> gt0_m; apply/(ler_lt_trans (ler_norm _)). + apply/(ltr_le_trans (ltf m)); rewrite ler_add2r. + by rewrite gtr0_norm // ler_pmul2r // ler_norm. +exists (`|k + B| + 1); first by rewrite ltz_addr1. +rewrite ltr_subr_addl -ltr_subr_addr. +rewrite (ltr_trans (ltf _ _)) ?ltz_addr1 //. +rewrite intS [1+_]addrC [in X in _ < X]mulrDr mulr1. +rewrite [`|A|*_]mulrC -addrA ler_lt_add //. +by rewrite ltr_subr_addl ltz_addr1 ler_norm. +Qed. + +Canonical eudoxus_archiType := + Eval hnf in ArchiFieldType eudoxus eudoxus_archimedean. + +End EudoxusNum. From d85ff0d4959fcc1de4ade43c99999f1847a28f89 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 25 Oct 2018 12:40:53 +0200 Subject: [PATCH 09/13] nits --- eudoxus.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/eudoxus.v b/eudoxus.v index f4db2c02d4..34dcd1e04d 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -794,7 +794,7 @@ Canonical eudoxus_comUnitRing := Local Fact eudoxus_field_axiom : GRing.Field.mixin_of eudoxus_unitRing. Proof. exact. Qed. -Definition RatFieldIdomainMixin := +Definition eudoxus_FieldIdomainMixin := FieldIdomainMixin eudoxus_field_axiom. Canonical eudoxus_iDomain := Eval hnf in IdomainType eudoxus (FieldIdomainMixin eudoxus_field_axiom). From 96c66403deb0791d0490ac2ca105381d3af48df3 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 25 Oct 2018 16:01:29 +0200 Subject: [PATCH 10/13] qzendo from qzendo on nat --- eudoxus.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/eudoxus.v b/eudoxus.v index 34dcd1e04d..02f8d643c4 100644 --- a/eudoxus.v +++ b/eudoxus.v @@ -198,6 +198,23 @@ rewrite !abszE ler_paddr ?sumr_ge0 //; case: (ger0P k) => _. + by rewrite opprK; apply/ler_addr. Qed. +Lemma is_qzendo_nat k f : + (forall m n : nat, `|f (m + n)%:Z - (f m + f n)| < k) + -> (forall n : nat, - f(- n%:Z) = f n) + -> f \is a k.-qzendo. +Proof. +move=> qzf fN; have h m n: `|f (m%:Z - n%:Z) - (f m + (f (- n%:Z)))| < k. ++ rewrite -[f (-_)]opprK fN opprB addrA; case: (ltnP m n) => [lt_mn|ge_nm]. + * have := qzf (n - m)%N m; rewrite subnK 1?ltnW // opprD addrCA addrA. + by rewrite -fN opprK -subzn 1?ltnW // opprB. + * have := qzf n (m - n)%N; rewrite addnC subnK //. + by rewrite opprD -distrC -opprB opprK subzn. +apply/is_qzendoP; case=> [] m [] n; rewrite ?NegzE -?PoszD //. ++ by rewrite [_ + n%:Z]addrC [_ + f n]addrC. ++ rewrite opprD !fN -opprD -PoszD -[X in `|X + _|]opprK. + by rewrite fN addrC distrC. +Qed. + End QzEndoTheory. (* ==================================================================== *) From a99930294d832b8e482396b1687249c062f1338e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 25 Oct 2019 09:01:23 +0200 Subject: [PATCH 11/13] Draft --- theories/eudoxus.v | 236 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 200 insertions(+), 36 deletions(-) diff --git a/theories/eudoxus.v b/theories/eudoxus.v index 02f8d643c4..de7667674b 100644 --- a/theories/eudoxus.v +++ b/theories/eudoxus.v @@ -13,6 +13,7 @@ Unset SsrOldRewriteGoalsOrder. Import GRing.Theory Num.Def Num.Theory. Local Open Scope ring_scope. +Local Open Scope int_scope. Local Open Scope classical_set_scope. Local Open Scope quotient_scope. @@ -373,11 +374,19 @@ Canonical qzendo_choiceType := Eval hnf in ChoiceType qzEndo qzendo_choiceMixi (* -------------------------------------------------------------------- *) Section QZEqv. -Definition qzeqv (f g : qzEndo) := - `[]. +Definition eqv {T : Type} (f g : T -> int) := + `[]. -Local Notation "~%E" := qzeqv. -Local Notation "f ~ g" := (qzeqv f g). +Definition qzeqv (f g : qzEndo) := eqv f g. + +Local Notation "~%E" := eqv. +Local Notation "f ~ g" := (eqv f g). + +Lemma eqvP {T : Type} (f g : T -> int) : + reflect + (exists k : int, forall n : T, `|f n - g n| < k) + (f ~ g). +Proof. by apply: asboolP. Qed. Lemma qzeqvP (f g : qzEndo) : reflect @@ -385,38 +394,57 @@ Lemma qzeqvP (f g : qzEndo) : (f ~ g). Proof. by apply: asboolP. Qed. -Lemma qzeqv_is_equiv : equiv_class_of ~%E. +Lemma eqv_is_equiv {T : Type} : equiv_class_of (@eqv T). Proof. split. -+ by move=> f; apply/qzeqvP; exists 1 => n; rewrite subrr normr0. -+ suff sym f g: f ~ g -> g ~ f by move=> f g; apply/idP/idP => /sym. - by case/qzeqvP=> [k hk]; apply/qzeqvP; exists k=> n; rewrite distrC. -+ move=> f g h /qzeqvP[k1 h1] /qzeqvP[k2 h2]. - apply/qzeqvP; exists (k1 + k2) => n. ++ by move=> f; apply/eqvP; exists 1 => n; rewrite subrr normr0. ++ suff sym (f g : T -> int): f ~ g -> g ~ f. + - by move=> f g; apply/idP/idP => /sym. + by case/eqvP => [k hk]; apply/eqvP; exists k=> n; rewrite distrC. ++ move=> f g h /eqvP[k1 h1] /eqvP[k2 h2]. + apply/eqvP; exists (k1 + k2) => n. apply/(ler_lt_trans _ (ltr_add (h1 n) (h2 n))). apply/(ler_trans _ (ler_norm_add _ _)). by rewrite [f n - _]addrC addrACA addNr addr0. Qed. -Lemma qzeqv_refl_eq (f g : qzEndo) : f =1 g -> f ~ g. +Lemma qzeqv_is_equiv : equiv_class_of qzeqv. Proof. -move=> eq_fg; apply/qzeqvP; exists 1 => n. +case: (@eqv_is_equiv int) => hr hs ht; split. ++ by apply: hr. + by apply: hs. + by apply: ht. +Qed. + +Lemma eqv_refl_eq (f g : int -> int) : f =1 g -> f ~ g. +Proof. +move=> eq_fg; apply/eqvP; exists 1 => n. by rewrite eq_fg subrr normr0. Qed. +Canonical eqv_equiv T := EquivRelPack (@eqv_is_equiv T). Canonical qzeqv_equiv := EquivRelPack qzeqv_is_equiv. -Canonical qzeqv_encModRel := defaultEncModRel ~%E. +Canonical qzeqv_encModRel := defaultEncModRel qzeqv. + +Definition eudoxus := {eq_quot qzeqv}. + +Canonical eudoxus_quotType := [quotType of eudoxus]. +Canonical eudoxus_eqType := [eqType of eudoxus]. +Canonical eudoxus_choiceType := [choiceType of eudoxus]. +Canonical eudoxus_eqQuotType := [eqQuotType qzeqv of eudoxus]. + +Lemma eqv_refl {T : Type} : reflexive (@eqv T). +Proof. by apply: equiv_refl. Qed. -Definition eudoxus := {eq_quot ~%E}. +Lemma eqv_sym {T : Type} : symmetric (@eqv T). +Proof. by apply: equiv_sym. Qed. -Canonical eudoxus_quotType := [quotType of eudoxus]. -Canonical eudoxus_eqType := [eqType of eudoxus]. -Canonical eudoxus_choiceType := [choiceType of eudoxus]. -Canonical eudoxus_eqQuotType := [eqQuotType ~%E of eudoxus]. +Lemma eqv_symL {T : Type} (f g : T -> int) : f ~ g -> g ~ f. +Proof. by rewrite eqv_sym. Qed. +Lemma eqv_trans {T : Type} : transitive (@eqv T). +Proof. by apply: equiv_trans. Qed. End QZEqv. -Local Notation "~%E" := qzeqv. -Local Notation "f ~ g" := (qzeqv f g). +Local Notation "~%E" := eqv. +Local Notation "f ~ g" := (eqv f g). (* -------------------------------------------------------------------- *) Definition edxoppf (f : qzEndo) : qzEndo := @@ -442,7 +470,7 @@ Canonical to_eudoxus_pi_morph := PiEmbed to_eudoxus. Lemma pi_edxopp : {morph \pi_eudoxus : f / edxoppf f >-> edxopp f}. Proof. move=> f; unlock edxopp; apply/eqmodP/qzeqvP; rewrite /edxoppf /=. -set g := repr _; have: f ~ g by apply/eqmodP; rewrite reprK. +set g := repr _; have: qzeqv f g by apply/eqmodP; rewrite reprK. by case/qzeqvP=> k hk; exists k => n; rewrite -opprD normrN. Qed. @@ -453,8 +481,8 @@ Lemma pi_edxadd : {morph \pi_eudoxus : f g / edxaddf f g >-> edxadd f g}. Proof. move=> f g; unlock edxadd; apply/eqmodP/qzeqvP; rewrite /edxaddf /=. set f' := repr (_ f); set g' := repr (_ g). -have: g ~ g' by apply/eqmodP; rewrite reprK. -have: f ~ f' by apply/eqmodP; rewrite reprK. +have: qzeqv g g' by apply/eqmodP; rewrite reprK. +have: qzeqv f f' by apply/eqmodP; rewrite reprK. move=> /qzeqvP[k1 h1] /qzeqvP[k2 h2]; exists (k1 + k2) => n. rewrite opprD addrACA (ler_lt_trans _ (ltr_add (h1 n) (h2 n))) //. by apply/ler_norm_add. @@ -468,9 +496,9 @@ Proof. move=> f g; unlock edxmul; apply/eqmodP => /=. set f' := repr (_ f); set g' := repr (_ g). apply/(@equiv_trans _ _ (edxmulf f' g)); apply/qzeqvP=> /=. -+ have: f ~ f' by apply/eqmodP; rewrite reprK. ++ have: qzeqv f f' by apply/eqmodP; rewrite reprK. by case/qzeqvP=> [k hk]; exists k. -have /qzeqvP[k hk]: g ~ g' by apply/eqmodP; rewrite reprK. +have /qzeqvP[k hk]: qzeqv g g' by apply/eqmodP; rewrite reprK. pose M : int := \sum_(0 <= j < `|k|) (`|f' j| + `|f' (- j%:Z)|). case/is_eqzendoPP: (valP f') => /= kf hkf; exists (kf + M) => n. rewrite -[X in `|X|](subrK (f' (g n - g' n))). @@ -501,13 +529,13 @@ Lemma edxzmod : & left_inverse (0%:R)%E edxopp edxadd]. Proof. split. + elim/quotW=> f; elim/quotW=> g; elim/quotW=> h /=. - rewrite !piE; apply/eqmodP/qzeqv_refl_eq => n /=. + rewrite !piE; apply/eqmodP/eqv_refl_eq => n /=. by rewrite addrA. + elim/quotW=> f; elim/quotW=> g; rewrite !piE. - by apply/eqmodP/qzeqv_refl_eq => n /=; rewrite addrC. -+ elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. + by apply/eqmodP/eqv_refl_eq => n /=; rewrite addrC. ++ elim/quotW=> f; rewrite !piE; apply/eqmodP/eqv_refl_eq. by move=> n /=; rewrite /qzendoC mulr0 add0r. -+ elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. ++ elim/quotW=> f; rewrite !piE; apply/eqmodP/eqv_refl_eq. by move=> n /=; rewrite addNr /qzendoC mulr0. Qed. @@ -535,7 +563,7 @@ Lemma edxcomring : & (1%:R)%E != 0 ]. Proof. split. + elim/quotW=> f; elim/quotW=> g; elim/quotW=> h. - by rewrite !piE /=; apply/eqmodP/qzeqv_refl_eq. + by rewrite !piE /=; apply/eqmodP/eqv_refl_eq. + elim/quotW=> f; elim/quotW=> g; rewrite !piE. case/is_eqzendoP: (valP f) => /= kf hf. case/is_eqzendoP: (valP g) => /= kg hg. @@ -578,10 +606,10 @@ Proof. split. rewrite [X in X + _ <= _]addrACA [X in _ + X <= _]addrACA. rewrite [X in X <= _]addrACA addrC [X in _ + X]addrACA. by rewrite [X in _ + X <= _]addrC -!addrA. -+ elim/quotW=> f; rewrite !piE; apply/eqmodP/qzeqv_refl_eq. ++ elim/quotW=> f; rewrite !piE; apply/eqmodP/eqv_refl_eq. by move=> n /=; rewrite /qzendoC mulr1. + elim/quotW=> f; elim/quotW=> g; elim/quotW=> h. - by rewrite !piE /=; apply/eqmodP/qzeqv_refl_eq. + by rewrite !piE /=; apply/eqmodP/eqv_refl_eq. + apply/eqP; rewrite !piE => /eqmodP/qzeqvP /= [k hk]. have := (hk 0); rewrite /qzendoC normr0 => /ltrW ge0k. move/(_ (k+1)): hk; rewrite /qzendoC !(mulr0, mulr1). @@ -604,7 +632,7 @@ Canonical comRingType := Eval hnf in ComRingType eudoxus edxmulC. Lemma edxnatrE n : n%:R = \pi_eudoxus (QZEndo (is_eqzendoC n)) :> eudoxus. Proof. rewrite !piE; elim: n => [|n ihn]; first by rewrite mulr0n !piE. -rewrite mulrS ihn !piE; apply/eqmodP/qzeqv_refl_eq => /=. +rewrite mulrS ihn !piE; apply/eqmodP/eqv_refl_eq => /=. by move=> k; rewrite /qzendoC /= -mulrDr intS. Qed. @@ -732,6 +760,24 @@ Lemma edxposfP (f : qzEndo) : (edxposf f). Proof. by apply/asboolP. Qed. +(* -------------------------------------------------------------------- *) +Lemma edxposfPE (f : qzEndo) : edxposf f -> + forall C : int, exists N : int, forall p : int, N < p -> C < f p. +Proof. (* See edxposf_spec *) +move=> /edxposfP gt0_f; case: (edxcmp0_spec (valP f)) => //=. ++ case=> C lt_fC; suff: C < C by rewrite ltrr. + move/(_ C): gt0_f => [n _ le_Cf]; rewrite (ltr_trans le_Cf) //. + by rewrite (ler_lt_trans (ler_norm _)). ++ move=> /(_ 0) [N]; rewrite oppr0 => h. + pose M : int := \sum_(0 <= i < `|N|.+1) `|f i|. + move/(_ M): gt0_f => [] [] // n _; rewrite ltrNge => /negP[]. + rewrite {}/M; case: (ltnP n `|N|.+1) => [lt_n_SN|]. + * rewrite (bigD1_seq n) 1?(iota_uniq, mem_iota) //=. + by rewrite ler_paddr 1?ler_norm //= sumr_ge0. + * rewrite -ltz_nat abszE => /(ler_lt_trans (ler_norm _)) /h. + by move/ltrW/ler_trans; apply; rewrite sumr_ge0. +Qed. + (* -------------------------------------------------------------------- *) Local Lemma pi_edxpos_r (f g : qzEndo) : f ~ g -> edxposf f -> edxposf g. Proof. @@ -749,7 +795,7 @@ Qed. Lemma pi_edxpos : {mono \pi_eudoxus : f / edxposf f >-> edxpos f}. Proof. move=> f; unlock edxpos; apply/idP/idP; apply: pi_edxpos_r; - by apply/eqmodP; rewrite reprK. + by rewrite -/(qzeqv _ _); apply/eqmodP; rewrite reprK. Qed. Canonical pi_edxpos_morph := PiMono1 pi_edxpos. @@ -771,7 +817,7 @@ Proof. split. + apply/orP; left; apply/edxposfP => /= k; case: (hf k). move=> N hN; exists (`|N| + 1); first by rewrite ltz_addr1. by rewrite hN // ltz_addr1 ler_norm. - by move/edxzero_spec; rewrite (negbTE h). + by move/edxzero_spec; rewrite -/(qzeqv _ _) (negbTE h). + elim/quotW=> f; elim/quotW=> g; rewrite !piE /=. move=> /edxposfP hf /edxposfP hg; apply/edxposfP => k. case/(edxposf_spec `|k| (valP _)): hf => /= kf hkf. @@ -794,12 +840,130 @@ End EudoxusPos. (* ==================================================================== *) Section EudoxusFieldType. +(* +Lemma eqvPd {T : Type} (f g : T -> int) : f ~ g <-> + exists C : int, forall n, exists2 a : int, + `|a| < C & g n = f n + a. +Proof. split. +* case/eqvP=> C bdC; exists C => n; exists (g n - f n) => //. + + by rewrite distrC. + by rewrite addrCA subrr addr0. +* case=> C bdC; apply/eqvP; exists C => n; case: (bdC n). + by move=> a lt_aC ->; rewrite opprD addrA subrr add0r normrN. +Qed. + +Lemma qzeqvDC (f : qzEndo) (c : int) : (f \o (fun x => x + c)) ~ f. +Proof. +case/is_eqzendoPP: (valP f) => /= C bdC; apply/eqvP; exists (C + `|f c|). +move=> k /=; move/(_ k c): bdC; rewrite -{1}(ltr_add2r `|f c| _ C). +by move/(ler_lt_trans (ler_norm_add _ _)); rewrite opprD -!addrA addNr addr0. +Qed. + +Lemma qzeqvD (f : qzEndo) : + (fun '(x, y) => f (x + y)) ~ (fun '(x, y) => f x + f y). +Proof. +by case/is_eqzendoPP: (valP f) => /= C bdC; apply/eqvP; exists C; case. +Qed. + +Lemma qzeqvN (f : qzEndo) : f \o [eta -%R] ~ - (val f). +Proof. +case/is_eqzendoPP: (valP f) => /= C bdC. +apply/eqvP; exists (C + `|f 0|) => x; rewrite opprK /=. +move/(_ x (-x)): bdC; rewrite subrr distrC -{1}(ltr_add2r `|f 0| _ C). +by move/(ler_lt_trans (ler_norm_add _ _)); rewrite -addrA addNr addr0 addrC. +Qed. + +Lemma L (f : qzEndo) : + (fun '(p, q, r) => f (r - p - q)) + ~ (fun '(p, q, r) => f r - f (p-1) - f (q-1)). +Proof. +apply/eqvPd => /=; evar (C : int); evar (a : int). +exists C; case=> [[p q] r]; exists a; last first. ++ rewrite -[r-p-q]addrA -opprD. + + case/eqv_symL/eqvPd: (qzeqvDC f (-1)) => /= Cp1 /(_ p)[ap1] ltp1 ->. + + case/eqv_symL/eqvPd: (qzeqvDC f (-1)) => /= Cq1 /(_ q)[aq1] ltq1 ->. + case/eqv_symL/eqvPd: (qzeqvD f) => CDr /= /(_ (r, -(p+q)))[aDr] ltDr ->. + rewrite -![LHS]addrA -![RHS]addrA; congr (f r + _). + case/eqv_symL/eqvPd: (qzeqvN f) => CN /= /(_ (p+q))[aN] ltN ->. + rewrite [in RHS]/GRing.opp /=. + case/eqv_symL/eqvPd: (qzeqvD f) => CD /= /(_ (p, q))[aD] ltD ->. + rewrite !opprD -![LHS]addrA -![RHS]addrA; congr (- f p + _). + rewrite addrC -![LHS]addrA; congr (-f q + _); apply/eqP. + rewrite [X in _==X]addrC -subr_eq [X in _==X]addrC -subr_eq. + rewrite [X in _==X]addrC -subr_eq; apply/eqP/esym. + rewrite -!opprD; set av := (X in _ = X). + + rewrite /a; reflexivity. + + +Lemma edxinv_r (x : qzEndo) : + edxposf x -> { y : eudoxus | y * \pi_eudoxus x = 1 }. +Proof. +move: x => f gt0_f; have h (p : nat) : exists n : nat, p%:Z <= f n. ++ by move/edxposfP: gt0_f => /(_ p) [] [|//] n _ /ltrW ?; exists n. +pose g p := (ex_minn (h p))%:Z. +have hC: exists C : int, forall n m, `|g (n + m)%N - g n - g m| <= C. ++ have [N gt0_g]: exists N, forall n, (N <= n)%N -> 0 < g n. + - exists `|f 0|.+1 => n lt_f0_n; rewrite /g; case: ex_minnP. + case=> //; rewrite lerNgt => /negP[]. + by rewrite (ler_lt_trans (ler_norm _)). + have hrg: forall r, (N <= r)%N -> f (g r - 1) < r%:Z <= f (g r). + - move=> r /gt0_g; rewrite /g; case: ex_minnP. + move=> m le_m_fr hmin gt0_m; rewrite le_m_fr andbT. + rewrite ltrNge; apply/negP; rewrite -predn_int //. + move/hmin; case: {le_m_fr hmin} m gt0_m => //=. + by move=> m _; rewrite ltnn. + have h1: forall m n, (N <= m)%N -> (N <= n)%N -> + 0 < f (g (m + n)%N) - f (g m - 1) - f (g n - 1). + - move=> m n le_Nm le_Nn; rewrite -[X in X<_](subrr (m%:Z + n%:Z)). + rewrite opprD !addrA ltr_sub //; last by case/andP: (hrg _ le_Nn). + rewrite ler_lt_sub //; last by case/andP: (hrg _ le_Nm). + suff: (N <= m + n)%N by move/hrg => /andP[]. + by apply: (leq_trans le_Nm); rewrite leq_addr. + have h2: forall m n, (N <= m)%N -> (N <= n)%N -> + f (g (m + n)%N - 1) - f (g m) - f (g n) < 0. + - move=> m n le_Nm le_Nn; rewrite -[X in _ /andP[]. + by apply: (leq_trans le_Nm); rewrite leq_addr. + + + + +Search _ (_ \is a eqzendo). +; last by case/andP: (hrg _ le_Nn). + + + +Search _ (_ <= _ + _)%N. + + + have := hrg (n + m)%N. + +rewrite -(rwP andP); split; last first. + * by rewrite /g; + + + - move/edxposfPE: (gt0_f) => /(_ (f 0))[n hn]; exists `|n|%N.+1. + move=> p; rewrite -ltz_nat abszE => /(ler_lt_trans (ler_norm _)). + move/hn => lt_f0_fp; rewrite /g; case: ex_minnP. + case=> //. + + + +eexists=> n le_Nn; rewrite /g; case: ex_minnP. + move=> m le_n_fm min. +*) + Parameter (edxinv : eudoxus -> eudoxus). Lemma edxfield : (forall x, x != 0 -> edxinv x * x = 1) /\ (edxinv 0 = 0). -Proof. Admitted. +Proof. +Admitted. Definition eudoxus_fieldUnitMixin := FieldUnitMixin edxfield.1 edxfield.2. From 9d20d85f8639c7ffdd900e0d55ab63edfa7b96d2 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 6 Nov 2020 19:03:19 +0100 Subject: [PATCH 12/13] --- theories/eudoxus.v | 298 +++++++++++++++++++++++++++++++++++---------- 1 file changed, 236 insertions(+), 62 deletions(-) diff --git a/theories/eudoxus.v b/theories/eudoxus.v index de7667674b..f81c70e661 100644 --- a/theories/eudoxus.v +++ b/theories/eudoxus.v @@ -359,6 +359,26 @@ apply: (ltr_trans _ gt_E_fN); rewrite mulr_natl mulr2n. by rewrite ltr_add2r /E ltr_addl. Qed. +Definition eqzlift (g : nat -> int) := + fun (x : int) => match x with Posz x => g x | Negz x => - (g x.+1) end. + +Lemma eqzendo_nat (g : nat -> int) : + (exists C : int, forall m n, `|g (m + n)%N - g m - g n| < C) + -> eqzlift g \is a eqzendo. +Proof. +case=> C hC; apply/is_eqzendoP; exists C; apply/is_qzendoP=> m n. +wlog: m n / (m <= n) => [wlog|]; first case: (lerP m n) => [|/ltrW] /wlog //. ++ by rewrite [n+m]addrC [X in _-X]addrC. +case: m n => [m|m] [n|n] //= _. ++ by rewrite opprD addrA; apply: hC. ++ rewrite [Negz m + n]/GRing.add /=; case: ltnP => /=. + * move=> lt_mn; rewrite distrC addrAC addrC addrA. + by rewrite -{1}[n](subnKC lt_mn); apply: hC. + * move=> le_nm; rewrite -subSn // opprD opprK addrCA addrA. + by rewrite -{1}[m.+1](@subnK n) 1?ltnW. ++ by rewrite -opprD normrN addrA -addSn -addnS; apply: hC. +Qed. + End EQzEndoTheory. (* ==================================================================== *) @@ -851,6 +871,8 @@ Proof. split. by move=> a lt_aC ->; rewrite opprD addrA subrr add0r normrN. Qed. + +*) Lemma qzeqvDC (f : qzEndo) (c : int) : (f \o (fun x => x + c)) ~ f. Proof. case/is_eqzendoPP: (valP f) => /= C bdC; apply/eqvP; exists (C + `|f c|). @@ -858,12 +880,7 @@ move=> k /=; move/(_ k c): bdC; rewrite -{1}(ltr_add2r `|f c| _ C). by move/(ler_lt_trans (ler_norm_add _ _)); rewrite opprD -!addrA addNr addr0. Qed. -Lemma qzeqvD (f : qzEndo) : - (fun '(x, y) => f (x + y)) ~ (fun '(x, y) => f x + f y). -Proof. -by case/is_eqzendoPP: (valP f) => /= C bdC; apply/eqvP; exists C; case. -Qed. - +(* Lemma qzeqvN (f : qzEndo) : f \o [eta -%R] ~ - (val f). Proof. case/is_eqzendoPP: (valP f) => /= C bdC. @@ -871,45 +888,199 @@ apply/eqvP; exists (C + `|f 0|) => x; rewrite opprK /=. move/(_ x (-x)): bdC; rewrite subrr distrC -{1}(ltr_add2r `|f 0| _ C). by move/(ler_lt_trans (ler_norm_add _ _)); rewrite -addrA addNr addr0 addrC. Qed. +*) -Lemma L (f : qzEndo) : - (fun '(p, q, r) => f (r - p - q)) - ~ (fun '(p, q, r) => f r - f (p-1) - f (q-1)). +Lemma qzeqvD {T : Type} (El Er : T -> int) (f : qzEndo) : + (fun x => f (El x + Er x)) ~ (fun x => f (El x) + f (Er x)). Proof. -apply/eqvPd => /=; evar (C : int); evar (a : int). -exists C; case=> [[p q] r]; exists a; last first. -+ rewrite -[r-p-q]addrA -opprD. - - case/eqv_symL/eqvPd: (qzeqvDC f (-1)) => /= Cp1 /(_ p)[ap1] ltp1 ->. - - case/eqv_symL/eqvPd: (qzeqvDC f (-1)) => /= Cq1 /(_ q)[aq1] ltq1 ->. - case/eqv_symL/eqvPd: (qzeqvD f) => CDr /= /(_ (r, -(p+q)))[aDr] ltDr ->. - rewrite -![LHS]addrA -![RHS]addrA; congr (f r + _). - case/eqv_symL/eqvPd: (qzeqvN f) => CN /= /(_ (p+q))[aN] ltN ->. - rewrite [in RHS]/GRing.opp /=. - case/eqv_symL/eqvPd: (qzeqvD f) => CD /= /(_ (p, q))[aD] ltD ->. - rewrite !opprD -![LHS]addrA -![RHS]addrA; congr (- f p + _). - rewrite addrC -![LHS]addrA; congr (-f q + _); apply/eqP. - rewrite [X in _==X]addrC -subr_eq [X in _==X]addrC -subr_eq. - rewrite [X in _==X]addrC -subr_eq; apply/eqP/esym. - rewrite -!opprD; set av := (X in _ = X). - - rewrite /a; reflexivity. - +case/is_eqzendoPP: (valP f) => /= C bdC. +by apply/eqvP; exists C => n; apply: bdC. +Qed. + +Lemma qzeqvN {T : Type} (E : T -> int) (f : qzEndo) : + (fun x => f (- (E x))) ~ (fun x => - (f (E x))). +Proof. Admitted. + +Lemma qzeqvD_split {T : Type} (f1 f2 g1 g2 : T -> int) : + f1 ~ g1 -> f2 ~ g2 -> f1 \+ f2 ~ g1 \+ g2. +Proof. Admitted. + +Lemma qzeqvN_split {T : Type} (f g : T -> int) : + f ~ g -> \- f ~ \- g. +Proof. Admitted. + +Lemma eqv_eq {T : Type} (g f : T -> int) : f =1 g -> f ~ g. +Proof. by move=> /funext ->. Qed. + +Let D := (int * (int * int))%type. + +Lemma L1 (f : qzEndo) : + (fun x : D => f (x.1 - x.2.1 - x.2.2)) + ~ (fun x : D => f x.1 - f (x.2.1-1) - f (x.2.2-1)). +Proof. +apply: (@eqv_trans _ (fun x : D => f (x.1 - (x.2.1 + x.2.2)))). ++ by apply: eqv_eq => /= -[r [p q]] /=; rewrite opprD addrA. +apply: (eqv_trans (qzeqvD _ _ f)); rewrite eqv_sym. +apply: (@eqv_trans _ (fun x : D => f x.1 - (f (x.2.1-1) + f (x.2.2-1)))). ++ by apply: eqv_eq=> /= -[r [p q]] /=; rewrite opprD addrA. +apply/qzeqvD_split=> //; rewrite eqv_sym. +apply/(eqv_trans (qzeqvN _ f))/qzeqvN_split. +apply/(eqv_trans (qzeqvD _ _ f))/qzeqvD_split. ++ rewrite eqv_sym. +Admitted. + +Lemma L2 (f : qzEndo) : + (fun x : D => f (x.1 - x.2.1 - x.2.2)) + ~ (fun x : D => f (x.1-1) - f x.2.1 - f x.2.2). +Proof. Admitted. + +Lemma eqv_eqzendo f g : + f ~ g -> f \is a eqzendo -> g \is a eqzendo. +Proof. +move/eqvP=> [C hC] /is_eqzendoP[C' /is_qzendoP hC']. +apply/is_eqzendoP; exists (C *+ 3 + C'); apply/is_qzendoP=> m n. +apply: (ler_lt_trans (@ler_dist_add _ (f (m + n)) _ _)). +rewrite mulrS -addrA ltr_add //; first by rewrite distrC hC. +apply: (ler_lt_trans (@ler_dist_add _ (f m + f n) _ _)). +rewrite [X in _ < X]addrC ltr_add // opprD addrACA. +by apply: (ler_lt_trans (ler_norm_add _ _)); rewrite ltr_add. +Qed. Lemma edxinv_r (x : qzEndo) : edxposf x -> { y : eudoxus | y * \pi_eudoxus x = 1 }. Proof. -move: x => f gt0_f; have h (p : nat) : exists n : nat, p%:Z <= f n. -+ by move/edxposfP: gt0_f => /(_ p) [] [|//] n _ /ltrW ?; exists n. +move: x => f; wlog: f / forall n : nat, f (Negz n) = - (f n.+1) => [wlog gt0_f|]. + pose g := eqzlift (fun n => f n%:Z); have eq_fg: f ~ g. + have /= := qzeqvN idfun f => /eqvP[C hC]. + apply/eqvP; exists `|C|.+1; case=> n /=. + by rewrite subrr normr0. + have /= := hC n.+1%:Z; rewrite NegzE => /ltr_trans; apply. + by apply: (ler_lt_trans (ler_norm _)); rewrite ltz_nat. + pose gh := QZEndo (eqv_eqzendo eq_fg (valP f)); case: (wlog gh) => //. + by apply: (@pi_edxpos_r _ gh eq_fg gt0_f). + move=> gI hV; exists gI; rewrite -[RHS]hV. + by congr (_ * _); apply/eqmodP. +move=> fNE gt0_f; have h (p : nat) : exists n : nat, p%:Z <= f n. + by move/edxposfP: gt0_f => /(_ p) [] [|//] n _ /ltrW ?; exists n. pose g p := (ex_minn (h p))%:Z. +have [N gt0_g]: { N | forall n, (N <= n)%N -> 0 < g n}. + exists `|f 0|.+1 => n lt_f0_n; rewrite /g; case: ex_minnP. + case=> //; rewrite lerNgt => /negP[]. + by rewrite (ler_lt_trans (ler_norm _)). +have comp_fg : forall n : nat, f (g n) >= n%:Z. + by move=> n; rewrite /g; case: ex_minnP. +have hrg: forall r, (N <= r)%N -> f (g r - 1) < r%:Z <= f (g r). + move=> r /gt0_g; rewrite /g; case: ex_minnP. + move=> m le_m_fr hmin gt0_m; rewrite le_m_fr andbT. + rewrite ltrNge; apply/negP; rewrite -predn_int //. + move/hmin; case: {le_m_fr hmin} m gt0_m => //=. + by move=> m _; rewrite ltnn. +have h1: forall m n, (N <= m)%N -> (N <= n)%N -> + 0 < f (g (m + n)%N) - f (g m - 1) - f (g n - 1). + move=> m n le_Nm le_Nn; rewrite -[X in X<_](subrr (m%:Z + n%:Z)). + rewrite opprD !addrA ltr_sub //; last by case/andP: (hrg _ le_Nn). + rewrite ler_lt_sub //; last by case/andP: (hrg _ le_Nm). + suff: (N <= m + n)%N by move/hrg => /andP[]. + by apply: (leq_trans le_Nm); rewrite leq_addr. +have h2: forall m n, (N <= m)%N -> (N <= n)%N -> + f (g (m + n)%N - 1) - f (g m) - f (g n) < 0. + move=> m n le_Nm le_Nn; rewrite -[X in _ /andP[]. + by apply: (leq_trans le_Nm); rewrite leq_addr. +suff hg: eqzlift (fun p => g (N + p)%N) \is a eqzendo. + exists (\pi_eudoxus (QZEndo hg)). + rewrite mulrC !piE; apply/eqmodP/qzeqvP=> /=. + suff [C hC]: exists C : int, forall n, (N <= n)%N -> `|f (g n) - n%:Z| < C. + have bdnat n: `|f (g (N + n)%N) - n%:Z| < C + N. + rewrite -[X in `|X|](@subrK _ N%:Z). + apply: (ler_lt_trans (ler_norm_add _ _)); rewrite ltr_le_add //. + by rewrite -addrA -opprD [(N+_)%N]addnC hC // leq_addl. + exists (C + N%:Z) => n; rewrite /qzendoC mulr1; case: n => //= n. + set x := (X in g X); rewrite NegzE (_ : f (- (g x)) = -(f (g x))). + have := (gt0_g x (leq_addr _ _)); case: (g x) => //. + by case=> // p _; rewrite -NegzE fNE. + by rewrite -opprD normrN {}/x. + have /eqvP[/= C hC] := qzeqvDC f (-1); exists `|C|.+1. + move=> n le_Nn; rewrite ltr_norml (@ltr_le_trans _ 0) /=. + - by rewrite oppr_lt0. + - by rewrite subr_ge0; have /andP[] := hrg _ le_Nn. + rewrite (@ler_lt_trans _ `|C|) //; last by rewrite ltz_nat ltnS. + apply: (@ler_trans _ (f (g n) - f (g n - 1))). + by rewrite ler_sub //; have /andP[/ltrW] := hrg _ le_Nn. + have /ltrW := hC (g n); rewrite distrC ler_norml => /andP[_]. + by move/ler_trans; apply; rewrite ler_norm. +set gh := fun p => g (N + p)%N; apply: eqzendo_nat. +have [C hC]: exists C : int, forall (m n : nat), + `|f (gh (n + m)%N - gh n - gh m)| < C. + suff [C hC]: exists C : int, forall (m n : nat), + (N <= m)%N -> (N <= n)%N -> `|f (g (n + m)%N - g n - g m)| < C. + exists C. + + + have bd1: exists C : int, forall (m n : nat), + (N <= m)%N -> (N <= n)%N -> f (g (n + m)%N - g n - g m) > C. + have /eqvP[C hC] := L1 f; exists (-C) => m n le_Mm le_Mn. + move/(_ (g (n + m)%N, (g n, g m))): hC => /=; rewrite ltr_norml. + case/andP=> [+ _] => /ltr_trans; apply; rewrite ltr_subl_addr. + by rewrite ltr_spaddr //; apply: h1. + + have bd2: exists C : int, forall (m n : nat), + (N <= m)%N -> (N <= n)%N -> f (g (n + m)%N - g n - g m) < C. + have /eqvP[C hC] := L2 f; exists C => m n le_Mm le_Mn. + move/(_ (g (n + m)%N, (g n, g m))): hC => /=; rewrite ltr_norml. + case/andP=> _ /(ltr_trans _); apply; rewrite ltr_subr_addr. + by rewrite ltr_snaddr //; apply: h2. + case: bd1 bd2 => {h1 h2} [C1 h1] [C2 h2]; pose C := Num.max `|C1| `|C2|. + exists C; move=> m n le_Mm le_Mn; rewrite ltr_norml. + rewrite andbC ltr_maxr orbC ltr_normr h2 //= ltr_oppl. + by rewrite ltr_maxr ltr_normr ltr_opp2 h1 ?Monoid.simpm. + + + +case/boolP: [exists p : 'I_N, g p <= 0]; last first. + move/existsPn=> /= gt0_g_le; exists 0%N => n. + rewrite leq0n; apply/esym; case: (leqP N n) => [/gt0_g//|lt_nN]. + by move/(_ (Ordinal lt_nN)): gt0_g_le; rewrite -ltrNge. +move=> ge0_g; have {}ge0_g: exists p, g p <= 0. +* by case/existsP: ge0_g=> /= x ge0_gx; exists (val x). +have bdN p: g p <= 0 -> (p <= N)%N. +* by apply: contraLR; rewrite -ltrNge -ltnNge => /ltnW /gt0_g. +exists (ex_maxn ge0_g bdN).+1 => n; case: ex_maxnP => m. +move=> le0_gm hmax; apply/idP/idP. +* move=> lt_mn; rewrite ltrNge; apply/negP. + by move/hmax; rewrite leqNgt lt_mn. +* move/(ler_lt_trans le0_gm); apply: contraLR. + by rewrite -lerNgt -ltnNge ltnS; apply: homo_g. + + + +have homo_g: forall x y, (x <= y)%N -> (g x <= g y). ++ move=> x y le_xy; rewrite /g. + case: ex_minnP=> m le_fm hm; case: ex_minnP=> n le_fn hn. + by apply/hm/(ler_trans _ le_fn); rewrite lez_nat. have hC: exists C : int, forall n m, `|g (n + m)%N - g n - g m| <= C. -+ have [N gt0_g]: exists N, forall n, (N <= n)%N -> 0 < g n. - - exists `|f 0|.+1 => n lt_f0_n; rewrite /g; case: ex_minnP. - case=> //; rewrite lerNgt => /negP[]. - by rewrite (ler_lt_trans (ler_norm _)). ++ have [N gt0_g]: exists N, forall n, (N <= n)%N = (0 < g n). + - have [N gt0_g]: exists N, forall n, (N <= n)%N -> 0 < g n. + exists `|f 0|.+1 => n lt_f0_n; rewrite /g; case: ex_minnP. + case=> //; rewrite lerNgt => /negP[]. + by rewrite (ler_lt_trans (ler_norm _)). + case/boolP: [exists p : 'I_N, g p <= 0]; last first. + move/existsPn=> /= gt0_g_le; exists 0%N => n. + rewrite leq0n; apply/esym; case: (leqP N n) => [/gt0_g//|lt_nN]. + by move/(_ (Ordinal lt_nN)): gt0_g_le; rewrite -ltrNge. + move=> ge0_g; have {}ge0_g: exists p, g p <= 0. + * by case/existsP: ge0_g=> /= x ge0_gx; exists (val x). + have bdN p: g p <= 0 -> (p <= N)%N. + * by apply: contraLR; rewrite -ltrNge -ltnNge => /ltnW /gt0_g. + exists (ex_maxn ge0_g bdN).+1 => n; case: ex_maxnP => m. + move=> le0_gm hmax; apply/idP/idP. + * move=> lt_mn; rewrite ltrNge; apply/negP. + by move/hmax; rewrite leqNgt lt_mn. + * move/(ler_lt_trans le0_gm); apply: contraLR. + by rewrite -lerNgt -ltnNge ltnS; apply: homo_g. + have eq0_g n: (n < N)%N = (g n == 0). + + by rewrite ltnNge gt0_g -lerNgt lez_nat leqn0. have hrg: forall r, (N <= r)%N -> f (g r - 1) < r%:Z <= f (g r). - - move=> r /gt0_g; rewrite /g; case: ex_minnP. + - move=> r; rewrite gt0_g /g; case: ex_minnP. move=> m le_m_fr hmin gt0_m; rewrite le_m_fr andbT. rewrite ltrNge; apply/negP; rewrite -predn_int //. move/hmin; case: {le_m_fr hmin} m gt0_m => //=. @@ -928,35 +1099,38 @@ have hC: exists C : int, forall n m, `|g (n + m)%N - g n - g m| <= C. rewrite ltr_le_sub //; last by case/andP: (hrg _ le_Nm). suff: (N <= m + n)%N by move/hrg => /andP[]. by apply: (leq_trans le_Nm); rewrite leq_addr. - - - - -Search _ (_ \is a eqzendo). -; last by case/andP: (hrg _ le_Nn). + - have [C hC]: exists C : int, forall (m n : nat), + `|f (g (n + m)%N - g n - g m)| < C. + * have [C hC]: exists C : int, forall (m n : nat), + (N <= m)%N -> (N <= n)%N -> `|f (g (n + m)%N - g n - g m)| < C. + + have bd1: exists C : int, forall (m n : nat), + (N <= m)%N -> (N <= n)%N -> f (g (n + m)%N - g n - g m) > C. + have /eqvP[C hC] := L1 f; exists (-C) => m n le_Mm le_Mn. + move/(_ (g (n + m)%N, (g n, g m))): hC => /=; rewrite ltr_norml. + case/andP=> [+ _] => /ltr_trans; apply; rewrite ltr_subl_addr. + by rewrite ltr_spaddr //; apply: h1. + + have bd2: exists C : int, forall (m n : nat), + (N <= m)%N -> (N <= n)%N -> f (g (n + m)%N - g n - g m) < C. + have /eqvP[C hC] := L2 f; exists C => m n le_Mm le_Mn. + move/(_ (g (n + m)%N, (g n, g m))): hC => /=; rewrite ltr_norml. + case/andP=> _ /(ltr_trans _); apply; rewrite ltr_subr_addr. + by rewrite ltr_snaddr //; apply: h2. + case: bd1 bd2 => {h1 h2} [C1 h1] [C2 h2]; pose C := Num.max `|C1| `|C2|. + exists C; move=> m n le_Mm le_Mn; rewrite ltr_norml. + rewrite andbC ltr_maxr orbC ltr_normr h2 //= ltr_oppl. + by rewrite ltr_maxr ltr_normr ltr_opp2 h1 ?Monoid.simpm. + pose F i j : int := `|f (g (i + j)%N - g i - g j)|. + pose C' : int := \sum_(0 <= i < N) g i; exists (`|C| + `|C'|). + move=> m n; wlog: m n / (m <= n)%N => [wlog|le_mn]. + * case: (leqP m n) => [|/ltnW] /wlog //. + by rewrite addnC addrAC. + case: (ltnP m N) => [|le_Nm]; last first. + * have le_Nn := leq_trans le_Nm le_mn. + by rewrite ltr_paddr ?normr_ge0 // ltr_normr hC. + rewrite eq0_g => /eqP->; rewrite subr0. -Search _ (_ <= _ + _)%N. - - - have := hrg (n + m)%N. - -rewrite -(rwP andP); split; last first. - * by rewrite /g; - - - - move/edxposfPE: (gt0_f) => /(_ (f 0))[n hn]; exists `|n|%N.+1. - move=> p; rewrite -ltz_nat abszE => /(ler_lt_trans (ler_norm _)). - move/hn => lt_f0_fp; rewrite /g; case: ex_minnP. - case=> //. - - - -eexists=> n le_Nn; rewrite /g; case: ex_minnP. - move=> m le_n_fm min. -*) - Parameter (edxinv : eudoxus -> eudoxus). Lemma edxfield : From de2a47b4511b11d90c00706ec6e022c337bc7eb7 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 6 Nov 2020 20:33:36 +0100 Subject: [PATCH 13/13] make things compiling again --- theories/eudoxus.v | 239 ++++++++++++++++++++++++--------------------- 1 file changed, 127 insertions(+), 112 deletions(-) diff --git a/theories/eudoxus.v b/theories/eudoxus.v index f81c70e661..022498ce60 100644 --- a/theories/eudoxus.v +++ b/theories/eudoxus.v @@ -11,6 +11,7 @@ Unset Printing Implicit Defensive. Unset SsrOldRewriteGoalsOrder. Import GRing.Theory Num.Def Num.Theory. +Import Order.POrderTheory Order.TotalTheory. Local Open Scope ring_scope. Local Open Scope int_scope. @@ -53,12 +54,15 @@ Qed. Local Lemma sub_ge0 x y : le 0 (y - x) = le x y. Proof. by rewrite /le /lt subr0 [0==_]eq_sym subr_eq0 eq_sym. Qed. -Local Lemma le_total x : le 0 x || le x 0. +Local Lemma cmp0_total x : le 0 x || le x 0. Proof. rewrite /le /lt [0==_]eq_sym orbCA !orbA orbb subr0 sub0r. by case: eqP => //= /eqP /p_total. Qed. +Local Lemma le_total x y : le x y || le y x. +Proof. Admitted. + Local Lemma normN x : norm (- x) = norm x. Proof. have h v : v != 0 -> (v \in p) = (-v \notin p). @@ -83,7 +87,7 @@ by rewrite subrr (negbTE p_N0). Qed. Definition PosNumMixin := - RealLeMixin le0D le0M le_anti sub_ge0 le_total normN ge0_norm lt_def. + RealLeMixin le0D le0M le_anti sub_ge0 cmp0_total normN ge0_norm lt_def. End PosNumMixin. (* -------------------------------------------------------------------- *) @@ -140,10 +144,10 @@ Lemma is_qzendoP k f : Proof. by apply/asboolP. Qed. Lemma is_qzendo_gt0 k f : f \is a k.-qzendo -> 0 < k. -Proof. by move/is_qzendoP => /(_ 0 0) /(ler_lt_trans _); apply. Qed. +Proof. by move/is_qzendoP => /(_ 0 0) /(le_lt_trans _); apply. Qed. Lemma is_qzendo_ge0 k f : f \is a k.-qzendo -> 0 <= k. -Proof. by move=> h; apply/ltrW/(is_qzendo_gt0 h). Qed. +Proof. by move=> h; apply/ltW/(is_qzendo_gt0 h). Qed. Lemma qzendoC_is_additive z : additive (qzendoC z). Proof. by move=> n m; rewrite /qzendoC; rewrite -mulrBl. Qed. @@ -167,7 +171,7 @@ Lemma is_qzendoD kf kg f g : Proof. move=> /is_qzendoP bdf /is_qzendoP bdg. apply/is_qzendoP => n m; rewrite addrACA opprD addrACA. -by apply/(ler_lt_trans (ler_norm_add _ _))/ltr_add. +by apply/(le_lt_trans (ler_norm_add _ _))/ltr_add. Qed. Lemma is_qzendoN k f : f \is a k.-qzendo -> \- f \is a k.-qzendo. @@ -185,14 +189,14 @@ move/is_qzendoP=> bdf; move/is_qzendoP=> bdg. pose M : int := \sum_(0 <= i < `|kg|) (`|f i| + `|f (- i%:Z)|). exists (M + kf *+ 2); apply/is_qzendoP => m n /=. rewrite -[X in `|X - _|](subrK (f (g m + g n))). -rewrite -[X in `|X|]addrA (ler_lt_trans (ler_norm_add _ _)) //. +rewrite -[X in `|X|]addrA (le_lt_trans (ler_norm_add _ _)) //. rewrite mulr2n addrA ltr_add //. rewrite -[X in `|X|](subrK (f (g (m + n) - (g m + g n)))). -rewrite [X in _ < X]addrC (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. +rewrite [X in _ < X]addrC (le_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. + by rewrite addrAC -{1}[g (m + n)](subrK (g m + g n)) -addrA -opprD. rewrite {}/M; set k := g _ - _; rewrite (bigD1_seq `|k|%N) /=. + rewrite mem_index_iota /k /= -ltz_nat !abszE. - by apply/(ltr_le_trans (bdg _ _))/ler_norm. + by apply/(lt_le_trans (bdg _ _))/ler_norm. + by apply/iota_uniq. rewrite !abszE ler_paddr ?sumr_ge0 //; case: (ger0P k) => _. + by apply/ler_addl. @@ -232,15 +236,15 @@ move=> hf m n; elim/int_rec: m => [|m|m]. * rewrite -![`|_%:Z|]abszE !absz_nat => ihm. rewrite [in X in _ < X]intS -addrA mulrDl mul1r. have /is_qzendoP/(_ n (m%:Z * n)) lek := hf. - apply/(ler_lt_trans _ (ltr_add lek ihm)). - apply/(ler_trans _ (ler_norm_add _ _)). + apply/(le_lt_trans _ (ltr_add lek ihm)). + apply/(le_trans _ (ler_norm_add _ _)). rewrite opprD addrA addrACA !addrA addrK. by rewrite intS !mulrDl !mul1r -addrA -opprD. * rewrite !normrN -![`|_%:Z|]abszE !absz_nat !mulNr !opprK. move=> ihm; rewrite [in X in _ < X]intS mulrDl mul1r [1+_]addrC. have /is_qzendoP/(_ n (- (m.+1%:Z * n))) lek := hf. - apply/(ler_lt_trans _ (ltr_add ihm lek)). - apply/(ler_trans _ (ler_norm_sub _ _)). + apply/(le_lt_trans _ (ltr_add ihm lek)). + apply/(le_trans _ (ler_norm_sub _ _)). rewrite !opprD !opprK !addrA [X in `|X + _ + _|]addrAC. rewrite [X in n - X * n]intS mulrDl mul1r. rewrite opprD addrA subrr add0r subrr add0r. @@ -254,8 +258,8 @@ Proof. move=> hf m n; rewrite (natrD _ 1 1) addrACA mulrDl. have hL := qzendo_crossbdL hf m n. have hR := qzendo_crossbdL hf n m. -apply/(ler_lt_trans _ (ltr_add hL hR)). -apply/(ler_trans _ (ler_norm_sub _ _)). +apply/(le_lt_trans _ (ltr_add hL hR)). +apply/(le_trans _ (ler_norm_sub _ _)). rewrite opprB [n * m]mulrC [in X in _ <= X]addrC. by rewrite !addrA subrK distrC. Qed. @@ -269,8 +273,8 @@ have := qzendo_crossbd hf m 1; rewrite mul1r normr1 distrC. rewrite -addrA -(natrD _ 1 2) -[(1+2)%N]/3 => h. rewrite mulrDl addrAC [k*_]mulrC -mulrDl. set M : int := `|f 1| * _; move: h; rewrite -(ltr_add2r M). -move/(ler_lt_trans _); apply; rewrite {}/M. -rewrite -normrM (ler_trans _ (ler_norm_add _ _)) //. +move/(le_lt_trans _); apply; rewrite {}/M. +rewrite -normrM (le_trans _ (ler_norm_add _ _)) //. by rewrite [f 1 * _]mulrC subrK. Qed. @@ -344,18 +348,18 @@ Lemma eqzendo_suplin f (D : int) : Proof. move=> ge0_D edf infp; case/is_eqzendoPP: edf => C edfC. pose E : int := C + D; case: (infp (2%:R * E)) => N gt0_n gt_E_fN. -exists N => //; case=> // k gt0_k; apply/(@ltr_trans _ ((k%:Z + 1) * E)). +exists N => //; case=> // k gt0_k; apply/(@lt_trans _ _ ((k%:Z + 1) * E)). + rewrite ltr_pmul2l; first by rewrite addrC ltz_add1r. - by rewrite ltr_addr (ler_lt_trans _ (edfC 0 0)). + by rewrite ltr_addr (le_lt_trans _ (edfC 0 0)). case: k gt0_k => // k _; rewrite [_+1]addrC -intS. elim: k => [|k ihk]; first by rewrite mul1r. move: k.+1 ihk => {k} k ihk; have := edfC (k%:Z * N) N. rewrite ltr_norml => /andP[h _]; move: h. rewrite ltr_subr_addl (_ : k%:Z * N + N = (k.+1)%:Z * N). + by rewrite intS mulrDl mul1r addrC. -move/(ltr_trans _); apply; rewrite intS mulrDl mul1r addrC -addrA. +move/(lt_trans _); apply; rewrite intS mulrDl mul1r addrC -addrA. apply: ltr_add => //; rewrite ltr_subr_addl. -apply: (ltr_trans _ gt_E_fN); rewrite mulr_natl mulr2n. +apply: (lt_trans _ gt_E_fN); rewrite mulr_natl mulr2n. by rewrite ltr_add2r /E ltr_addl. Qed. @@ -367,7 +371,7 @@ Lemma eqzendo_nat (g : nat -> int) : -> eqzlift g \is a eqzendo. Proof. case=> C hC; apply/is_eqzendoP; exists C; apply/is_qzendoP=> m n. -wlog: m n / (m <= n) => [wlog|]; first case: (lerP m n) => [|/ltrW] /wlog //. +wlog: m n / (m <= n) => [wlog|]; first case: (lerP m n) => [|/ltW] /wlog //. + by rewrite [n+m]addrC [X in _-X]addrC. case: m n => [m|m] [n|n] //= _. + by rewrite opprD addrA; apply: hC. @@ -422,8 +426,8 @@ Proof. split. by case/eqvP => [k hk]; apply/eqvP; exists k=> n; rewrite distrC. + move=> f g h /eqvP[k1 h1] /eqvP[k2 h2]. apply/eqvP; exists (k1 + k2) => n. - apply/(ler_lt_trans _ (ltr_add (h1 n) (h2 n))). - apply/(ler_trans _ (ler_norm_add _ _)). + apply/(le_lt_trans _ (ltr_add (h1 n) (h2 n))). + apply/(le_trans _ (ler_norm_add _ _)). by rewrite [f n - _]addrC addrACA addNr addr0. Qed. @@ -504,7 +508,7 @@ set f' := repr (_ f); set g' := repr (_ g). have: qzeqv g g' by apply/eqmodP; rewrite reprK. have: qzeqv f f' by apply/eqmodP; rewrite reprK. move=> /qzeqvP[k1 h1] /qzeqvP[k2 h2]; exists (k1 + k2) => n. -rewrite opprD addrACA (ler_lt_trans _ (ltr_add (h1 n) (h2 n))) //. +rewrite opprD addrACA (le_lt_trans _ (ltr_add (h1 n) (h2 n))) //. by apply/ler_norm_add. Qed. @@ -522,11 +526,11 @@ have /qzeqvP[k hk]: qzeqv g g' by apply/eqmodP; rewrite reprK. pose M : int := \sum_(0 <= j < `|k|) (`|f' j| + `|f' (- j%:Z)|). case/is_eqzendoPP: (valP f') => /= kf hkf; exists (kf + M) => n. rewrite -[X in `|X|](subrK (f' (g n - g' n))). -rewrite (ler_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. +rewrite (le_lt_trans (ler_norm_add _ _)) ?ltr_le_add //. + by rewrite addrAC -addrA -opprD -{1}[g n](subrK (g' n)). rewrite {}/M (bigD1_seq `|g n - g' n|%N) /=. + rewrite mem_index_iota /= -ltz_nat abszE. - by apply/(ltr_le_trans (hk _))/ler_norm. + by apply/(lt_le_trans (hk _))/ler_norm. + by apply/iota_uniq. rewrite ler_paddr ?sumr_ge0 // !abszE; case: (ger0P (g n - g' n)) => _. + by rewrite ler_addl. @@ -592,35 +596,35 @@ Proof. split. pose M := (6%:R + (Af + Bf) + (Ag + Bg)) * maxr kf kg. apply/eqmodP/qzeqvP; exists (maxr M (1 + `|f (g 0) - g (f 0)|)). move=> n; case: (n =P 0) => /= [->|/eqP nz_n]. - * by rewrite ltr_maxr ltz_add1r lerr orbT. - rewrite ltr_maxr; apply/orP; left; rewrite {}/M. + * by rewrite lt_maxr ltz_add1r lexx orbT. + rewrite lt_maxr; apply/orP; left; rewrite {}/M. rewrite -(@ltr_pmul2l _ `|n|) ?normr_gt0 //. have /= h1 := qzendo_crossbd hf n (g n). have /= h2 := qzendo_crossbd hg (f n) n. - have {h1 h2} /(ler_lt_trans (ler_norm_add _ _)) := ltr_add h1 h2. + have {h1 h2} /(le_lt_trans (ler_norm_add _ _)) := ltr_add h1 h2. rewrite [g n * _]mulrC ![in X in X < _]addrA subrK -mulrBr normrM. - move/ltr_le_trans; apply; set M := maxr _ _. + move/lt_le_trans; apply; set M := maxr _ _. set x1 := (X in X * _ + _); set x2 := (X in _ + X * _). have h1: x1 * kf <= (`|n| * (Ag + 1) + (Bg + 2%:R)) * M. * apply/ler_pmul; rewrite ?addr_ge0 ?(is_qzendo_ge0 hf) //; last first. - - by rewrite /M ler_maxr lerr orTb. + - by rewrite /M le_maxr lexx orTb. rewrite {}/x1 !addrA !ler_add2r mulrDr mulr1. - by rewrite addrAC [X in X<=_]addrC ler_add2r mulrC 1?ltrW. + by rewrite addrAC [X in X<=_]addrC ler_add2r mulrC 1?ltW. have h2: x2 * kg <= (`|n| * (Af + 1) + (Bf + 2%:R)) * M. * apply/ler_pmul; rewrite ?addr_ge0 ?(is_qzendo_ge0 hg) //; last first. - - by rewrite /M ler_maxr lerr orbT. + - by rewrite /M le_maxr lexx orbT. rewrite {}/x2 !addrA !ler_add2r mulrDr mulr1. - by rewrite addrAC ler_add2r mulrC 1?ltrW. - apply/(ler_trans (ler_add h1 h2)); rewrite -mulrDl mulrA. - apply/ler_wpmul2r; first by rewrite ler_maxr (is_qzendo_ge0 hf). + by rewrite addrAC ler_add2r mulrC 1?ltW. + apply/(le_trans (ler_add h1 h2)); rewrite -mulrDl mulrA. + apply/ler_wpmul2r; first by rewrite le_maxr (is_qzendo_ge0 hf). rewrite addrACA -mulrDr => {M h1 h2 x1 x2}. set M := (X in _ + X <= _); set N := (X in `|n| * X). - apply/(@ler_trans _ (`|n| * (N + M))). + apply/(@le_trans _ _ (`|n| * (N + M))). * rewrite mulrDr ler_add2l ler_pemull // ?addr_ge0 //. - move/(_ 0): subg; rewrite normr0 mulr0 add0r. - by move/(ler_lt_trans _)/(ltrW); apply. + by move/(le_lt_trans _)/ltW; apply. - move/(_ 0): subf; rewrite normr0 mulr0 add0r. - by move/(ler_lt_trans _)/(ltrW); apply. + by move/(le_lt_trans _)/ltW; apply. by rewrite -gtz0_ge1 normr_gt0. apply/ler_wpmul2l => //; rewrite {}/N {}/M. rewrite [X in X + _ <= _]addrACA [X in _ + X <= _]addrACA. @@ -631,10 +635,10 @@ Proof. split. + elim/quotW=> f; elim/quotW=> g; elim/quotW=> h. by rewrite !piE /=; apply/eqmodP/eqv_refl_eq. + apply/eqP; rewrite !piE => /eqmodP/qzeqvP /= [k hk]. - have := (hk 0); rewrite /qzendoC normr0 => /ltrW ge0k. + have := (hk 0); rewrite /qzendoC normr0 => /ltW ge0k. move/(_ (k+1)): hk; rewrite /qzendoC !(mulr0, mulr1). rewrite subr0 ger0_norm ?ler_paddr //. - by apply/negP; rewrite -lerNgt ler_addl. + by apply/negP; rewrite -leNgt ler_addl. Qed. Let edxmulA := let: And5 h _ _ _ _ := edxcomring in h. @@ -668,43 +672,43 @@ Proof. move=> edf posf; wlog: C / 0 < C => [wlog|]. + case: (ltrP 0 C) => [gt0_C|le0_C]; first by apply: wlog. case: (wlog 1) => // N hN; exists N => p /hN. - by move/(ler_lt_trans _); apply; apply/(ler_trans le0_C). + by move/(le_lt_trans _); apply; apply/(le_trans le0_C). move=> gt0_C; case/is_eqzendoPP: {+}edf => D edfD. have [|M gt0_M slf] := eqzendo_suplin _ (D := D) edf posf. -+ by apply: (ler_lt_trans _ (edfD 0 0)). ++ by apply: (le_lt_trans _ (edfD 0 0)). pose g (p : int) := f (p - (p %% M)%Z). pose E : int := \sum_(0 <= i < `|M|) `|f i|. have bd_fBg p : `|f p - g p| < E + D. + rewrite /g {1 2}[p](divz_eq _ M) addrK (addrC E D). rewrite -[X in `|X|](subrK (f (p %% M)%Z)). - apply/(ler_lt_trans (ler_norm_add _ _))/ltr_le_add. + apply/(le_lt_trans (ler_norm_add _ _))/ltr_le_add. * by rewrite -addrA -opprD. rewrite /E (bigD1_seq (absz (p %% M)%Z)) /=. * rewrite mem_index_iota /= -ltz_nat !abszE ger0_norm. - - by rewrite modz_ge0 //gtr_eqF. + - by rewrite modz_ge0 //gt_eqF. by rewrite gtr0_norm // ltz_pmod. * by apply: iota_uniq. - * rewrite abszE [`|(_ %% _)%Z|]ger0_norm ?modz_ge0 ?gtr_eqF //. + * rewrite abszE [`|(_ %% _)%Z|]ger0_norm ?modz_ge0 ?gt_eqF //. by rewrite ler_addl sumr_ge0. pose n : int := ((E + D + C) %/ D)%Z; exists (n * M) => p ltp. have := bd_fBg p; rewrite ltr_norml => /andP[h _]; move: h. -rewrite ltr_subr_addl => /(ltr_trans _); apply. +rewrite ltr_subr_addl => /(lt_trans _); apply. rewrite ltr_subr_addl /g {1}[p](divz_eq _ M) addrK. -apply/(ler_lt_trans _ (slf _ _)); last first. +apply/(le_lt_trans _ (slf _ _)); last first. + suff ltMp: M < p. - rewrite -(ltr_pmul2r gt0_M) mul0r -[X in _ [hQneg|hNQneg]. by move=> N hN; exists N => p /hN /=; rewrite ltr_oppr. have: exists2 c : int, 0 < c & forall n : int, 0 < n -> f n < c. + move/asboolPn/existsp_asboolPn: hNQpos => [c hc]. - exists (maxr 0 c + 1); first by rewrite ltz_addr1 ler_maxr lerr. - move=> n gt0_n; rewrite ltz_addr1 ler_maxr -(rwP orP); right. - by rewrite lerNgt -(rwP negP) => h; apply/hc; exists n. + exists (maxr 0 c + 1); first by rewrite ltz_addr1 le_maxr lexx. + move=> n gt0_n; rewrite ltz_addr1 le_maxr -(rwP orP); right. + by rewrite leNgt -(rwP negP) => h; apply/hc; exists n. have: exists2 c : int, 0 < c & forall n : int, 0 < n -> - c < f n. + move/asboolPn/existsp_asboolPn: hNQneg => [c hc]. - exists (maxr (1 - c) 1); first by rewrite ltr_maxr ltr01 orbT. - move=> n gt0_n; rewrite ltr_oppl ltr_maxr -(rwP orP); left. + exists (maxr (1 - c) 1); first by rewrite lt_maxr ltr01 orbT. + move=> n gt0_n; rewrite ltr_oppl lt_maxr -(rwP orP); left. rewrite ltr_oppl opprB ltr_subl_addr ltz_addr1. - by rewrite lerNgt -(rwP negP) => h; apply/hc; exists n. + by rewrite leNgt -(rwP negP) => h; apply/hc; exists n. case=> [cN gt0_cN hN] [cP gt0_cP hP]. have: exists2 C : int, 0 < C & forall n : int, 0 < n -> `|f n| < C. -+ exists (maxr cP cN); first by rewrite ltr_maxr gt0_cP. - move=> n gt0_n; rewrite ltr_norml ltr_oppl !ltr_maxr. ++ exists (maxr cP cN); first by rewrite lt_maxr gt0_cP. + move=> n gt0_n; rewrite ltr_norml ltr_oppl !lt_maxr. by rewrite hP //= andbT [X in _ || X]ltr_oppl hN // orbT. case=> C gt0_C hC; case/is_eqzendoPP: edzf=> D hD. -have gt0_D: 0 < D by apply/(ler_lt_trans _ (hD 0 0)). +have gt0_D: 0 < D by apply/(le_lt_trans _ (hD 0 0)). absurd False => //; apply/hNP; exists (C + D + `|f 1|). move=> n; case: (ltrP 0 n) => [gt0_n|le0_n]. -+ rewrite -addrA (ltr_trans (hC _ gt0_n)) // ltr_addl. - by rewrite (ltr_le_trans gt0_D) // ler_addl. ++ rewrite -addrA (lt_trans (hC _ gt0_n)) // ltr_addl. + by rewrite (lt_le_trans gt0_D) // ler_addl. have: `|f (1 - n)| < C by apply: hC; rewrite subr_gt0. -rewrite -addrA -(ltr_add2r (D + `|f 1|)) => /(ler_lt_trans _); apply. +rewrite -addrA -(ltr_add2r (D + `|f 1|)) => /(le_lt_trans _); apply. rewrite addrCA; have := hD (1 - n) n; rewrite subrK. rewrite -(ltr_add2r (`|f (1 - n)| + `|f 1|)). -move/ltrW/(ler_trans _); apply. set x := (X in _ <= X + _). +move/ltW/(le_trans _); apply. set x := (X in _ <= X + _). have := ler_norm_sub (f (1 - n)) (f 1); rewrite -(ler_add2l x). -move/(ler_trans _); apply; apply/(ler_trans _ (ler_norm_add _ _)). +move/(le_trans _); apply; apply/(le_trans _ (ler_norm_add _ _)). rewrite [X in _ <= `|X|]addrC !addrA subrK. by rewrite opprD addrCA addKr normrN. Qed. @@ -785,17 +789,17 @@ Lemma edxposfPE (f : qzEndo) : edxposf f -> forall C : int, exists N : int, forall p : int, N < p -> C < f p. Proof. (* See edxposf_spec *) move=> /edxposfP gt0_f; case: (edxcmp0_spec (valP f)) => //=. -+ case=> C lt_fC; suff: C < C by rewrite ltrr. - move/(_ C): gt0_f => [n _ le_Cf]; rewrite (ltr_trans le_Cf) //. - by rewrite (ler_lt_trans (ler_norm _)). ++ case=> C lt_fC; suff: C < C by rewrite ltxx. + move/(_ C): gt0_f => [n _ le_Cf]; rewrite (lt_trans le_Cf) //. + by rewrite (le_lt_trans (ler_norm _)). + move=> /(_ 0) [N]; rewrite oppr0 => h. pose M : int := \sum_(0 <= i < `|N|.+1) `|f i|. - move/(_ M): gt0_f => [] [] // n _; rewrite ltrNge => /negP[]. + move/(_ M): gt0_f => [] [] // n _; rewrite ltNge => /negP[]. rewrite {}/M; case: (ltnP n `|N|.+1) => [lt_n_SN|]. * rewrite (bigD1_seq n) 1?(iota_uniq, mem_iota) //=. by rewrite ler_paddr 1?ler_norm //= sumr_ge0. - * rewrite -ltz_nat abszE => /(ler_lt_trans (ler_norm _)) /h. - by move/ltrW/ler_trans; apply; rewrite sumr_ge0. + * rewrite -ltz_nat abszE => /(le_lt_trans (ler_norm _)) /h. + by move/ltW/le_trans; apply; rewrite sumr_ge0. Qed. (* -------------------------------------------------------------------- *) @@ -803,12 +807,12 @@ Local Lemma pi_edxpos_r (f g : qzEndo) : f ~ g -> edxposf f -> edxposf g. Proof. case/qzeqvP=> C bdC /edxposfP /edxposf_spec h. apply/edxposfP => k; case/(_ (C + k) (valP _)): h. -move=> N hN; exists (maxr 0 N + 1); first by rewrite ltz_addr1 ler_maxr. +move=> N hN; exists (maxr 0 N + 1); first by rewrite ltz_addr1 le_maxr. set p : int := maxr _ _ + _; have := bdC p; rewrite distrC. rewrite ltr_norml => /andP[h _]; move: h. -rewrite ltr_subr_addl => /(ltr_trans _); apply. +rewrite ltr_subr_addl => /(lt_trans _); apply. rewrite ltr_subr_addl; apply: hN; rewrite ltz_addr1. -by rewrite ler_maxr lerr orbT. +by rewrite le_maxr lexx orbT. Qed. (* -------------------------------------------------------------------- *) @@ -842,17 +846,17 @@ Proof. split. move=> /edxposfP hf /edxposfP hg; apply/edxposfP => k. case/(edxposf_spec `|k| (valP _)): hf => /= kf hkf. case/(edxposf_spec `|k| (valP _)): hg => /= kg hkg. - exists (maxr 0 (maxr kf kg) + 1); first by rewrite ltz_addr1 ler_maxr. - apply/(@ler_lt_trans _ (`|k| + `|k|)). - * by apply/(ler_trans (ler_norm _))/ler_addr. - by rewrite ltr_add ?(hkf, hkg) // ltz_addr1 !ler_maxr lerr !orbT. + exists (maxr 0 (maxr kf kg) + 1); first by rewrite ltz_addr1 le_maxr. + apply/(@le_lt_trans _ _ (`|k| + `|k|)). + * by apply/(le_trans (ler_norm _))/ler_addr. + by rewrite ltr_add ?(hkf, hkg) // ltz_addr1 !le_maxr lexx !orbT. + elim/quotW=> f; elim/quotW=> g; rewrite !piE /=. move=> /edxposfP hf /edxposfP hg; apply/edxposfP => k. case/(edxposf_spec `|k | (valP _)): hf => /= kf hkf. case/(edxposf_spec `|kf| (valP _)): hg => /= kg hkg. exists (`|kg| + 1); first by rewrite ltz_addr1. - apply/(ler_lt_trans (ler_norm _))/hkf. - apply/(ler_lt_trans (ler_norm _))/hkg. + apply/(le_lt_trans (ler_norm _))/hkf. + apply/(le_lt_trans (ler_norm _))/hkg. by rewrite ltz_addr1 ler_norm. Qed. End EudoxusPos. @@ -877,7 +881,7 @@ Lemma qzeqvDC (f : qzEndo) (c : int) : (f \o (fun x => x + c)) ~ f. Proof. case/is_eqzendoPP: (valP f) => /= C bdC; apply/eqvP; exists (C + `|f c|). move=> k /=; move/(_ k c): bdC; rewrite -{1}(ltr_add2r `|f c| _ C). -by move/(ler_lt_trans (ler_norm_add _ _)); rewrite opprD -!addrA addNr addr0. +by move/(le_lt_trans (ler_norm_add _ _)); rewrite opprD -!addrA addNr addr0. Qed. (* @@ -939,11 +943,11 @@ Lemma eqv_eqzendo f g : Proof. move/eqvP=> [C hC] /is_eqzendoP[C' /is_qzendoP hC']. apply/is_eqzendoP; exists (C *+ 3 + C'); apply/is_qzendoP=> m n. -apply: (ler_lt_trans (@ler_dist_add _ (f (m + n)) _ _)). +apply: (le_lt_trans (@ler_dist_add _ _ (f (m + n)) _ _)). rewrite mulrS -addrA ltr_add //; first by rewrite distrC hC. -apply: (ler_lt_trans (@ler_dist_add _ (f m + f n) _ _)). +apply: (le_lt_trans (@ler_dist_add _ _ (f m + f n) _ _)). rewrite [X in _ < X]addrC ltr_add // opprD addrACA. -by apply: (ler_lt_trans (ler_norm_add _ _)); rewrite ltr_add. +by apply: (le_lt_trans (ler_norm_add _ _)); rewrite ltr_add. Qed. Lemma edxinv_r (x : qzEndo) : @@ -954,25 +958,25 @@ move: x => f; wlog: f / forall n : nat, f (Negz n) = - (f n.+1) => [wlog gt0_f|] have /= := qzeqvN idfun f => /eqvP[C hC]. apply/eqvP; exists `|C|.+1; case=> n /=. by rewrite subrr normr0. - have /= := hC n.+1%:Z; rewrite NegzE => /ltr_trans; apply. - by apply: (ler_lt_trans (ler_norm _)); rewrite ltz_nat. + have /= := hC n.+1%:Z; rewrite NegzE => /lt_trans; apply. + by apply: (le_lt_trans (ler_norm _)); rewrite ltz_nat. pose gh := QZEndo (eqv_eqzendo eq_fg (valP f)); case: (wlog gh) => //. by apply: (@pi_edxpos_r _ gh eq_fg gt0_f). move=> gI hV; exists gI; rewrite -[RHS]hV. by congr (_ * _); apply/eqmodP. move=> fNE gt0_f; have h (p : nat) : exists n : nat, p%:Z <= f n. - by move/edxposfP: gt0_f => /(_ p) [] [|//] n _ /ltrW ?; exists n. + by move/edxposfP: gt0_f => /(_ p) [] [|//] n _ /ltW ?; exists n. pose g p := (ex_minn (h p))%:Z. have [N gt0_g]: { N | forall n, (N <= n)%N -> 0 < g n}. exists `|f 0|.+1 => n lt_f0_n; rewrite /g; case: ex_minnP. - case=> //; rewrite lerNgt => /negP[]. - by rewrite (ler_lt_trans (ler_norm _)). + case=> //; rewrite leNgt => /negP[]. + by rewrite (le_lt_trans (ler_norm _)). have comp_fg : forall n : nat, f (g n) >= n%:Z. by move=> n; rewrite /g; case: ex_minnP. have hrg: forall r, (N <= r)%N -> f (g r - 1) < r%:Z <= f (g r). move=> r /gt0_g; rewrite /g; case: ex_minnP. move=> m le_m_fr hmin gt0_m; rewrite le_m_fr andbT. - rewrite ltrNge; apply/negP; rewrite -predn_int //. + rewrite ltNge; apply/negP; rewrite -predn_int //. move/hmin; case: {le_m_fr hmin} m gt0_m => //=. by move=> m _; rewrite ltnn. have h1: forall m n, (N <= m)%N -> (N <= n)%N -> @@ -994,7 +998,7 @@ suff hg: eqzlift (fun p => g (N + p)%N) \is a eqzendo. suff [C hC]: exists C : int, forall n, (N <= n)%N -> `|f (g n) - n%:Z| < C. have bdnat n: `|f (g (N + n)%N) - n%:Z| < C + N. rewrite -[X in `|X|](@subrK _ N%:Z). - apply: (ler_lt_trans (ler_norm_add _ _)); rewrite ltr_le_add //. + apply: (le_lt_trans (ler_norm_add _ _)); rewrite ltr_le_add //. by rewrite -addrA -opprD [(N+_)%N]addnC hC // leq_addl. exists (C + N%:Z) => n; rewrite /qzendoC mulr1; case: n => //= n. set x := (X in g X); rewrite NegzE (_ : f (- (g x)) = -(f (g x))). @@ -1002,21 +1006,21 @@ suff hg: eqzlift (fun p => g (N + p)%N) \is a eqzendo. by case=> // p _; rewrite -NegzE fNE. by rewrite -opprD normrN {}/x. have /eqvP[/= C hC] := qzeqvDC f (-1); exists `|C|.+1. - move=> n le_Nn; rewrite ltr_norml (@ltr_le_trans _ 0) /=. + move=> n le_Nn; rewrite ltr_norml (@lt_le_trans _ _ 0) /=. - by rewrite oppr_lt0. - by rewrite subr_ge0; have /andP[] := hrg _ le_Nn. - rewrite (@ler_lt_trans _ `|C|) //; last by rewrite ltz_nat ltnS. - apply: (@ler_trans _ (f (g n) - f (g n - 1))). - by rewrite ler_sub //; have /andP[/ltrW] := hrg _ le_Nn. - have /ltrW := hC (g n); rewrite distrC ler_norml => /andP[_]. - by move/ler_trans; apply; rewrite ler_norm. + rewrite (@le_lt_trans _ _ `|C|) //; last by rewrite ltz_nat ltnS. + apply: (@le_trans _ _ (f (g n) - f (g n - 1))). + by rewrite ler_sub //; have /andP[/ltW] := hrg _ le_Nn. + have /ltW := hC (g n); rewrite distrC ler_norml => /andP[_]. + by move/le_trans; apply; rewrite ler_norm. set gh := fun p => g (N + p)%N; apply: eqzendo_nat. have [C hC]: exists C : int, forall (m n : nat), `|f (gh (n + m)%N - gh n - gh m)| < C. suff [C hC]: exists C : int, forall (m n : nat), (N <= m)%N -> (N <= n)%N -> `|f (g (n + m)%N - g n - g m)| < C. exists C. - +(* + have bd1: exists C : int, forall (m n : nat), (N <= m)%N -> (N <= n)%N -> f (g (n + m)%N - g n - g m) > C. have /eqvP[C hC] := L1 f; exists (-C) => m n le_Mm le_Mn. @@ -1128,7 +1132,8 @@ have hC: exists C : int, forall n m, `|g (n + m)%N - g n - g m| <= C. * have le_Nn := leq_trans le_Nm le_mn. by rewrite ltr_paddr ?normr_ge0 // ltr_normr hC. rewrite eq0_g => /eqP->; rewrite subr0. - +*) +Admitted. Parameter (edxinv : eudoxus -> eudoxus). @@ -1165,15 +1170,25 @@ Let edxpos_total := let: And4 _ h _ _ := edxpos_order in h. Let edxpos_add := let: And4 _ _ h _ := edxpos_order in h. Let edxpos_mul := let: And4 _ _ _ h := edxpos_order in h. -Definition eudoxus_numDomainMixin := +Definition eudoxus_realLeMixin := PosNumMixin edxpos_N0 edxpos_total edxpos_add edxpos_mul. -Canonical eudoxus_numDomainType := - Eval hnf in NumDomainType eudoxus eudoxus_numDomainMixin. +Canonical eudoxus_porderType := + Eval hnf in POrderType ring_display eudoxus eudoxus_realLeMixin. +Canonical eudoxus_latticeType := + Eval hnf in LatticeType eudoxus eudoxus_realLeMixin. +Canonical eudoxus_distrLatticeType := + Eval hnf in DistrLatticeType eudoxus eudoxus_realLeMixin. +Canonical eudoxus_orderType := + Eval hnf in OrderType eudoxus (le_total edxpos_N0 edxpos_total edxpos_add edxpos_mul). +Canonical rat_numDomainType := + Eval hnf in NumDomainType eudoxus eudoxus_realLeMixin. +Canonical eudoxus_normedZmodType := + Eval hnf in NormedZmodType eudoxus eudoxus eudoxus_realLeMixin. Canonical eudoxus_numFieldType := Eval hnf in [numFieldType of eudoxus]. Canonical eudoxus_realDomainType := - Eval hnf in RealDomainType eudoxus (le_total edxpos_total). + Eval hnf in [realDomainType of eudoxus]. Canonical eudoxus_realFieldType := Eval hnf in [realFieldType of eudoxus]. @@ -1189,12 +1204,12 @@ elim/quotW=> /= f; have /is_eqzendoP[C /qzendo_sublin] /= := valP f. case=> [A] [B] ltf; exists `|A|%N.+1; rewrite edx_ltrE /=. rewrite edxnatrE !piE; apply/edxposfP => /=; rewrite /qzendoC => k. have {ltf} ltf (m : int) : 0 < m -> f m < `|A| * m + B. -+ move=> gt0_m; apply/(ler_lt_trans (ler_norm _)). - apply/(ltr_le_trans (ltf m)); rewrite ler_add2r. ++ move=> gt0_m; apply/(le_lt_trans (ler_norm _)). + apply/(lt_le_trans (ltf m)); rewrite ler_add2r. by rewrite gtr0_norm // ler_pmul2r // ler_norm. exists (`|k + B| + 1); first by rewrite ltz_addr1. rewrite ltr_subr_addl -ltr_subr_addr. -rewrite (ltr_trans (ltf _ _)) ?ltz_addr1 //. +rewrite (lt_trans (ltf _ _)) ?ltz_addr1 //. rewrite intS [1+_]addrC [in X in _ < X]mulrDr mulr1. rewrite [`|A|*_]mulrC -addrA ler_lt_add //. by rewrite ltr_subr_addl ltz_addr1 ler_norm.