diff options
Diffstat (limited to 'theories')
35 files changed, 1594 insertions, 1529 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 1d5e3e54ff..57cc8c4e90 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -9,9 +9,12 @@ (************************************************************************) (** The type [bool] is defined in the prelude as - [Inductive bool : Set := true : bool | false : bool] *) +[[ +Inductive bool : Set := true : bool | false : bool +]] + *) -(** Most of the lemmas in this file are trivial after breaking all booleans *) +(** Most of the lemmas in this file are trivial by case analysis *) Ltac destr_bool := intros; destruct_all bool; simpl in *; trivial; try discriminate. @@ -75,9 +78,9 @@ Proof. destr_bool; intuition. Qed. -(**********************) +(************************) (** * Order on booleans *) -(**********************) +(************************) Definition leb (b1 b2:bool) := match b1 with @@ -91,11 +94,28 @@ Proof. destr_bool; intuition. Qed. -(* Infix "<=" := leb : bool_scope. *) +Definition ltb (b1 b2:bool) := + match b1 with + | true => False + | false => b2 = true + end. +Hint Unfold ltb: bool. + +Definition compareb (b1 b2 : bool) := + match b1, b2 with + | false, true => Lt + | true, false => Gt + | _, _ => Eq + end. + +Lemma compareb_spec : forall b1 b2, + CompareSpec (b1 = b2) (ltb b1 b2) (ltb b2 b1) (compareb b1 b2). +Proof. destr_bool; auto. Qed. + -(*************) +(***************) (** * Equality *) -(*************) +(***************) Definition eqb (b1 b2:bool) : bool := match b1, b2 with @@ -131,9 +151,9 @@ Proof. destr_bool; intuition. Qed. -(************************) +(**********************************) (** * A synonym of [if] on [bool] *) -(************************) +(**********************************) Definition ifb (b1 b2 b3:bool) : bool := match b1 with @@ -143,9 +163,9 @@ Definition ifb (b1 b2 b3:bool) : bool := Open Scope bool_scope. -(****************************) -(** * De Morgan laws *) -(****************************) +(*********************) +(** * De Morgan laws *) +(*********************) Lemma negb_orb : forall b1 b2:bool, negb (b1 || b2) = negb b1 && negb b2. Proof. @@ -157,9 +177,9 @@ Proof. destr_bool. Qed. -(********************************) -(** * Properties of [negb] *) -(********************************) +(***************************) +(** * Properties of [negb] *) +(***************************) Lemma negb_involutive : forall b:bool, negb (negb b) = b. Proof. @@ -212,9 +232,9 @@ Proof. Qed. -(********************************) -(** * Properties of [orb] *) -(********************************) +(**************************) +(** * Properties of [orb] *) +(**************************) Lemma orb_true_iff : forall b1 b2, b1 || b2 = true <-> b1 = true \/ b2 = true. @@ -305,6 +325,11 @@ Proof. Qed. Hint Resolve orb_negb_r: bool. +Lemma orb_negb_l : forall b:bool, negb b || b = true. +Proof. + destr_bool. +Qed. + Notation orb_neg_b := orb_negb_r (only parsing). (** Commutativity *) @@ -322,9 +347,9 @@ Proof. Qed. Hint Resolve orb_comm orb_assoc: bool. -(*******************************) -(** * Properties of [andb] *) -(*******************************) +(***************************) +(** * Properties of [andb] *) +(***************************) Lemma andb_true_iff : forall b1 b2:bool, b1 && b2 = true <-> b1 = true /\ b2 = true. @@ -404,6 +429,11 @@ Proof. Qed. Hint Resolve andb_negb_r: bool. +Lemma andb_negb_l : forall b:bool, negb b && b = false. +Proof. + destr_bool. +Qed. + Notation andb_neg_b := andb_negb_r (only parsing). (** Commutativity *) @@ -422,9 +452,9 @@ Qed. Hint Resolve andb_comm andb_assoc: bool. -(*******************************************) +(*****************************************) (** * Properties mixing [andb] and [orb] *) -(*******************************************) +(*****************************************) (** Distributivity *) @@ -476,9 +506,88 @@ Notation absoption_andb := absorption_andb (only parsing). Notation absoption_orb := absorption_orb (only parsing). (* end hide *) -(*********************************) -(** * Properties of [xorb] *) -(*********************************) +(****************************) +(** * Properties of [implb] *) +(****************************) + +Lemma implb_true_iff : forall b1 b2:bool, implb b1 b2 = true <-> (b1 = true -> b2 = true). +Proof. + destr_bool; intuition. +Qed. + +Lemma implb_false_iff : forall b1 b2:bool, implb b1 b2 = false <-> (b1 = true /\ b2 = false). +Proof. + destr_bool; intuition. +Qed. + +Lemma implb_orb : forall b1 b2:bool, implb b1 b2 = negb b1 || b2. +Proof. + destr_bool. +Qed. + +Lemma implb_negb_orb : forall b1 b2:bool, implb (negb b1) b2 = b1 || b2. +Proof. + destr_bool. +Qed. + +Lemma implb_true_r : forall b:bool, implb b true = true. +Proof. + destr_bool. +Qed. + +Lemma implb_false_r : forall b:bool, implb b false = negb b. +Proof. + destr_bool. +Qed. + +Lemma implb_true_l : forall b:bool, implb true b = b. +Proof. + destr_bool. +Qed. + +Lemma implb_false_l : forall b:bool, implb false b = true. +Proof. + destr_bool. +Qed. + +Lemma implb_same : forall b:bool, implb b b = true. +Proof. + destr_bool. +Qed. + +Lemma implb_contrapositive : forall b1 b2:bool, implb (negb b1) (negb b2) = implb b2 b1. +Proof. + destr_bool. +Qed. + +Lemma implb_negb : forall b1 b2:bool, implb (negb b1) b2 = implb (negb b2) b1. +Proof. + destr_bool. +Qed. + +Lemma implb_curry : forall b1 b2 b3:bool, implb (b1 && b2) b3 = implb b1 (implb b2 b3). +Proof. + destr_bool. +Qed. + +Lemma implb_andb_distrib_r : forall b1 b2 b3:bool, implb b1 (b2 && b3) = implb b1 b2 && implb b1 b3. +Proof. + destr_bool. +Qed. + +Lemma implb_orb_distrib_r : forall b1 b2 b3:bool, implb b1 (b2 || b3) = implb b1 b2 || implb b1 b3. +Proof. + destr_bool. +Qed. + +Lemma implb_orb_distrib_l : forall b1 b2 b3:bool, implb (b1 || b2) b3 = implb b1 b3 && implb b2 b3. +Proof. + destr_bool. +Qed. + +(***************************) +(** * Properties of [xorb] *) +(***************************) (** [false] is neutral for [xorb] *) @@ -632,9 +741,9 @@ Proof. Qed. Hint Resolve trans_eq_bool : core. -(*****************************************) +(***************************************) (** * Reflection of [bool] into [Prop] *) -(*****************************************) +(***************************************) (** [Is_true] and equality *) @@ -752,10 +861,10 @@ Proof. destr_bool. Qed. -(*****************************************) +(***********************************************) (** * Alternative versions of [andb] and [orb] - with lazy behavior (for vm_compute) *) -(*****************************************) + with lazy behavior (for vm_compute) *) +(***********************************************) Declare Scope lazy_bool_scope. @@ -776,11 +885,11 @@ Proof. reflexivity. Qed. -(*****************************************) +(************************************************) (** * Reflect: a specialized inductive type for relating propositions and booleans, - as popularized by the Ssreflect library. *) -(*****************************************) + as popularized by the Ssreflect library. *) +(************************************************) Inductive reflect (P : Prop) : bool -> Set := | ReflectT : P -> reflect P true @@ -823,3 +932,11 @@ Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b'). Proof. destruct b, b'; now constructor. Defined. + +(** Notations *) +Module BoolNotations. +Infix "<=" := leb : bool_scope. +Infix "<" := ltb : bool_scope. +Infix "?=" := compareb (at level 70) : bool_scope. +Infix "=?" := eqb (at level 70) : bool_scope. +End BoolNotations. diff --git a/theories/Bool/BoolOrder.v b/theories/Bool/BoolOrder.v new file mode 100644 index 0000000000..61aab607a9 --- /dev/null +++ b/theories/Bool/BoolOrder.v @@ -0,0 +1,105 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** The order relations [le] [lt] and [compare] are defined in [Bool.v] *) + +(** Order properties of [bool] *) + +Require Export Bool. +Require Import Orders. + +Local Notation le := Bool.leb. +Local Notation lt := Bool.ltb. +Local Notation compare := Bool.compareb. +Local Notation compare_spec := Bool.compareb_spec. + +(** * Order [le] *) + +Lemma le_refl : forall b, le b b. +Proof. destr_bool. Qed. + +Lemma le_trans : forall b1 b2 b3, + le b1 b2 -> le b2 b3 -> le b1 b3. +Proof. destr_bool. Qed. + +Lemma le_true : forall b, le b true. +Proof. destr_bool. Qed. + +Lemma false_le : forall b, le false b. +Proof. intros; constructor. Qed. + +Instance le_compat : Proper (eq ==> eq ==> iff) le. +Proof. intuition. Qed. + +(** * Strict order [lt] *) + +Lemma lt_irrefl : forall b, ~ lt b b. +Proof. destr_bool; auto. Qed. + +Lemma lt_trans : forall b1 b2 b3, + lt b1 b2 -> lt b2 b3 -> lt b1 b3. +Proof. destr_bool; auto. Qed. + +Instance lt_compat : Proper (eq ==> eq ==> iff) lt. +Proof. intuition. Qed. + +Lemma lt_trichotomy : forall b1 b2, { lt b1 b2 } + { b1 = b2 } + { lt b2 b1 }. +Proof. destr_bool; auto. Qed. + +Lemma lt_total : forall b1 b2, lt b1 b2 \/ b1 = b2 \/ lt b2 b1. +Proof. destr_bool; auto. Qed. + +Lemma lt_le_incl : forall b1 b2, lt b1 b2 -> le b1 b2. +Proof. destr_bool; auto. Qed. + +Lemma le_lteq_dec : forall b1 b2, le b1 b2 -> { lt b1 b2 } + { b1 = b2 }. +Proof. destr_bool; auto. Qed. + +Lemma le_lteq : forall b1 b2, le b1 b2 <-> lt b1 b2 \/ b1 = b2. +Proof. destr_bool; intuition. Qed. + + +(** * Order structures *) + +(* Class structure *) +Instance le_preorder : PreOrder le. +Proof. +split. +- intros b; apply le_refl. +- intros b1 b2 b3; apply le_trans. +Qed. + +Instance lt_strorder : StrictOrder lt. +Proof. +split. +- intros b; apply lt_irrefl. +- intros b1 b2 b3; apply lt_trans. +Qed. + +(* Module structure *) +Module BoolOrd <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. + Definition t := bool. + Definition eq := @eq bool. + Definition eq_equiv := @eq_equivalence bool. + Definition lt := lt. + Definition lt_strorder := lt_strorder. + Definition lt_compat := lt_compat. + Definition le := le. + Definition le_lteq := le_lteq. + Definition lt_total := lt_total. + Definition compare := compare. + Definition compare_spec := compare_spec. + Definition eq_dec := bool_dec. + Definition eq_refl := @eq_Reflexive bool. + Definition eq_sym := @eq_Symmetric bool. + Definition eq_trans := @eq_Transitive bool. + Definition eqb := eqb. + Definition eqb_eq := eqb_true_iff. +End BoolOrd. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index f78c0ecc1e..ad0124db6d 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -123,7 +123,7 @@ Definition create l x e r := Definition assert_false := create. -Fixpoint bal l x d r := +Definition bal l x d r := let hl := height l in let hr := height r in if gt_le_dec hl (hr+2) then @@ -191,7 +191,7 @@ Fixpoint remove_min l x d r : t*(key*elt) := [|height t1 - height t2| <= 2]. *) -Fixpoint merge s1 s2 := match s1,s2 with +Definition merge s1 s2 := match s1,s2 with | Leaf, _ => s2 | _, Leaf => s1 | _, Node l2 x2 d2 r2 h2 => diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 0f2717beef..9f77221d5a 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -26,6 +26,8 @@ Inductive Empty_set : Set :=. Inductive unit : Set := tt : unit. +Register unit as core.unit.type. +Register tt as core.unit.tt. (********************************************************************) (** * The boolean datatype *) @@ -198,6 +200,10 @@ Notation "x + y" := (sum x y) : type_scope. Arguments inl {A B} _ , [A] B _. Arguments inr {A B} _ , A [B] _. +Register sum as core.sum.type. +Register inl as core.sum.inl. +Register inr as core.sum.inr. + (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 855db8bc3f..2a84456500 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -179,7 +179,7 @@ Definition del_head_int n d := (** [del_tail n d] removes [n] digits at end of [d] or returns [zero] if [d] has less than [n] digits. *) -Fixpoint del_tail n d := rev (del_head n (rev d)). +Definition del_tail n d := rev (del_head n (rev d)). Definition del_tail_int n d := match d with diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 5d5f74db44..638e8e8308 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -1141,7 +1141,7 @@ Section Map. Qed. Lemma map_eq_cons : forall l l' b, - map l = b :: l' -> exists a tl, l = a :: tl /\ b = f a /\ l' = map tl. + map l = b :: l' -> exists a tl, l = a :: tl /\ f a = b /\ map tl = l'. Proof. intros l l' b Heq. destruct l; inversion_clear Heq. @@ -1149,7 +1149,7 @@ Section Map. Qed. Lemma map_eq_app : forall l l1 l2, - map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ l1 = map l1' /\ l2 = map l2'. + map l = l1 ++ l2 -> exists l1' l2', l = l1' ++ l2' /\ map l1' = l1 /\ map l2' = l2. Proof. induction l; simpl; intros l1 l2 Heq. - symmetry in Heq; apply app_eq_nil in Heq; destruct Heq; subst. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index ea53618acb..04685cc3eb 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -126,7 +126,7 @@ Infix "?=" := compare (at level 70, no associativity) : N_scope. (** Boolean equality and comparison *) -Fixpoint eqb n m := +Definition eqb n m := match n, m with | 0, 0 => true | pos p, pos q => Pos.eqb p q @@ -313,7 +313,7 @@ Definition land n m := (** Logical [diff] *) -Fixpoint ldiff n m := +Definition ldiff n m := match n, m with | 0, _ => 0 | _, 0 => n diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index bacc4a7650..2c112c3469 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -135,29 +135,29 @@ Register Inline subcarry. Definition addc_def x y := let r := x + y in if r < x then C1 r else C0 r. -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive addc := #int63_addc. Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : int63_scope. Definition addcarryc_def x y := let r := addcarry x y in if r <= x then C1 r else C0 r. -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive addcarryc := #int63_addcarryc. Definition subc_def x y := if y <= x then C0 (x - y) else C1 (x - y). -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive subc := #int63_subc. Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : int63_scope. Definition subcarryc_def x y := if y < x then C0 (x - y - 1) else C1 (x - y - 1). -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive subcarryc := #int63_subcarryc. Definition diveucl_def x y := (x/y, x\%y). -(* the same but direct implementation for effeciancy *) +(* the same but direct implementation for efficiency *) Primitive diveucl := #int63_diveucl. Primitive diveucl_21 := #int63_div21. @@ -978,7 +978,7 @@ Proof. case (leb_spec digits j); rewrite H; auto with zarith. intros _ HH; generalize (HH H1); discriminate. clear H. - generalize (ltb_spec j i); case ltb; intros H2; unfold bit; simpl. + generalize (ltb_spec j i); case Int63.ltb; intros H2; unfold bit; simpl. assert (F2: (φ j < φ i)%Z) by (case H2; auto); clear H2. replace (is_zero (((x << i) >> j) << (digits - 1))) with true; auto. case (to_Z_bounded j); intros H1j H2j. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index bd5225d9ef..74cdd1797c 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -22,6 +22,10 @@ Declare Scope Q_scope. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. Arguments Qmake _%Z _%positive. + +Register Q as rat.Q.type. +Register Qmake as rat.Q.Qmake. + Open Scope Q_scope. Ltac simpl_mult := rewrite ?Pos2Z.inj_mul. @@ -101,6 +105,10 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope. Notation "x >= y" := (Qle y x)(only parsing) : Q_scope. Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope. +Register Qeq as rat.Q.Qeq. +Register Qle as rat.Q.Qle. +Register Qlt as rat.Q.Qlt. + (** injection from Z is injective. *) Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b. @@ -278,6 +286,11 @@ Infix "*" := Qmult : Q_scope. Notation "/ x" := (Qinv x) : Q_scope. Infix "/" := Qdiv : Q_scope. +Register Qplus as rat.Q.Qplus. +Register Qminus as rat.Q.Qminus. +Register Qopp as rat.Q.Qopp. +Register Qmult as rat.Q.Qmult. + (** A light notation for [Zpos] *) Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b). @@ -1053,6 +1066,8 @@ Definition Qpower (q:Q) (z:Z) := Notation " q ^ z " := (Qpower q z) : Q_scope. +Register Qpower as rat.Q.Qpower. + Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower. Proof. intros x x' Hx y y' Hy. rewrite <- Hy; clear y' Hy. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyAbs.v b/theories/Reals/Cauchy/ConstructiveCauchyAbs.v index ce263e1d21..f8c6429982 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyAbs.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyAbs.v @@ -32,8 +32,8 @@ Local Open Scope CReal_scope. CReal_abs : CReal -> CReal *) Lemma CauchyAbsStable : forall xn : positive -> Q, - QCauchySeq xn id - -> QCauchySeq (fun n => Qabs (xn n)) id. + QCauchySeq xn + -> QCauchySeq (fun n => Qabs (xn n)). Proof. intros xn cau n p q H H0. specialize (cau n p q H H0). diff --git a/theories/Reals/Cauchy/ConstructiveCauchyReals.v b/theories/Reals/Cauchy/ConstructiveCauchyReals.v index 8ca65c30c8..70574f6135 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyReals.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyReals.v @@ -40,104 +40,16 @@ Require CMorphisms. WARNING: this module is not meant to be imported directly, please import `Reals.Abstract.ConstructiveReals` instead. *) -Definition QSeqEquiv (un vn : positive -> Q) (cvmod : positive -> positive) +Definition QCauchySeq (un : positive -> Q) : Prop := forall (k : positive) (p q : positive), - Pos.le (cvmod k) p - -> Pos.le (cvmod k) q - -> Qlt (Qabs (un p - vn q)) (1 # k). - -(* A Cauchy sequence is a sequence equivalent to itself. - If sequences are equivalent, they are both Cauchy and have the same limit. *) -Definition QCauchySeq (un : positive -> Q) (cvmod : positive -> positive) : Prop - := QSeqEquiv un un cvmod. - -Lemma QSeqEquiv_sym : forall (un vn : positive -> Q) (cvmod : positive -> positive), - QSeqEquiv un vn cvmod - -> QSeqEquiv vn un cvmod. -Proof. - intros. intros k p q H0 H1. - rewrite Qabs_Qminus. apply H; assumption. -Qed. - -Lemma factorDenom : forall (a:Z) (b d:positive), (a # (d * b)) == (1#d) * (a#b). -Proof. - intros. unfold Qeq. simpl. destruct a; reflexivity. -Qed. - -Lemma QSeqEquiv_trans : forall (un vn wn : positive -> Q) - (cvmod cvmodw : positive -> positive), - QSeqEquiv un vn cvmod - -> QSeqEquiv vn wn cvmodw - -> QSeqEquiv un wn (fun q => Pos.max (cvmod (2 * q)%positive) - (cvmodw (2 * q)%positive)). -Proof. - intros. intros k p q H1 H2. - setoid_replace (un p - wn q) with (un p - vn p + (vn p - wn q)). - apply (Qle_lt_trans - _ (Qabs (un p - vn p) + Qabs (vn p - wn q))). - apply Qabs_triangle. apply (Qlt_le_trans _ ((1 # (2*k)) + (1 # (2*k)))). - apply Qplus_lt_le_compat. - - assert ((cvmod (2 * k)%positive <= p)%positive). - { apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive) - (cvmodw (2 * k)%positive))). - apply Pos.le_max_l. assumption. } - apply H. assumption. assumption. - - apply Qle_lteq. left. apply H0. - apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive) - (cvmodw (2 * k)%positive))). - apply Pos.le_max_r. assumption. - apply (Pos.le_trans _ (Pos.max (cvmod (2 * k)%positive) - (cvmodw (2 * k)%positive))). - apply Pos.le_max_r. assumption. - - rewrite (factorDenom _ _ 2). ring_simplify. apply Qle_refl. - - ring. -Qed. - -Definition QSeqEquivEx (un vn : positive -> Q) : Prop - := exists (cvmod : positive -> positive), QSeqEquiv un vn cvmod. - -Lemma QSeqEquivEx_sym : forall (un vn : positive -> Q), - QSeqEquivEx un vn -> QSeqEquivEx vn un. -Proof. - intros. destruct H. exists x. apply QSeqEquiv_sym. apply H. -Qed. - -Lemma QSeqEquivEx_trans : forall un vn wn : positive -> Q, - QSeqEquivEx un vn - -> QSeqEquivEx vn wn - -> QSeqEquivEx un wn. -Proof. - intros. destruct H,H0. - exists (fun q => Pos.max (x (2 * q)%positive) (x0 (2 * q)%positive)). - apply (QSeqEquiv_trans un vn wn); assumption. -Qed. - -Lemma QSeqEquiv_cau_r : forall (un vn : positive -> Q) (cvmod : positive -> positive), - QSeqEquiv un vn cvmod - -> QCauchySeq vn (fun k => cvmod (2 * k)%positive). -Proof. - intros. intros k p q H0 H1. - setoid_replace (vn p - vn q) - with (vn p - - un (cvmod (2 * k)%positive) - + (un (cvmod (2 * k)%positive) - vn q)). - - apply (Qle_lt_trans - _ (Qabs (vn p - - un (cvmod (2 * k)%positive)) - + Qabs (un (cvmod (2 * k)%positive) - vn q))). - apply Qabs_triangle. - apply (Qlt_le_trans _ ((1 # (2 * k)) + (1 # (2 * k)))). - apply Qplus_lt_le_compat. - + rewrite Qabs_Qminus. apply H. apply Pos.le_refl. assumption. - + apply Qle_lteq. left. apply H. apply Pos.le_refl. assumption. - + rewrite (factorDenom _ _ 2). ring_simplify. apply Qle_refl. - - ring. -Qed. + Pos.le k p + -> Pos.le k q + -> Qlt (Qabs (un p - un q)) (1 # k). (* A Cauchy real is a Cauchy sequence with the standard modulus *) Definition CReal : Set - := { x : (positive -> Q) | QCauchySeq x id }. + := { x : (positive -> Q) | QCauchySeq x }. Declare Scope CReal_scope. @@ -272,78 +184,6 @@ Proof. apply Qle_Qabs. apply H. Qed. -(* The equality on Cauchy reals is just QSeqEquiv, - which is independant of the convergence modulus. *) -Lemma CRealEq_modindep : forall (x y : CReal), - QSeqEquivEx (proj1_sig x) (proj1_sig y) - <-> forall n:positive, - Qle (Qabs (proj1_sig x n - proj1_sig y n)) (2 # n). -Proof. - assert (forall x y: CReal, QSeqEquivEx (proj1_sig x) (proj1_sig y) -> x <= y ). - { intros [xn limx] [yn limy] [cvmod H] [n abs]. simpl in abs, H. - pose (xn n - yn n - (2#n)) as eps. - destruct (Qarchimedean (/eps)) as [k maj]. - remember (Pos.max (cvmod k) n) as p. - assert (Pos.le (cvmod k) p). - { rewrite Heqp. apply Pos.le_max_l. } - assert (n <= p)%positive. - { rewrite Heqp. apply Pos.le_max_r. } - specialize (H k p p H0 H0). - setoid_replace (Z.pos k #1)%Q with (/ (1#k)) in maj. 2: reflexivity. - apply Qinv_lt_contravar in maj. 2: reflexivity. unfold eps in maj. - clear abs. (* less precise majoration *) - apply (Qplus_lt_r _ _ (2#n)) in maj. ring_simplify in maj. - apply (Qlt_not_le _ _ maj). clear maj. - setoid_replace (xn n + -1 * yn n) - with (xn n - xn p + (xn p - yn p + (yn p - yn n))). - 2: ring. - setoid_replace (2 # n)%Q with ((1 # n) + (1#n)). - rewrite <- Qplus_assoc. - apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)). - apply Qlt_le_weak. apply limx. apply Pos.le_refl. assumption. - rewrite (Qplus_comm (1#n)). - apply Qplus_le_compat. apply (Qle_trans _ _ _ (Qle_Qabs _)). - apply Qlt_le_weak. exact H. - apply (Qle_trans _ _ _ (Qle_Qabs _)). apply Qlt_le_weak. apply limy. - assumption. apply Pos.le_refl. ring_simplify. reflexivity. - unfold eps. unfold Qminus. rewrite <- Qlt_minus_iff. exact abs. } - split. - - rewrite <- CRealEq_diff. intros. split. - apply H, QSeqEquivEx_sym. exact H0. apply H. exact H0. - - clear H. intros. destruct x as [xn limx], y as [yn limy]. - exists (fun q:positive => 2 * (3 * q))%positive. intros k p q H0 H1. - unfold proj1_sig. specialize (H (2 * (3 * k))%positive). - assert (3 * k <= 2 * (3 * k))%positive. - { generalize (3 * k)%positive. intros. apply (Pos.le_trans _ (1 * p0)). - apply Pos.le_refl. rewrite <- Pos.mul_le_mono_r. discriminate. } - setoid_replace (xn p - yn q) - with (xn p - xn (2 * (3 * k))%positive - + (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive - + (yn (2 * (3 * k))%positive - yn q))). - 2: ring. - setoid_replace (1 # k)%Q with ((1 # 3 * k) + ((1 # 3 * k) + (1 # 3 * k))). - apply (Qle_lt_trans - _ (Qabs (xn p - xn (2 * (3 * k))%positive) - + (Qabs (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive - + (yn (2 * (3 * k))%positive - yn q))))). - apply Qabs_triangle. apply Qplus_lt_le_compat. - apply limx. apply (Pos.le_trans _ (2 * (3 * k))). assumption. assumption. - assumption. - apply (Qle_trans - _ (Qabs (xn (2 * (3 * k))%positive - yn (2 * (3 * k))%positive) - + Qabs (yn (2 * (3 * k))%positive - yn q))). - apply Qabs_triangle. apply Qplus_le_compat. - setoid_replace (1 # 3 * k)%Q with (2 # 2 * (3 * k))%Q. apply H. - rewrite (factorDenom _ _ 3). - rewrite (factorDenom _ _ 2). rewrite (factorDenom _ _ 3). - rewrite Qmult_assoc. rewrite (Qmult_comm (1#2)). - rewrite <- Qmult_assoc. apply Qmult_comp. reflexivity. - unfold Qeq. reflexivity. - apply Qle_lteq. left. apply limy. assumption. - apply (Pos.le_trans _ (2 * (3 * k))). assumption. assumption. - rewrite (factorDenom _ _ 3). ring_simplify. reflexivity. -Qed. - (* Extend separation to all indices above *) Lemma CRealLt_aboveSig : forall (x y : CReal) (n : positive), (Qlt (2 # n) @@ -687,8 +527,7 @@ Qed. (* Injection of Q into CReal *) -Lemma ConstCauchy : forall q : Q, - QCauchySeq (fun _ => q) id. +Lemma ConstCauchy : forall q : Q, QCauchySeq (fun _ => q). Proof. intros. intros k p r H H0. unfold Qminus. rewrite Qplus_opp_r. unfold Qlt. simpl. @@ -842,78 +681,37 @@ Qed. (* Algebraic operations *) Lemma CReal_plus_cauchy - : forall (xn yn zn : positive -> Q) (cvmod : positive -> positive), - QSeqEquiv xn yn cvmod - -> QCauchySeq zn id - -> QSeqEquiv (fun n:positive => xn n + zn n) (fun n:positive => yn n + zn n) - (fun p => Pos.max (cvmod (2 * p)%positive) - (2 * p)%positive). -Proof. - intros. intros p n k H1 H2. - setoid_replace (xn n + zn n - (yn k + zn k)) - with (xn n - yn k + (zn n - zn k)). - 2: field. - apply (Qle_lt_trans _ (Qabs (xn n - yn k) + Qabs (zn n - zn k))). - apply Qabs_triangle. - setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. + : forall (x y : CReal), + QCauchySeq (fun n : positive => Qred (proj1_sig x (2 * n)%positive + + proj1_sig y (2 * n)%positive)). +Proof. + destruct x as [xn limx], y as [yn limy]; unfold proj1_sig. + intros n p q H H0. + rewrite Qred_correct, Qred_correct. + setoid_replace (xn (2 * p)%positive + yn (2 * p)%positive + - (xn (2 * q)%positive + yn (2 * q)%positive)) + with (xn (2 * p)%positive - xn (2 * q)%positive + + (yn (2 * p)%positive - yn (2 * q)%positive)). + 2: ring. + apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)). + setoid_replace (1#n)%Q with ((1#2*n) + (1#2*n))%Q. apply Qplus_lt_le_compat. - - apply H. apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). - apply Pos.le_max_l. apply H1. - apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). - apply Pos.le_max_l. apply H2. - - apply Qle_lteq. left. apply H0. - apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). - apply Pos.le_max_r. apply H1. - apply (Pos.le_trans _ (Pos.max (cvmod (2 * p)%positive) (2 * p))). - apply Pos.le_max_r. apply H2. + - apply limx. unfold id. apply Pos.mul_le_mono_l, H. + unfold id. apply Pos.mul_le_mono_l, H0. + - apply Qlt_le_weak, limy. + unfold id. apply Pos.mul_le_mono_l, H. + unfold id. apply Pos.mul_le_mono_l, H0. - rewrite Qinv_plus_distr. unfold Qeq. reflexivity. Qed. -Definition CReal_plus (x y : CReal) : CReal. -Proof. - destruct x as [xn limx], y as [yn limy]. - pose proof (CReal_plus_cauchy xn xn yn id limx limy). - exists (fun n : positive => xn (2 * n)%positive + yn (2 * n)%positive). - intros p k n H0 H1. apply H. - - rewrite Pos.max_l. unfold id. rewrite <- Pos.mul_le_mono_l. - exact H0. apply Pos.le_refl. - - rewrite Pos.max_l. unfold id. - apply Pos.mul_le_mono_l. exact H1. apply Pos.le_refl. -Defined. +(* We reduce the rational numbers to accelerate calculations. *) +Definition CReal_plus (x y : CReal) : CReal + := exist _ (fun n : positive => Qred (proj1_sig x (2 * n)%positive + + proj1_sig y (2 * n)%positive)) + (CReal_plus_cauchy x y). Infix "+" := CReal_plus : CReal_scope. -Lemma CReal_plus_nth : forall (x y : CReal) (n : positive), - proj1_sig (x + y) n = Qplus (proj1_sig x (2*n)%positive) - (proj1_sig y (2*n)%positive). -Proof. - intros. destruct x,y; reflexivity. -Qed. - -Lemma CReal_plus_unfold : forall (x y : CReal), - QSeqEquiv (proj1_sig (CReal_plus x y)) - (fun n : positive => proj1_sig x n + proj1_sig y n)%Q - (fun p => 2 * p)%positive. -Proof. - intros [xn limx] [yn limy]. - unfold CReal_plus; simpl. - intros p n k H H0. - setoid_replace (xn (2 * n)%positive + yn (2 * n)%positive - (xn k + yn k))%Q - with (xn (2 * n)%positive - xn k + (yn (2 * n)%positive - yn k))%Q. - 2: field. - apply (Qle_lt_trans _ (Qabs (xn (2 * n)%positive - xn k) + Qabs (yn (2 * n)%positive - yn k))). - apply Qabs_triangle. - setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. - apply Qplus_lt_le_compat. - - apply limx. apply (Pos.le_trans _ n). apply H. - apply (Pos.le_trans _ (1 * n)). apply Pos.le_refl. - apply Pos.mul_le_mono_r. discriminate. exact H0. - - apply Qlt_le_weak. apply limy. apply (Pos.le_trans _ n). apply H. - apply (Pos.le_trans _ (1 * n)). apply Pos.le_refl. - apply Pos.mul_le_mono_r. discriminate. exact H0. - - rewrite Qinv_plus_distr. unfold Qeq. reflexivity. -Qed. - Definition CReal_opp (x : CReal) : CReal. Proof. destruct x as [xn limx]. @@ -936,12 +734,12 @@ Proof. Qed. Lemma CReal_plus_assoc : forall (x y z : CReal), - CRealEq (CReal_plus (CReal_plus x y) z) - (CReal_plus x (CReal_plus y z)). + (x + y) + z == x + (y + z). Proof. intros. apply CRealEq_diff. intro n. destruct x as [xn limx], y as [yn limy], z as [zn limz]. unfold CReal_plus; unfold proj1_sig. + rewrite Qred_correct, Qred_correct, Qred_correct, Qred_correct. setoid_replace (xn (2 * (2 * n))%positive + yn (2 * (2 * n))%positive + zn (2 * n)%positive - (xn (2 * n)%positive + (yn (2 * (2 * n))%positive @@ -962,12 +760,12 @@ Lemma CReal_plus_comm : forall x y : CReal, x + y == y + x. Proof. intros [xn limx] [yn limy]. apply CRealEq_diff. intros. - unfold CReal_plus, proj1_sig. + unfold CReal_plus, proj1_sig. rewrite Qred_correct, Qred_correct. setoid_replace (xn (2 * n)%positive + yn (2 * n)%positive - (yn (2 * n)%positive + xn (2 * n)%positive))%Q with 0%Q. unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. - field. + ring. Qed. Lemma CReal_plus_0_l : forall r : CReal, @@ -976,7 +774,7 @@ Proof. intro r. split. - intros [n maj]. destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj. - rewrite Qplus_0_l in maj. + rewrite Qplus_0_l, Qred_correct in maj. specialize (q n n (Pos.mul 2 n) (Pos.le_refl _)). apply (Qlt_not_le (2#n) (xn n - xn (2 * n)%positive)). assumption. @@ -987,7 +785,7 @@ Proof. discriminate. discriminate. - intros [n maj]. destruct r as [xn q]; unfold CReal_plus, proj1_sig, inject_Q in maj. - rewrite Qplus_0_l in maj. + rewrite Qplus_0_l, Qred_correct in maj. specialize (q n n (Pos.mul 2 n) (Pos.le_refl _)). rewrite Qabs_Qminus in q. apply (Qlt_not_le (2#n) (xn (Pos.mul 2 n) - xn n)). @@ -1015,8 +813,9 @@ Proof. - proj1_sig (CReal_plus x y) n)%Q with (proj1_sig z (2 * n)%positive - proj1_sig y (2 * n)%positive)%Q. apply maj. apply belowMultiple. - simpl. destruct x as [xn limx], y as [yn limy], z as [zn limz]. - simpl; ring. + destruct x as [xn limx], y as [yn limy], z as [zn limz]; + unfold CReal_plus, proj1_sig. + rewrite Qred_correct, Qred_correct. ring. Qed. Lemma CReal_plus_lt_compat_r : @@ -1037,8 +836,9 @@ Proof. unfold Qle, Qnum, Qden. apply Z.mul_le_mono_nonneg_r. discriminate. discriminate. apply maj. - destruct x as [xn limx], y as [yn limy], z as [zn limz]. - simpl; ring. + destruct x as [xn limx], y as [yn limy], z as [zn limz]; + unfold CReal_plus, proj1_sig. + rewrite Qred_correct, Qred_correct. ring. Qed. Lemma CReal_plus_lt_reg_r : @@ -1090,9 +890,10 @@ Lemma CReal_plus_opp_r : forall x : CReal, Proof. intros [xn limx]. apply CRealEq_diff. intros. unfold CReal_plus, CReal_opp, inject_Q, proj1_sig. + rewrite Qred_correct. setoid_replace (xn (2 * n)%positive + - xn (2 * n)%positive - 0)%Q with 0%Q. - unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. field. + unfold Qle. simpl. unfold Z.le. intro absurd. inversion absurd. ring. Qed. Lemma CReal_plus_opp_l : forall x : CReal, @@ -1192,9 +993,11 @@ Lemma inject_Q_plus : forall q r : Q, inject_Q (q + r) == inject_Q q + inject_Q r. Proof. split. - - intros [n nmaj]. simpl in nmaj. + - intros [n nmaj]. unfold CReal_plus, inject_Q, proj1_sig in nmaj. + rewrite Qred_correct in nmaj. ring_simplify in nmaj. discriminate. - - intros [n nmaj]. simpl in nmaj. + - intros [n nmaj]. unfold CReal_plus, inject_Q, proj1_sig in nmaj. + rewrite Qred_correct in nmaj. ring_simplify in nmaj. discriminate. Qed. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index f3a59b493f..f4daedcb97 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -11,9 +11,7 @@ (* The multiplication and division of Cauchy reals. *) -Require Import QArith. -Require Import Qabs. -Require Import Qround. +Require Import QArith Qabs Qround. Require Import Logic.ConstructiveEpsilon. Require Export ConstructiveCauchyReals. Require CMorphisms. @@ -28,14 +26,15 @@ Definition QCauchySeq_bound (qn : positive -> Q) (cvmod : positive -> positive) | Z.neg p => p + 1 end. -Lemma QCauchySeq_bounded_prop (qn : positive -> Q) (cvmod : positive -> positive) - : QCauchySeq qn cvmod - -> forall n:positive, Pos.le (cvmod 1%positive) n - -> Qlt (Qabs (qn n)) (Z.pos (QCauchySeq_bound qn cvmod) # 1). +Lemma QCauchySeq_bounded_prop (qn : positive -> Q) + : QCauchySeq qn + -> forall n:positive, Qlt (Qabs (qn n)) (Z.pos (QCauchySeq_bound qn id) # 1). Proof. - intros H n H0. unfold QCauchySeq_bound. - specialize (H 1%positive (cvmod 1%positive) n (Pos.le_refl _) H0). - destruct (qn (cvmod 1%positive)) as [a b]. unfold Qnum. + intros H n. unfold QCauchySeq_bound. + assert (1 <= n)%positive as H0. { destruct n; discriminate. } + specialize (H 1%positive (1%positive) n (Pos.le_refl _) H0). + unfold id. + destruct (qn (1%positive)) as [a b]. unfold Qnum. rewrite Qabs_Qminus in H. apply (Qplus_lt_l _ _ (-Qabs (a#b))). apply (Qlt_le_trans _ 1). @@ -55,474 +54,405 @@ Proof. - apply H1. Qed. -Lemma CReal_mult_cauchy - : forall (xn yn zn : positive -> Q) (Ay Az : positive) (cvmod : positive -> positive), - QSeqEquiv xn yn cvmod - -> QCauchySeq zn id - -> (forall n:positive, Pos.le (cvmod 2%positive) n - -> Qlt (Qabs (yn n)) (Z.pos Ay # 1)) - -> (forall n:positive, Pos.le 1 n - -> Qlt (Qabs (zn n)) (Z.pos Az # 1)) - -> QSeqEquiv (fun n:positive => xn n * zn n) (fun n:positive => yn n * zn n) - (fun p => Pos.max (Pos.max (cvmod 2%positive) - (cvmod (2 * (Pos.max Ay Az) * p)%positive)) - (2 * (Pos.max Ay Az) * p)%positive). +Lemma factorDenom : forall (a:Z) (b d:positive), ((a # (d * b)) == (1#d) * (a#b))%Q. Proof. - intros xn yn zn Ay Az cvmod limx limz majy majz. - remember (Pos.mul 2 (Pos.max Ay Az)) as z. - intros k p q H H0. - setoid_replace (xn p * zn p - yn q * zn q)%Q - with ((xn p - yn q) * zn p + yn q * (zn p - zn q))%Q. + intros. unfold Qeq. simpl. destruct a; reflexivity. +Qed. + +Lemma CReal_mult_cauchy + : forall (x y : CReal) (A : positive), + (forall n : positive, (Qabs (proj1_sig x n) < Z.pos A # 1)%Q) + -> (forall n : positive, (Qabs (proj1_sig y n) < Z.pos A # 1)%Q) + -> QCauchySeq (fun n : positive => proj1_sig x (2 * A * n)%positive + * proj1_sig y (2 * A * n)%positive). +Proof. + intros [xn limx] [yn limy] A. unfold proj1_sig. + intros majx majy k p q H H0. + setoid_replace (xn (2*A*p)%positive * yn (2*A*p)%positive + - xn (2*A*q)%positive * yn (2*A*q)%positive)%Q + with ((xn (2*A*p)%positive - xn (2*A*q)%positive) * yn (2*A*p)%positive + + xn (2*A*q)%positive * (yn (2*A*p)%positive - yn (2*A*q)%positive))%Q. 2: ring. - apply (Qle_lt_trans _ (Qabs ((xn p - yn q) * zn p) - + Qabs (yn q * (zn p - zn q)))). - apply Qabs_triangle. rewrite Qabs_Qmult. rewrite Qabs_Qmult. + apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)). + rewrite Qabs_Qmult, Qabs_Qmult. setoid_replace (1#k)%Q with ((1#2*k) + (1#2*k))%Q. + 2: rewrite Qinv_plus_distr; reflexivity. apply Qplus_lt_le_compat. - - apply (Qle_lt_trans _ ((1#z * k) * Qabs (zn p)%nat)). - + apply Qmult_le_compat_r. apply Qle_lteq. left. apply limx. - apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) (z * k))). - apply Pos.le_max_l. refine (Pos.le_trans _ _ _ _ H). - rewrite <- Pos.max_assoc. apply Pos.le_max_r. - apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) (z * k))). - apply Pos.le_max_l. refine (Pos.le_trans _ _ _ _ H0). - rewrite <- Pos.max_assoc. apply Pos.le_max_r. apply Qabs_nonneg. - + subst z. rewrite <- (Qmult_1_r (1 # 2 * k)). + - apply (Qle_lt_trans _ ((1#2*A * k) * Qabs (yn (2*A*p)%positive))). + + apply Qmult_le_compat_r. apply Qlt_le_weak. apply limx. + apply Pos.mul_le_mono_l, H. apply Pos.mul_le_mono_l, H0. + apply Qabs_nonneg. + + rewrite <- (Qmult_1_r (1 # 2 * k)). rewrite <- Pos.mul_assoc. rewrite <- (Pos.mul_comm k). rewrite Pos.mul_assoc. rewrite (factorDenom _ _ (2 * k)). rewrite <- Qmult_assoc. apply Qmult_lt_l. reflexivity. - apply (Qle_lt_trans _ (Qabs (zn p)%nat * (1 # Az))). - rewrite <- (Qmult_comm (1 # Az)). apply Qmult_le_compat_r. - unfold Qle. simpl. rewrite Pos2Z.inj_max. apply Z.le_max_r. - apply Qabs_nonneg. rewrite <- (Qmult_inv_r (1#Az)). + apply (Qle_lt_trans _ (Qabs (yn (2 * A * p)%positive) * (1 # A))). + rewrite <- (Qmult_comm (1 # A)). apply Qmult_le_compat_r. + unfold Qle. simpl. apply Z.le_refl. + apply Qabs_nonneg. rewrite <- (Qmult_inv_r (1#A)). 2: intro abs; inversion abs. rewrite Qmult_comm. apply Qmult_lt_l. reflexivity. - setoid_replace (/(1#Az))%Q with (Z.pos Az # 1)%Q. + setoid_replace (/(1#A))%Q with (Z.pos A # 1)%Q. 2: reflexivity. - apply majz. refine (Pos.le_trans _ _ _ _ H). - apply (Pos.le_trans _ (2 * Pos.max Ay Az * k)). - discriminate. apply Pos.le_max_r. - - apply (Qle_trans _ ((1 # z * k) * Qabs (yn q)%nat)). - + rewrite Qmult_comm. apply Qmult_le_compat_r. apply Qle_lteq. - left. apply limz. - apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) - (z * k)%positive)). - apply Pos.le_max_r. refine (Pos.le_trans _ _ _ _ H). - rewrite <- Pos.max_assoc. apply Pos.le_max_r. - apply (Pos.le_trans _ (Pos.max (cvmod (z * k)%positive) - (z * k)%positive)). - apply Pos.le_max_r. refine (Pos.le_trans _ _ _ _ H0). - rewrite <- Pos.max_assoc. apply Pos.le_max_r. + apply majy. + - apply (Qle_trans _ ((1 # 2 * A * k) * Qabs (xn (2*A*q)%positive))). + + rewrite Qmult_comm. apply Qmult_le_compat_r. + apply Qlt_le_weak. apply limy. + apply Pos.mul_le_mono_l, H. apply Pos.mul_le_mono_l, H0. apply Qabs_nonneg. - + subst z. rewrite <- (Qmult_1_r (1 # 2 * k)). + + rewrite <- (Qmult_1_r (1 # 2 * k)). rewrite <- Pos.mul_assoc. rewrite <- (Pos.mul_comm k). rewrite Pos.mul_assoc. rewrite (factorDenom _ _ (2 * k)). rewrite <- Qmult_assoc. - apply Qle_lteq. left. - apply Qmult_lt_l. unfold Qlt. simpl. unfold Z.lt. auto. - apply (Qle_lt_trans _ (Qabs (yn q)%nat * (1 # Ay))). - rewrite <- (Qmult_comm (1 # Ay)). apply Qmult_le_compat_r. - unfold Qle. simpl. rewrite Pos2Z.inj_max. apply Z.le_max_l. - apply Qabs_nonneg. rewrite <- (Qmult_inv_r (1#Ay)). + apply Qlt_le_weak. + apply Qmult_lt_l. reflexivity. + apply (Qle_lt_trans _ (Qabs (xn (2 * A * q)%positive) * (1 # A))). + rewrite <- (Qmult_comm (1 # A)). apply Qmult_le_compat_r. + apply Qle_refl. + apply Qabs_nonneg. rewrite <- (Qmult_inv_r (1#A)). 2: intro abs; inversion abs. rewrite Qmult_comm. apply Qmult_lt_l. reflexivity. - setoid_replace (/(1#Ay))%Q with (Z.pos Ay # 1)%Q. 2: reflexivity. - apply majy. refine (Pos.le_trans _ _ _ _ H0). - rewrite <- Pos.max_assoc. apply Pos.le_max_l. - - rewrite Qinv_plus_distr. unfold Qeq. reflexivity. -Qed. - -Lemma linear_max : forall (p Ax Ay i : positive), - Pos.le p i - -> (Pos.max (Pos.max 2 (2 * Pos.max Ax Ay * p)) - (2 * Pos.max Ax Ay * p) - <= (2 * Pos.max Ax Ay) * i)%positive. -Proof. - intros. rewrite Pos.max_l. 2: apply Pos.le_max_r. rewrite Pos.max_r. - apply Pos.mul_le_mono_l. exact H. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2). - destruct (Pos.max Ax Ay * p)%positive; discriminate. + setoid_replace (/(1#A))%Q with (Z.pos A # 1)%Q. 2: reflexivity. + apply majx. Qed. Definition CReal_mult (x y : CReal) : CReal. Proof. - destruct x as [xn limx]. destruct y as [yn limy]. - pose (QCauchySeq_bound xn id) as Ax. - pose (QCauchySeq_bound yn id) as Ay. - exists (fun n : positive => xn ((2 * Pos.max Ax Ay) * n)%positive - * yn ((2 * Pos.max Ax Ay) * n)%positive). - intros p n k H0 H1. - apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). - intros. apply (QCauchySeq_bounded_prop xn id limx). - apply (Pos.le_trans _ 2). discriminate. exact H. - intros. exact (QCauchySeq_bounded_prop yn id limy _ H). - apply linear_max; assumption. apply linear_max; assumption. + exists (fun n : positive => proj1_sig x ((2 * Pos.max (QCauchySeq_bound (proj1_sig x) id) (QCauchySeq_bound (proj1_sig y) id)) * n)%positive + * proj1_sig y ((2 * Pos.max (QCauchySeq_bound (proj1_sig x) id) + (QCauchySeq_bound (proj1_sig y) id)) * n)%positive). + apply (CReal_mult_cauchy x y). + - intro n. destruct x as [xn caux]. unfold proj1_sig. + pose proof (QCauchySeq_bounded_prop xn caux). + apply (Qlt_le_trans _ (Z.pos (QCauchySeq_bound xn id) # 1)). + apply H. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + rewrite Pos2Z.inj_max. apply Z.le_max_l. + - intro n. destruct y as [yn cauy]. unfold proj1_sig. + pose proof (QCauchySeq_bounded_prop yn cauy). + apply (Qlt_le_trans _ (Z.pos (QCauchySeq_bound yn id) # 1)). + apply H. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + rewrite Pos2Z.inj_max. apply Z.le_max_r. Defined. Infix "*" := CReal_mult : CReal_scope. -Lemma CReal_mult_unfold : forall x y : CReal, - QSeqEquivEx (proj1_sig (CReal_mult x y)) - (fun n : positive => proj1_sig x n * proj1_sig y n)%Q. +Lemma CReal_mult_comm : forall x y : CReal, x * y == y * x. Proof. - intros [xn limx] [yn limy]. unfold CReal_mult ; simpl. - pose proof (QCauchySeq_bounded_prop xn id limx) as majx. - pose proof (QCauchySeq_bounded_prop yn id limy) as majy. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound yn id) as Ay. - exists (fun p : positive => - Pos.max (2 * Pos.max Ax Ay * p) - (2 * Pos.max Ax Ay * p)). - intros p n k H0 H1. rewrite Pos.max_l in H0, H1. - apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). - 2: apply majy. intros. apply majx. - refine (Pos.le_trans _ _ _ _ H). discriminate. - 3: apply Pos.le_refl. 3: apply Pos.le_refl. - apply linear_max. refine (Pos.le_trans _ _ _ _ H0). - apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. - apply Pos.mul_le_mono_r. discriminate. - rewrite Pos.max_l. - rewrite Pos.max_r. apply H1. 2: apply Pos.le_max_r. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. unfold id. - rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). - destruct (Pos.max Ax Ay * p)%positive; discriminate. + assert (forall x y : CReal, x * y <= y * x) as H. + { intros x y [n nmaj]. apply (Qlt_not_le _ _ nmaj). clear nmaj. + unfold CReal_mult, proj1_sig. + destruct x as [xn limx], y as [yn limy]. + rewrite Pos.max_comm, Qmult_comm. ring_simplify. discriminate. } + split; apply H. Qed. -Lemma CReal_mult_assoc_bounded_r : forall (xn yn zn : positive -> Q), - QSeqEquivEx xn yn (* both are Cauchy with same limit *) - -> QSeqEquiv zn zn id - -> QSeqEquivEx (fun n => xn n * zn n)%Q (fun n => yn n * zn n)%Q. -Proof. - intros xn yn zn [cvmod cveq] H0. - exists (fun p => Pos.max (Pos.max (cvmod 2%positive) (cvmod (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn id)) * p)%positive)) - (2 * (Pos.max (QCauchySeq_bound yn (fun k : positive => cvmod (2 * k)%positive)) (QCauchySeq_bound zn id)) * p)%positive). - apply (CReal_mult_cauchy _ _ _ _ _ _ cveq H0). - exact (QCauchySeq_bounded_prop - yn (fun k => cvmod (2 * k)%positive) - (QSeqEquiv_cau_r xn yn cvmod cveq)). - exact (QCauchySeq_bounded_prop zn id H0). +Lemma CReal_mult_proper_0_l : forall x y : CReal, + y == 0 -> x * y == 0. +Proof. + assert (forall a:Q, a-0 == a)%Q as Qmin0. + { intros. ring. } + intros. apply CRealEq_diff. intros n. + destruct x as [xn limx], y as [yn limy]. + unfold CReal_mult, proj1_sig, inject_Q. + rewrite CRealEq_diff in H; unfold proj1_sig, inject_Q in H. + specialize (H (2 * Pos.max (QCauchySeq_bound xn id) + (QCauchySeq_bound yn id) * n))%positive. + rewrite Qmin0 in H. rewrite Qmin0, Qabs_Qmult, Qmult_comm. + apply (Qle_trans + _ ((2 # (2 * Pos.max (QCauchySeq_bound xn id) (QCauchySeq_bound yn id) * n)%positive) * + (Qabs (xn (2 * Pos.max (QCauchySeq_bound xn id) (QCauchySeq_bound yn id) * n)%positive) ))). + apply Qmult_le_compat_r. + 2: apply Qabs_nonneg. exact H. clear H. rewrite Qmult_comm. + apply (Qle_trans _ ((Z.pos (QCauchySeq_bound xn id) # 1) + * (2 # (2 * Pos.max (QCauchySeq_bound xn id) (QCauchySeq_bound yn id) * n)%positive))). + apply Qmult_le_compat_r. + apply Qlt_le_weak, (QCauchySeq_bounded_prop xn limx). + discriminate. + unfold Qle, Qmult, Qnum, Qden. + rewrite Pos.mul_1_l. rewrite <- (Z.mul_comm 2), <- Z.mul_assoc. + apply Z.mul_le_mono_nonneg_l. discriminate. + rewrite <- Pos2Z.inj_mul. apply Pos2Z.pos_le_pos, Pos.mul_le_mono_r. + apply (Pos.le_trans _ (2 * QCauchySeq_bound xn id)). + apply (Pos.le_trans _ (1 * QCauchySeq_bound xn id)). + apply Pos.le_refl. apply Pos.mul_le_mono_r. discriminate. + apply Pos.mul_le_mono_l. apply Pos.le_max_l. Qed. -Lemma CReal_mult_assoc : forall x y z : CReal, (x * y) * z == x * (y * z). +Lemma CReal_mult_0_r : forall r, r * 0 == 0. Proof. - intros. apply CRealEq_diff. apply CRealEq_modindep. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n * proj1_sig y n * proj1_sig z n)%Q). - - apply (QSeqEquivEx_trans _ (fun n => proj1_sig (CReal_mult x y) n * proj1_sig z n)%Q). - apply CReal_mult_unfold. - destruct x as [xn limx], y as [yn limy], z as [zn limz]; unfold CReal_mult; simpl. - pose proof (QCauchySeq_bounded_prop xn id limx) as majx. - pose proof (QCauchySeq_bounded_prop yn id limy) as majy. - pose proof (QCauchySeq_bounded_prop zn id limz) as majz. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound yn id) as Ay. - remember (QCauchySeq_bound zn id) as Az. - apply CReal_mult_assoc_bounded_r. 2: exact limz. - exists (fun p : positive => - Pos.max (2 * Pos.max Ax Ay * p) - (2 * Pos.max Ax Ay * p)). - intros p n k H0 H1. - apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). - 2: exact majy. intros. apply majx. refine (Pos.le_trans _ _ _ _ H). - discriminate. rewrite Pos.max_l in H0, H1. - 2: apply Pos.le_refl. 2: apply Pos.le_refl. - apply linear_max. - apply (Pos.le_trans _ (2 * Pos.max Ax Ay * p)). - apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. - apply Pos.mul_le_mono_r. discriminate. - exact H0. rewrite Pos.max_l. 2: apply Pos.le_max_r. - rewrite Pos.max_r in H1. 2: apply Pos.le_refl. - refine (Pos.le_trans _ _ _ _ H1). rewrite Pos.max_r. - apply Pos.le_refl. apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - unfold id. - rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). - destruct (Pos.max Ax Ay * p)%positive; discriminate. - - apply (QSeqEquivEx_trans - _ (fun n => proj1_sig x n * proj1_sig (CReal_mult y z) n)%Q). - 2: apply QSeqEquivEx_sym; apply CReal_mult_unfold. - destruct x as [xn limx], y as [yn limy], z as [zn limz]; unfold CReal_mult; simpl. - pose proof (QCauchySeq_bounded_prop xn id limx) as majx. - pose proof (QCauchySeq_bounded_prop yn id limy) as majy. - pose proof (QCauchySeq_bounded_prop zn id limz) as majz. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound yn id) as Ay. - remember (QCauchySeq_bound zn id) as Az. - pose proof (CReal_mult_assoc_bounded_r (fun n0 : positive => yn n0 * zn n0)%Q (fun n : positive => - yn ((Pos.max Ay Az)~0 * n)%positive - * zn ((Pos.max Ay Az)~0 * n)%positive)%Q xn) - as [cvmod cveq]. - + exists (fun p : positive => - Pos.max (2 * Pos.max Ay Az * p) - (2 * Pos.max Ay Az * p)). - intros p n k H0 H1. rewrite Pos.max_l in H0, H1. - apply (CReal_mult_cauchy yn yn zn Ay Az id limy limz). - 2: exact majz. intros. apply majy. refine (Pos.le_trans _ _ _ _ H). - discriminate. - 3: apply Pos.le_refl. 3: apply Pos.le_refl. - rewrite Pos.max_l. rewrite Pos.max_r. apply H0. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. unfold id. - rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). - destruct (Pos.max Ay Az * p)%positive; discriminate. - apply Pos.le_max_r. - apply linear_max. refine (Pos.le_trans _ _ _ _ H1). - apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. - apply Pos.mul_le_mono_r. discriminate. - + exact limx. - + exists cvmod. intros p k n H1 H2. specialize (cveq p k n H1 H2). - setoid_replace (xn k * yn k * zn k - - xn n * - (yn ((Pos.max Ay Az)~0 * n)%positive * - zn ((Pos.max Ay Az)~0 * n)%positive))%Q - with ((fun n : positive => yn n * zn n * xn n) k - - (fun n : positive => - yn ((Pos.max Ay Az)~0 * n)%positive * - zn ((Pos.max Ay Az)~0 * n)%positive * - xn n) n)%Q. - apply cveq. ring. + intros. apply CReal_mult_proper_0_l. reflexivity. Qed. -Lemma CReal_mult_comm : forall x y : CReal, x * y == y * x. +Lemma CReal_mult_0_l : forall r, 0 * r == 0. Proof. - intros. apply CRealEq_diff. apply CRealEq_modindep. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig y n * proj1_sig x n)%Q). - destruct x as [xn limx], y as [yn limy]; simpl. - 2: apply QSeqEquivEx_sym; apply CReal_mult_unfold. - pose proof (QCauchySeq_bounded_prop xn id limx) as majx. - pose proof (QCauchySeq_bounded_prop yn id limy) as majy. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound yn id) as Ay. - apply QSeqEquivEx_sym. - exists (fun p : positive => - Pos.max (2 * Pos.max Ay Ax * p) - (2 * Pos.max Ay Ax * p)). - intros p n k H0 H1. rewrite Pos.max_l in H0, H1. - 2: apply Pos.le_refl. 2: apply Pos.le_refl. - rewrite (Qmult_comm (xn ((Pos.max Ax Ay)~0 * k)%positive)). - apply (CReal_mult_cauchy yn yn xn Ay Ax id limy limx). - 2: exact majx. intros. apply majy. refine (Pos.le_trans _ _ _ _ H). - discriminate. - rewrite Pos.max_l. rewrite Pos.max_r. apply H0. - unfold id. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - rewrite <- Pos.mul_assoc, <- (Pos.mul_le_mono_l 2 1). - destruct (Pos.max Ay Ax * p)%positive; discriminate. - apply Pos.le_max_r. rewrite (Pos.max_comm Ax Ay). - apply linear_max. refine (Pos.le_trans _ _ _ _ H1). - apply (Pos.le_trans _ (1*p)). apply Pos.le_refl. - apply Pos.mul_le_mono_r. discriminate. + intros. rewrite CReal_mult_comm. apply CReal_mult_0_r. Qed. -Lemma CReal_mult_proper_l : forall x y z : CReal, - y == z -> x * y == x * z. -Proof. - intros. apply CRealEq_diff. apply CRealEq_modindep. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n * proj1_sig y n)%Q). - apply CReal_mult_unfold. - rewrite CRealEq_diff in H. rewrite <- CRealEq_modindep in H. - apply QSeqEquivEx_sym. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n * proj1_sig z n)%Q). - apply CReal_mult_unfold. - destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl. - destruct H as [cvmod H]. simpl in H. - pose proof (QCauchySeq_bounded_prop xn id limx) as majx. - pose proof (QCauchySeq_bounded_prop - zn (fun k => cvmod (2 * k)%positive) - (QSeqEquiv_cau_r yn zn cvmod H)) as majz. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound zn (fun k => cvmod (2 * k)%positive)) as Az. - apply QSeqEquivEx_sym. - exists (fun p : positive => - Pos.max (Pos.max (cvmod (2%positive)) (cvmod (2 * Pos.max Az Ax * p)%positive)) - (2 * Pos.max Az Ax * p)). - intros p n k H1 H2. - setoid_replace (xn n * yn n - xn k * zn k)%Q - with (yn n * xn n - zn k * xn k)%Q. 2: ring. - apply (CReal_mult_cauchy yn zn xn Az Ax cvmod H limx majz majx). - exact H1. exact H2. +Lemma CRealLt_0_aboveSig : forall (x : CReal) (n : positive), + Qlt (2 # n) (proj1_sig x n) + -> forall p:positive, + Pos.le n p -> Qlt (1 # n) (proj1_sig x p). +Proof. + intros. destruct x as [xn caux]. + unfold proj1_sig. unfold proj1_sig in H. + specialize (caux n n p (Pos.le_refl n) H0). + apply (Qplus_lt_l _ _ (xn n-xn p)). + apply (Qlt_trans _ ((1#n) + (1#n))). + apply Qplus_lt_r. exact (Qle_lt_trans _ _ _ (Qle_Qabs _) caux). + rewrite Qinv_plus_distr. ring_simplify. exact H. Qed. -Lemma CReal_mult_lt_0_compat : forall x y : CReal, - inject_Q 0 < x - -> inject_Q 0 < y - -> inject_Q 0 < x * y. +(* Correctness lemma for the Definition CReal_mult_lt_0_compat below. *) +Lemma CReal_mult_lt_0_compat_correct + : forall (x y : CReal) (H : 0 < x) (H0 : 0 < y), + (2 # 2 * proj1_sig H * proj1_sig H0 < + proj1_sig (x * y)%CReal (2 * proj1_sig H * proj1_sig H0)%positive - + proj1_sig (inject_Q 0) (2 * proj1_sig H * proj1_sig H0)%positive)%Q. Proof. - intros. destruct H as [x0 H], H0 as [x1 H0]. - pose proof (CRealLt_aboveSig (inject_Q 0) x x0 H). - pose proof (CRealLt_aboveSig (inject_Q 0) y x1 H0). + intros. + destruct H as [x0 H], H0 as [x1 H0]. unfold proj1_sig. + unfold inject_Q, proj1_sig, Qminus in H. rewrite Qplus_0_r in H. + pose proof (CRealLt_0_aboveSig x x0 H) as H1. + unfold inject_Q, proj1_sig, Qminus in H0. rewrite Qplus_0_r in H0. + pose proof (CRealLt_0_aboveSig y x1 H0) as H2. destruct x as [xn limx], y as [yn limy]; simpl in H, H1, H2, H0. - pose proof (QCauchySeq_bounded_prop xn id limx) as majx. - pose proof (QCauchySeq_bounded_prop yn id limy) as majy. - destruct (Qarchimedean (/ (xn x0 - 0 - (2 # x0)))). - destruct (Qarchimedean (/ (yn x1 - 0 - (2 # x1)))). - exists (Pos.max x0 x~0 * Pos.max x1 x2~0)%positive. - simpl. + unfold CReal_mult, inject_Q, proj1_sig. remember (QCauchySeq_bound xn id) as Ax. remember (QCauchySeq_bound yn id) as Ay. unfold Qminus. rewrite Qplus_0_r. - unfold Qminus in H1, H2. - specialize (H1 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive). - assert (Pos.max x1 x2~0 <= (Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive. - { rewrite Pos.mul_assoc. - rewrite <- (Pos.mul_1_l (Pos.max x1 x2~0)). - rewrite Pos.mul_assoc. apply Pos.mul_le_mono_r. discriminate. } - specialize (H2 ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive H3). - rewrite Qplus_0_r in H1, H2. - apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (2 # Pos.max x1 x2~0))). - unfold Qlt; simpl. assert (forall p : positive, (Z.pos p < Z.pos p~0)%Z). - intro p. rewrite <- (Z.mul_1_l (Z.pos p)). - replace (Z.pos p~0) with (2 * Z.pos p)%Z. apply Z.mul_lt_mono_pos_r. - apply Pos2Z.is_pos. reflexivity. reflexivity. - apply H4. - apply (Qlt_trans _ ((2 # Pos.max x0 x~0) * (yn ((Pos.max Ax Ay)~0 * (Pos.max x0 x~0 * Pos.max x1 x2~0))%positive))). - apply Qmult_lt_l. reflexivity. apply H2. apply Qmult_lt_r. - apply (Qlt_trans 0 (2 # Pos.max x1 x2~0)). reflexivity. apply H2. - apply H1. rewrite Pos.mul_comm. apply Pos2Nat.inj_le. - rewrite <- Pos.mul_assoc. rewrite Pos2Nat.inj_mul. - rewrite <- (mult_1_r (Pos.to_nat (Pos.max x0 x~0))). - rewrite <- mult_assoc. apply Nat.mul_le_mono_nonneg. - apply le_0_n. apply le_refl. auto. - rewrite mult_1_l. apply Pos2Nat.is_pos. + specialize (H2 (2 * (Pos.max Ax Ay) * (2 * x0 * x1))%positive). + setoid_replace (2 # 2 * x0 * x1)%Q with ((1#x0) * (1#x1))%Q. + assert (x0 <= 2 * Pos.max Ax Ay * (2 * x0 * x1))%positive. + { apply (Pos.le_trans _ (2 * Pos.max Ax Ay * x0)). + apply belowMultiple. apply Pos.mul_le_mono_l. + rewrite (Pos.mul_comm 2 x0), <- Pos.mul_assoc, Pos.mul_comm. + apply belowMultiple. } + apply (Qlt_trans _ (xn (2 * Pos.max Ax Ay * (2 * x0 * x1))%positive * (1#x1))). + - apply Qmult_lt_compat_r. reflexivity. apply H1, H3. + - apply Qmult_lt_l. + apply (Qlt_trans _ (1#x0)). reflexivity. apply H1, H3. + apply H2. apply (Pos.le_trans _ (2 * Pos.max Ax Ay * x1)). + apply belowMultiple. apply Pos.mul_le_mono_l. apply belowMultiple. + - unfold Qeq, Qmult, Qnum, Qden. + rewrite Z.mul_1_l, <- Pos2Z.inj_mul. reflexivity. +Qed. + +(* Strict inequality on CReal is in sort Type, for example + used in the computation of division. *) +Definition CReal_mult_lt_0_compat : forall x y : CReal, + 0 < x -> 0 < y -> 0 < x * y + := fun x y H H0 => exist _ (2 * proj1_sig H * proj1_sig H0)%positive + (CReal_mult_lt_0_compat_correct + x y H H0). + +Lemma CReal_mult_bound_indep + : forall (x y : CReal) (A : positive) + (xbound : forall n : positive, (Qabs (proj1_sig x n) < Z.pos A # 1)%Q) + (ybound : forall n : positive, (Qabs (proj1_sig y n) < Z.pos A # 1)%Q), + x * y == exist _ + (fun n : positive => proj1_sig x (2 * A * n)%positive + * proj1_sig y (2 * A * n)%positive)%Q + (CReal_mult_cauchy x y A xbound ybound). +Proof. + intros. apply CRealEq_diff. + pose proof (CReal_mult_cauchy x y) as xycau. intro n. + destruct x as [xn caux], y as [yn cauy]; + unfold CReal_mult, CReal_plus, proj1_sig; unfold proj1_sig in xycau. + pose proof (xycau A xbound ybound). + remember (QCauchySeq_bound xn id) as Ax. + remember (QCauchySeq_bound yn id) as Ay. + remember (Pos.max Ax Ay) as B. + setoid_replace (xn (2*B*n)%positive * yn (2*B*n)%positive + - xn (2*A*n)%positive * yn (2*A*n)%positive)%Q + with ((xn (2*B*n)%positive - xn (2*A*n)%positive) * yn (2*B*n)%positive + + xn (2*A*n)%positive * (yn (2*B*n)%positive - yn (2*A*n)%positive))%Q. + 2: ring. + apply (Qle_trans _ _ _ (Qabs_triangle _ _)). + rewrite Qabs_Qmult, Qabs_Qmult. + setoid_replace (2#n)%Q with ((1#n) + (1#n))%Q. + 2: rewrite Qinv_plus_distr; reflexivity. + apply Qplus_le_compat. + - apply (Qle_trans _ ((1#2*Pos.min A B * n) * Qabs (yn (2*B*n)%positive))). + + apply Qmult_le_compat_r. apply Qlt_le_weak. apply caux. + apply Pos.mul_le_mono_r, Pos.mul_le_mono_l, Pos.le_min_r. + apply Pos.mul_le_mono_r, Pos.mul_le_mono_l, Pos.le_min_l. + apply Qabs_nonneg. + + unfold proj1_sig in ybound. clear xbound. + apply (Qmult_le_l _ _ (Z.pos (2*Pos.min A B *n) # 1)). + reflexivity. rewrite Qmult_assoc. + setoid_replace ((Z.pos (2 * Pos.min A B * n) # 1) * (1 # 2 * Pos.min A B * n))%Q + with 1%Q. + rewrite Qmult_1_l. + setoid_replace ((Z.pos (2 * Pos.min A B * n) # 1) * (1 # n))%Q + with (Z.pos (2 * Pos.min A B) # 1)%Q. + apply (Qle_trans _ (Z.pos (Pos.min A B) # 1)). + destruct (Pos.lt_total A B). rewrite Pos.min_l. + apply Qlt_le_weak, ybound. apply Pos.lt_le_incl, H0. + destruct H0. rewrite Pos.min_l. + apply Qlt_le_weak, ybound. rewrite H0. apply Pos.le_refl. + rewrite Pos.min_r. subst B. apply (Qle_trans _ (Z.pos Ay #1)). subst Ay. + apply Qlt_le_weak, (QCauchySeq_bounded_prop yn cauy). + unfold Qle, Qnum, Qden. + rewrite Z.mul_1_r, Z.mul_1_r, Pos2Z.inj_max. apply Z.le_max_r. + apply Pos.lt_le_incl, H0. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply belowMultiple. + unfold Qeq, Qmult, Qnum, Qden. + rewrite Z.mul_1_r, Z.mul_1_r, Pos2Z.inj_mul. reflexivity. + unfold Qeq, Qmult, Qnum, Qden. + rewrite Z.mul_1_r, Z.mul_1_r, Pos2Z.inj_mul. reflexivity. + - rewrite Qmult_comm. + apply (Qle_trans _ ((1#2*Pos.min A B * n) * Qabs (xn (2*A*n)%positive))). + + apply Qmult_le_compat_r. apply Qlt_le_weak. apply cauy. + apply Pos.mul_le_mono_r, Pos.mul_le_mono_l, Pos.le_min_r. + apply Pos.mul_le_mono_r, Pos.mul_le_mono_l, Pos.le_min_l. + apply Qabs_nonneg. + + unfold proj1_sig in xbound. clear ybound. + apply (Qmult_le_l _ _ (Z.pos (2*Pos.min A B *n) # 1)). + reflexivity. rewrite Qmult_assoc. + setoid_replace ((Z.pos (2 * Pos.min A B * n) # 1) * (1 # 2 * Pos.min A B * n))%Q + with 1%Q. + rewrite Qmult_1_l. + setoid_replace ((Z.pos (2 * Pos.min A B * n) # 1) * (1 # n))%Q + with (Z.pos (2 * Pos.min A B) # 1)%Q. + apply (Qle_trans _ (Z.pos (Pos.min A B) # 1)). + destruct (Pos.lt_total A B). rewrite Pos.min_l. + apply Qlt_le_weak, xbound. apply Pos.lt_le_incl, H0. + destruct H0. rewrite Pos.min_l. + apply Qlt_le_weak, xbound. rewrite H0. apply Pos.le_refl. + rewrite Pos.min_r. subst B. apply (Qle_trans _ (Z.pos Ax #1)). subst Ax. + apply Qlt_le_weak, (QCauchySeq_bounded_prop xn caux). + unfold Qle, Qnum, Qden. + rewrite Z.mul_1_r, Z.mul_1_r, Pos2Z.inj_max. apply Z.le_max_l. + apply Pos.lt_le_incl, H0. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply belowMultiple. + unfold Qeq, Qmult, Qnum, Qden. + rewrite Z.mul_1_r, Z.mul_1_r, Pos2Z.inj_mul. reflexivity. + unfold Qeq, Qmult, Qnum, Qden. + rewrite Z.mul_1_r, Z.mul_1_r, Pos2Z.inj_mul. reflexivity. Qed. Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal, r1 * (r2 + r3) == (r1 * r2) + (r1 * r3). Proof. - intros x y z. apply CRealEq_diff. apply CRealEq_modindep. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n - * (proj1_sig (CReal_plus y z) n))%Q). - apply CReal_mult_unfold. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig (CReal_mult x y) n - + proj1_sig (CReal_mult x z) n))%Q. - 2: apply QSeqEquivEx_sym; exists (fun p:positive => 2 * p)%positive - ; apply CReal_plus_unfold. - apply (QSeqEquivEx_trans _ (fun n => proj1_sig x n - * (proj1_sig y n + proj1_sig z n))%Q). - - pose proof (CReal_plus_unfold y z). - destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl; simpl in H. - pose proof (QCauchySeq_bounded_prop xn id) as majx. - pose proof (QCauchySeq_bounded_prop yn id) as majy. - pose proof (QCauchySeq_bounded_prop zn id) as majz. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound yn id) as Ay. - remember (QCauchySeq_bound zn id) as Az. - pose proof (CReal_mult_cauchy (fun n => yn (n~0)%positive + zn (n~0)%positive)%Q - (fun n => yn n + zn n)%Q - xn (Ay + Az) Ax - (fun p:positive => 2 * p)%positive H limx). - exists (fun p : positive => (2 * (2 * Pos.max (Ay + Az) Ax * p))%positive). - intros p n k H1 H2. - setoid_replace (xn n * (yn (n~0)%positive + zn (n~0)%positive) - xn k * (yn k + zn k))%Q - with ((yn (n~0)%positive + zn (n~0)%positive) * xn n - (yn k + zn k) * xn k)%Q. - 2: ring. - assert ((2 * Pos.max (Ay + Az) Ax * p) <= - 2 * (2 * Pos.max (Ay + Az) Ax * p))%positive. - { rewrite <- Pos.mul_assoc. - apply Pos.mul_le_mono_l. - apply (Pos.le_trans _ (1*(Pos.max (Ay + Az) Ax * p))). - apply Pos.le_refl. apply Pos.mul_le_mono_r. discriminate. } - apply H0. intros n0 H4. + (* Use same bound, max of the 3 bounds for every product. *) + intros x y z. + remember (QCauchySeq_bound (proj1_sig x) id) as Ax. + remember (QCauchySeq_bound (proj1_sig y) id) as Ay. + remember (QCauchySeq_bound (proj1_sig z) id) as Az. + pose (Pos.max Ax (Pos.add Ay Az)) as B. + assert (forall n : positive, (Qabs (proj1_sig x n) < Z.pos B # 1)%Q) as xbound. + { intro n. subst B. apply (Qlt_le_trans _ (Z.pos Ax #1)). + rewrite HeqAx. + apply (QCauchySeq_bounded_prop (proj1_sig x)). + destruct x. exact q. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply Pos.le_max_l. } + assert (forall n : positive, (Qlt (Qabs (proj1_sig (y+z) n)) (Z.pos B # 1))) + as sumbound. + { intro n. destruct y as [yn cauy], z as [zn cauz]. + unfold CReal_plus, proj1_sig. rewrite Qred_correct. + subst B. apply (Qlt_le_trans _ ((Z.pos Ay#1) + (Z.pos Az#1))). apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)). - rewrite Pos2Z.inj_add, <- Qinv_plus_distr. apply Qplus_lt_le_compat. - apply majy. exact limy. - refine (Pos.le_trans _ _ _ _ H4); discriminate. - apply Qlt_le_weak. apply majz. exact limz. - refine (Pos.le_trans _ _ _ _ H4); discriminate. - apply majx. exact limx. refine (Pos.le_trans _ _ _ _ H1). - rewrite Pos.max_l. rewrite Pos.max_r. apply Pos.le_refl. - rewrite <- (Pos.mul_le_mono_l 2). - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - destruct (Pos.max (Ay + Az) Ax * p)%positive; discriminate. - apply (Pos.le_trans _ (2 * (2 * Pos.max (Ay + Az) Ax * p))). - 2: apply Pos.le_max_r. - rewrite <- Pos.mul_assoc. rewrite (Pos.mul_assoc 2 2). - rewrite <- Pos.mul_le_mono_r. discriminate. - refine (Pos.le_trans _ _ _ _ H2). rewrite <- Pos.max_comm. - rewrite Pos.max_assoc. rewrite Pos.max_r. apply Pos.le_refl. - apply Pos.max_lub. apply H3. - rewrite <- Pos.mul_le_mono_l. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - destruct (Pos.max (Ay + Az) Ax * p)%positive; discriminate. - - destruct x as [xn limx], y as [yn limy], z as [zn limz]; simpl. - pose proof (QCauchySeq_bounded_prop xn id) as majx. - pose proof (QCauchySeq_bounded_prop yn id) as majy. - pose proof (QCauchySeq_bounded_prop zn id) as majz. - remember (QCauchySeq_bound xn id) as Ax. - remember (QCauchySeq_bound yn id) as Ay. - remember (QCauchySeq_bound zn id) as Az. - exists (fun p : positive => (2 * (Pos.max (Pos.max Ax Ay) Az) * (2 * p))%positive). - intros p n k H H0. - setoid_replace (xn n * (yn n + zn n) - - (xn ((Pos.max Ax Ay)~0 * k)%positive * - yn ((Pos.max Ax Ay)~0 * k)%positive + - xn ((Pos.max Ax Az)~0 * k)%positive * - zn ((Pos.max Ax Az)~0 * k)%positive))%Q - with (xn n * yn n - (xn ((Pos.max Ax Ay)~0 * k)%positive * - yn ((Pos.max Ax Ay)~0 * k)%positive) - + (xn n * zn n - xn ((Pos.max Ax Az)~0 * k)%positive * - zn ((Pos.max Ax Az)~0 * k)%positive))%Q. - 2: ring. - apply (Qle_lt_trans _ (Qabs (xn n * yn n - (xn ((Pos.max Ax Ay)~0 * k)%positive * - yn ((Pos.max Ax Ay)~0 * k)%positive)) - + Qabs (xn n * zn n - xn ((Pos.max Ax Az)~0 * k)%positive * - zn ((Pos.max Ax Az)~0 * k)%positive))). - apply Qabs_triangle. - setoid_replace (1#p)%Q with ((1#2*p) + (1#2*p))%Q. - apply Qplus_lt_le_compat. - + apply (CReal_mult_cauchy xn xn yn Ax Ay id limx limy). - intros. apply majx. exact limx. - refine (Pos.le_trans _ _ _ _ H1). discriminate. - apply majy. exact limy. - rewrite <- Pos.max_assoc. - rewrite (Pos.max_l ((2 * Pos.max Ax Ay * (2 * p)))). - 2: apply Pos.le_refl. - refine (Pos.le_trans _ _ _ _ H). apply Pos.max_lub. - apply (Pos.le_trans _ (2*1)). - apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - destruct (Pos.max (Pos.max Ax Ay) Az * (2 * p))%positive; discriminate. - rewrite <- Pos.mul_assoc, <- Pos.mul_assoc. - rewrite <- Pos.mul_le_mono_l, <- Pos.mul_le_mono_r. - apply Pos.le_max_l. - rewrite <- Pos.max_assoc. - rewrite (Pos.max_l ((2 * Pos.max Ax Ay * (2 * p)))). - 2: apply Pos.le_refl. - rewrite Pos.max_r. apply (Pos.le_trans _ (1*k)). - rewrite Pos.mul_1_l. refine (Pos.le_trans _ _ _ _ H0). - rewrite <- Pos.mul_assoc, <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - rewrite <- Pos.mul_le_mono_r. - apply Pos.le_max_l. apply Pos.mul_le_mono_r. discriminate. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - destruct (Pos.max Ax Ay * (2 * p))%positive; discriminate. - + apply Qlt_le_weak. - apply (CReal_mult_cauchy xn xn zn Ax Az id limx limz). - intros. apply majx. exact limx. - refine (Pos.le_trans _ _ _ _ H1). discriminate. - intros. apply majz. exact limz. exact H1. - rewrite <- Pos.max_assoc. - rewrite (Pos.max_l ((2 * Pos.max Ax Az * (2 * p)))). - 2: apply Pos.le_refl. - refine (Pos.le_trans _ _ _ _ H). apply Pos.max_lub. - apply (Pos.le_trans _ (2*1)). - apply Pos.le_refl. rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - destruct (Pos.max (Pos.max Ax Ay) Az * (2 * p))%positive; discriminate. - rewrite <- Pos.mul_assoc, <- Pos.mul_assoc. - rewrite <- Pos.mul_le_mono_l, <- Pos.mul_le_mono_r. - rewrite <- Pos.max_assoc, (Pos.max_comm Ay Az), Pos.max_assoc. - apply Pos.le_max_l. - rewrite <- Pos.max_assoc. - rewrite (Pos.max_l ((2 * Pos.max Ax Az * (2 * p)))). - 2: apply Pos.le_refl. - rewrite Pos.max_r. apply (Pos.le_trans _ (1*k)). - rewrite Pos.mul_1_l. refine (Pos.le_trans _ _ _ _ H0). - rewrite <- Pos.mul_assoc, <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - rewrite <- Pos.mul_le_mono_r. - rewrite <- Pos.max_assoc, (Pos.max_comm Ay Az), Pos.max_assoc. - apply Pos.le_max_l. apply Pos.mul_le_mono_r. discriminate. - apply (Pos.le_trans _ (2*1)). apply Pos.le_refl. - rewrite <- Pos.mul_assoc, <- Pos.mul_le_mono_l. - destruct (Pos.max Ax Az * (2 * p))%positive; discriminate. - + rewrite Qinv_plus_distr. unfold Qeq. reflexivity. + apply Qplus_lt_le_compat. rewrite HeqAy. + unfold proj1_sig. apply (QCauchySeq_bounded_prop yn cauy). + rewrite HeqAz. + unfold proj1_sig. apply Qlt_le_weak, (QCauchySeq_bounded_prop zn cauz). + unfold Qplus, Qle, Qnum, Qden. + apply Pos2Z.pos_le_pos. simpl. repeat rewrite Pos.mul_1_r. + apply Pos.le_max_r. } + rewrite (CReal_mult_bound_indep x (y+z) B xbound sumbound). + assert (forall n : positive, (Qabs (proj1_sig y n) < Z.pos B # 1)%Q) as ybound. + { intro n. subst B. apply (Qlt_le_trans _ (Z.pos Ay #1)). + rewrite HeqAy. + apply (QCauchySeq_bounded_prop (proj1_sig y)). + destruct y; exact q. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (Ay + Az)). + apply Pos2Nat.inj_le. rewrite <- (Nat.add_0_r (Pos.to_nat Ay)). + rewrite Pos2Nat.inj_add. apply Nat.add_le_mono_l, le_0_n. + apply Pos.le_max_r. } + rewrite (CReal_mult_bound_indep x y B xbound ybound). + assert (forall n : positive, (Qabs (proj1_sig z n) < Z.pos B # 1)%Q) as zbound. + { intro n. subst B. apply (Qlt_le_trans _ (Z.pos Az #1)). + rewrite HeqAz. + apply (QCauchySeq_bounded_prop (proj1_sig z)). + destruct z; exact q. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (Ay + Az)). + apply Pos2Nat.inj_le. rewrite <- (Nat.add_0_l (Pos.to_nat Az)). + rewrite Pos2Nat.inj_add. apply Nat.add_le_mono_r, le_0_n. + apply Pos.le_max_r. } + rewrite (CReal_mult_bound_indep x z B xbound zbound). + apply CRealEq_diff. + pose proof (CReal_mult_cauchy x y) as xycau. intro n. + destruct x as [xn caux], y as [yn cauy], z as [zn cauz]; + unfold CReal_mult, CReal_plus, proj1_sig; unfold proj1_sig in xycau. + rewrite Qred_correct, Qred_correct. + assert (forall a b c d e : Q, + c * (d + e) - (a+b) == c*d-a + (c*e-b))%Q. + { intros. ring. } + rewrite H. clear H. + setoid_replace (2#n)%Q with ((1#n) + (1#n))%Q. + 2: rewrite Qinv_plus_distr; reflexivity. + apply (Qle_trans _ _ _ (Qabs_triangle _ _)). + apply Qplus_le_compat. + - rewrite Qabs_Qminus. + replace (2 * B * (2 * n))%positive with (2 * (2 * B * n))%positive. + setoid_replace (xn (2 * (2 * B * n))%positive * yn (2 * (2 * B * n))%positive - + xn (2 * B * n)%positive * yn (2 * (2 * B * n))%positive)%Q + with ((xn (2 * (2 * B * n))%positive - xn (2 * B * n)%positive) + * yn (2 * (2 * B * n))%positive)%Q. + 2: ring. rewrite Qabs_Qmult. + apply (Qle_trans _ ((1 # 2*B*n) * Qabs (yn (2 * (2 * B * n))%positive))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + apply Qlt_le_weak, caux. apply belowMultiple. apply Pos.le_refl. + apply (Qmult_le_l _ _ (Z.pos (2* B *n) # 1)). + reflexivity. rewrite Qmult_assoc. + setoid_replace ((Z.pos (2 * B * n) # 1) * (1 # 2 * B * n))%Q + with 1%Q. + rewrite Qmult_1_l. + setoid_replace ((Z.pos (2 * B * n) # 1) * (1 # n))%Q + with (Z.pos (2 * B) # 1)%Q. + apply (Qle_trans _ (Z.pos B # 1)). + apply Qlt_le_weak, ybound. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply belowMultiple. + unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + rewrite Pos2Z.inj_mul. reflexivity. + unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + rewrite Pos2Z.inj_mul. reflexivity. + rewrite <- (Pos.mul_assoc 2 B (2*n)%positive). + apply f_equal. rewrite Pos.mul_assoc, (Pos.mul_comm 2 B). reflexivity. + - rewrite Qabs_Qminus. + replace (2 * B * (2 * n))%positive with (2 * (2 * B * n))%positive. + setoid_replace (xn (2 * (2 * B * n))%positive * zn (2 * (2 * B * n))%positive - + xn (2 * B * n)%positive * zn (2 * (2 * B * n))%positive)%Q + with ((xn (2 * (2 * B * n))%positive - xn (2 * B * n)%positive) + * zn (2 * (2 * B * n))%positive)%Q. + 2: ring. rewrite Qabs_Qmult. + apply (Qle_trans _ ((1 # 2*B*n) * Qabs (zn (2 * (2 * B * n))%positive))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + apply Qlt_le_weak, caux. apply belowMultiple. apply Pos.le_refl. + apply (Qmult_le_l _ _ (Z.pos (2* B *n) # 1)). + reflexivity. rewrite Qmult_assoc. + setoid_replace ((Z.pos (2 * B * n) # 1) * (1 # 2 * B * n))%Q + with 1%Q. + rewrite Qmult_1_l. + setoid_replace ((Z.pos (2 * B * n) # 1) * (1 # n))%Q + with (Z.pos (2 * B) # 1)%Q. + apply (Qle_trans _ (Z.pos B # 1)). + apply Qlt_le_weak, zbound. + unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply belowMultiple. + unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + rewrite Pos2Z.inj_mul. reflexivity. + unfold Qeq, Qmult, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + rewrite Pos2Z.inj_mul. reflexivity. + rewrite <- (Pos.mul_assoc 2 B (2*n)%positive). + apply f_equal. rewrite Pos.mul_assoc, (Pos.mul_comm 2 B). reflexivity. Qed. Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal, @@ -534,13 +464,184 @@ Proof. reflexivity. Qed. +Lemma CReal_opp_mult_distr_r + : forall r1 r2 : CReal, - (r1 * r2) == r1 * (- r2). +Proof. + intros. apply (CReal_plus_eq_reg_l (r1*r2)). + rewrite CReal_plus_opp_r, <- CReal_mult_plus_distr_l. + symmetry. apply CReal_mult_proper_0_l. + apply CReal_plus_opp_r. +Qed. + +Lemma CReal_mult_proper_l : forall x y z : CReal, + y == z -> x * y == x * z. +Proof. + intros. apply (CReal_plus_eq_reg_l (-(x*z))). + rewrite CReal_plus_opp_l, CReal_opp_mult_distr_r. + rewrite <- CReal_mult_plus_distr_l. + apply CReal_mult_proper_0_l. rewrite H. apply CReal_plus_opp_l. +Qed. + +Lemma CReal_mult_proper_r : forall x y z : CReal, + y == z -> y * x == z * x. +Proof. + intros. rewrite CReal_mult_comm, (CReal_mult_comm z). + apply CReal_mult_proper_l, H. +Qed. + +Lemma CReal_mult_assoc : forall x y z : CReal, (x * y) * z == x * (y * z). +Proof. + intros. + remember (QCauchySeq_bound (proj1_sig x) id) as Ax. + remember (QCauchySeq_bound (proj1_sig y) id) as Ay. + remember (QCauchySeq_bound (proj1_sig z) id) as Az. + pose (Pos.add (Ax * Ay) (Ay * Az)) as B. + assert (forall n : positive, (Qabs (proj1_sig x n) < Z.pos B # 1)%Q) as xbound. + { intro n. + destruct x as [xn limx]; unfold CReal_mult, proj1_sig. + apply (Qlt_le_trans _ (Z.pos Ax#1)). + rewrite HeqAx. + apply (QCauchySeq_bounded_prop xn limx). + subst B. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (Ax*Ay)). + rewrite Pos.mul_comm. apply belowMultiple. + apply Pos.lt_le_incl, Pos.lt_add_r. } + assert (forall n : positive, (Qabs (proj1_sig y n) < Z.pos B # 1)%Q) as ybound. + { intro n. + destruct y as [xn limx]; unfold CReal_mult, proj1_sig. + apply (Qlt_le_trans _ (Z.pos Ay#1)). + rewrite HeqAy. + apply (QCauchySeq_bounded_prop xn limx). + subst B. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (Ax*Ay)). + apply belowMultiple. apply Pos.lt_le_incl, Pos.lt_add_r. } + assert (forall n : positive, (Qabs (proj1_sig z n) < Z.pos B # 1)%Q) as zbound. + { intro n. + destruct z as [xn limx]; unfold CReal_mult, proj1_sig. + apply (Qlt_le_trans _ (Z.pos Az#1)). + rewrite HeqAz. + apply (QCauchySeq_bounded_prop xn limx). + subst B. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. + apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (Ay*Az)). + apply belowMultiple. rewrite Pos.add_comm. + apply Pos.lt_le_incl, Pos.lt_add_r. } + pose (exist (fun x0 : positive -> Q => QCauchySeq x0) + (fun n : positive => + (proj1_sig x (2 * B * n)%positive * proj1_sig y (2 * B * n)%positive)%Q) + (CReal_mult_cauchy x y B xbound ybound)) as xy. + rewrite (CReal_mult_proper_r + z (x*y) xy + (CReal_mult_bound_indep x y B xbound ybound)). + pose (exist (fun x0 : positive -> Q => QCauchySeq x0) + (fun n : positive => + (proj1_sig y (2 * B * n)%positive * proj1_sig z (2 * B * n)%positive)%Q) + (CReal_mult_cauchy y z B ybound zbound)) as yz. + rewrite (CReal_mult_proper_l + x (y*z) yz + (CReal_mult_bound_indep y z B ybound zbound)). + assert (forall n : positive, (Qabs (proj1_sig xy n) < Z.pos B # 1)%Q) as xybound. + { intro n. unfold xy, proj1_sig. clear xy yz. + destruct x as [xn limx], y as [yn limy]; unfold CReal_mult, proj1_sig. + rewrite Qabs_Qmult. + apply (Qle_lt_trans _ ((Z.pos Ax#1) * (Qabs (yn (2 * B * n)%positive)))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + rewrite HeqAx. + apply Qlt_le_weak, (QCauchySeq_bounded_prop xn limx). + rewrite Qmult_comm. + apply (Qle_lt_trans _ ((Z.pos Ay#1) * (Z.pos Ax#1))). + apply Qmult_le_compat_r. 2: discriminate. rewrite HeqAy. + apply Qlt_le_weak, (QCauchySeq_bounded_prop yn limy). + subst B. unfold Qmult, Qlt, Qnum, Qden. + rewrite Pos.mul_1_r, Z.mul_1_r, Z.mul_1_r, <- Pos2Z.inj_mul. + apply Pos2Z.pos_lt_pos. rewrite Pos.mul_comm. apply Pos.lt_add_r. } + rewrite (CReal_mult_bound_indep _ z B xybound zbound). + assert (forall n : positive, (Qabs (proj1_sig yz n) < Z.pos B # 1)%Q) as yzbound. + { intro n. unfold yz, proj1_sig. clear xybound xy yz. + destruct z as [zn limz], y as [yn limy]; unfold CReal_mult, proj1_sig. + rewrite Qabs_Qmult. + apply (Qle_lt_trans _ ((Z.pos Ay#1) * (Qabs (zn (2 * B * n)%positive)))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + rewrite HeqAy. + apply Qlt_le_weak, (QCauchySeq_bounded_prop yn limy). + rewrite Qmult_comm. + apply (Qle_lt_trans _ ((Z.pos Az#1) * (Z.pos Ay#1))). + apply Qmult_le_compat_r. 2: discriminate. rewrite HeqAz. + apply Qlt_le_weak, (QCauchySeq_bounded_prop zn limz). + subst B. unfold Qmult, Qlt, Qnum, Qden. + rewrite Pos.mul_1_r, Z.mul_1_r, Z.mul_1_r, <- Pos2Z.inj_mul. + apply Pos2Z.pos_lt_pos. rewrite Pos.add_comm, Pos.mul_comm. + apply Pos.lt_add_r. } + rewrite (CReal_mult_bound_indep x yz B xbound yzbound). + apply CRealEq_diff. intro n. unfold proj1_sig, xy, yz. + destruct x as [xn limx], y as [yn limy], z as [zn limz]; + unfold CReal_mult, proj1_sig. + clear xybound yzbound xy yz. + assert (forall a b c d e : Q, a*b*c - d*(b*e) == b*(a*c - d*e))%Q. + { intros. ring. } + rewrite H. clear H. rewrite Qabs_Qmult, Qmult_comm. + setoid_replace (xn (2 * B * (2 * B * n))%positive * zn (2 * B * n)%positive - + xn (2 * B * n)%positive * zn (2 * B * (2 * B * n))%positive)%Q + with ((xn (2 * B * (2 * B * n))%positive - xn (2 * B * n)%positive) + * zn (2 * B * n)%positive + + xn (2 * B * n)%positive * + (zn (2*B*n)%positive - zn (2 * B * (2 * B * n))%positive))%Q. + 2: ring. + apply (Qle_trans _ ( (Qabs ((1 # (2 * B * n)) * zn (2 * B * n)%positive) + + Qabs (xn (2 * B * n)%positive * (1 # (2 * B * n)))) + * Qabs (yn (2 * B * (2 * B * n))%positive))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + apply (Qle_trans _ _ _ (Qabs_triangle _ _)). + apply Qplus_le_compat. + rewrite Qabs_Qmult, Qabs_Qmult. + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + apply Qlt_le_weak, limx. apply belowMultiple. apply Pos.le_refl. + rewrite Qabs_Qmult, Qabs_Qmult, Qmult_comm, <- (Qmult_comm (Qabs (1 # 2 * B * n))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + apply Qlt_le_weak, limz. apply Pos.le_refl. apply belowMultiple. + rewrite Qabs_Qmult, Qabs_Qmult. + rewrite (Qmult_comm (Qabs (1 # 2 * B * n))). + rewrite <- Qmult_plus_distr_l. + rewrite (Qabs_pos (1 # 2 * B * n)). 2: discriminate. + rewrite <- (Qmult_comm (1 # 2 * B * n)), <- Qmult_assoc. + apply (Qmult_le_l _ _ (Z.pos (2* B *n) # 1)). + reflexivity. rewrite Qmult_assoc. + setoid_replace ((Z.pos (2 * B * n) # 1) * (1 # 2 * B * n))%Q + with 1%Q. + rewrite Qmult_1_l. + setoid_replace ((Z.pos (2 * B * n) # 1) * (2 # n))%Q + with (Z.pos (2 * 2 * B) # 1)%Q. + apply (Qle_trans _ (((Z.pos Az#1) + (Z.pos Ax#1)) * + Qabs (yn (2 * B * (2 * B * n))%positive))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. + apply Qplus_le_compat. rewrite HeqAz. + apply Qlt_le_weak, (QCauchySeq_bounded_prop zn limz). + rewrite HeqAx. + apply Qlt_le_weak, (QCauchySeq_bounded_prop xn limx). + rewrite Qmult_comm. + apply (Qle_trans _ ((Z.pos Ay#1)* ((Z.pos Az # 1) + (Z.pos Ax # 1)))). + apply Qmult_le_compat_r. + rewrite HeqAy. + apply Qlt_le_weak, (QCauchySeq_bounded_prop yn limy). discriminate. + rewrite Qinv_plus_distr. subst B. + unfold Qle, Qmult, Qplus, Qnum, Qden. + repeat rewrite Pos.mul_1_r. repeat rewrite Z.mul_1_r. + rewrite <- Pos2Z.inj_add, <- Pos2Z.inj_mul. + apply Pos2Z.pos_le_pos. rewrite Pos.mul_add_distr_l. + rewrite Pos.add_comm, Pos.mul_comm. apply belowMultiple. + unfold Qeq, Qmult, Qnum, Qden. + simpl. rewrite Pos.mul_1_r. rewrite Pos.mul_comm. reflexivity. + unfold Qeq, Qmult, Qnum, Qden. + simpl. rewrite Pos.mul_1_r, Pos.mul_1_r. reflexivity. +Qed. + + Lemma CReal_mult_1_l : forall r: CReal, 1 * r == r. Proof. intros [rn limr]. split. - intros [m maj]. simpl in maj. rewrite Qmult_1_l in maj. - pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) id (ConstCauchy 1)). - pose proof (QCauchySeq_bounded_prop rn id limr). + pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) (ConstCauchy 1)). + pose proof (QCauchySeq_bounded_prop rn limr). remember (QCauchySeq_bound (fun _ : positive => 1%Q) id) as x. remember (QCauchySeq_bound rn id) as x0. specialize (limr m). @@ -555,8 +656,8 @@ Proof. apply Z.mul_le_mono_nonneg. discriminate. discriminate. discriminate. apply Z.le_refl. - intros [m maj]. simpl in maj. - pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) id (ConstCauchy 1)). - pose proof (QCauchySeq_bounded_prop rn id limr). + pose proof (QCauchySeq_bounded_prop (fun _ : positive => 1%Q) (ConstCauchy 1)). + pose proof (QCauchySeq_bounded_prop rn limr). remember (QCauchySeq_bound (fun _ : positive => 1%Q) id) as x. remember (QCauchySeq_bound rn id) as x0. simpl in maj. rewrite Qmult_1_l in maj. @@ -655,17 +756,6 @@ Qed. Add Ring CRealRing : CReal_isRing. (**********) -Lemma CReal_mult_0_l : forall r, 0 * r == 0. -Proof. - intro; ring. -Qed. - -Lemma CReal_mult_0_r : forall r, r * 0 == 0. -Proof. - intro; ring. -Qed. - -(**********) Lemma CReal_mult_1_r : forall r, r * 1 == r. Proof. intro; ring. @@ -677,12 +767,6 @@ Proof. intros. ring. Qed. -Lemma CReal_opp_mult_distr_r - : forall r1 r2 : CReal, - (r1 * r2) == r1 * (- r2). -Proof. - intros. ring. -Qed. - Lemma CReal_mult_lt_compat_l : forall x y z : CReal, 0 < x -> y < z -> x*y < x*z. Proof. @@ -707,22 +791,22 @@ Qed. Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal), r # 0 - -> CRealEq (CReal_mult r r1) (CReal_mult r r2) - -> CRealEq r1 r2. + -> r * r1 == r * r2 + -> r1 == r2. Proof. intros. destruct H; split. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. - exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r). + exact (CRealLe_refl _ abs). apply (CReal_plus_lt_reg_l r). rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l (-r)) in abs. rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs. - exact (CRealLt_irrefl _ abs). apply (CReal_plus_lt_reg_l r). + exact (CRealLe_refl _ abs). apply (CReal_plus_lt_reg_l r). rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l. exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs. - exact (CRealLt_irrefl _ abs). exact c. + exact (CRealLe_refl _ abs). exact c. - intro abs. apply (CReal_mult_lt_compat_l r) in abs. rewrite H0 in abs. - exact (CRealLt_irrefl _ abs). exact c. + exact (CRealLe_refl _ abs). exact c. Qed. Lemma CReal_abs_appart_zero : forall (x : CReal) (n : positive), @@ -775,7 +859,8 @@ Proof. apply Qle_Qabs. apply limx. apply Pos.le_max_l. apply Pos.le_refl. - apply (CReal_plus_lt_reg_l (-(2))). ring_simplify. - exists 4%positive. simpl. + exists 4%positive. unfold inject_Q, CReal_minus, CReal_plus, proj1_sig. + rewrite Qred_correct. simpl. rewrite <- Qinv_plus_distr. rewrite <- (Qplus_lt_r _ _ ((n#1) - (1#2))). ring_simplify. apply (Qle_lt_trans _ (xn 4%positive + (1 # 4)) _ H0). @@ -833,203 +918,60 @@ Proof. (proj1_sig d (Pos.of_nat (S n)) - proj1_sig c (Pos.of_nat (S n)))); assumption. Qed. -Lemma CRealShiftReal : forall (x : CReal) (k : positive), - QCauchySeq (fun n => proj1_sig x (Pos.add n k)) id. -Proof. - assert (forall p k : positive, (p <= p + k)%positive). - { intros. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add. - apply (le_trans _ (Pos.to_nat p + 0)). - rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l. - apply le_0_n. } - intros x k n p q H0 H1. - destruct x as [xn cau]; unfold proj1_sig. - apply cau. apply (Pos.le_trans _ _ _ H0). apply H. - apply (Pos.le_trans _ _ _ H1). apply H. -Qed. - -Lemma CRealShiftEqual : forall (x : CReal) (k : positive), - CRealEq x (exist _ (fun n => proj1_sig x (Pos.add n k)) (CRealShiftReal x k)). -Proof. - intros. split. - - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (n + k)%positive n). - apply Qlt_not_le in maj. apply maj. clear maj. - apply (Qle_trans _ (Qabs (xn (n + k)%positive - xn n))). - apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Zlt_le_weak. - apply cau. unfold id. apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add. - apply (le_trans _ (Pos.to_nat n + 0)). - rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l. - apply le_0_n. apply Pos.le_refl. - apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. discriminate. - - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n n (n + k)%positive). - apply Qlt_not_le in maj. apply maj. clear maj. - apply (Qle_trans _ (Qabs (xn n - xn (n + k)%positive))). - apply Qle_Qabs. apply (Qle_trans _ (1#n)). apply Zlt_le_weak. - apply cau. apply Pos.le_refl. - apply Pos2Nat.inj_le. rewrite Pos2Nat.inj_add. - apply (le_trans _ (Pos.to_nat n + 0)). - rewrite plus_0_r. apply le_refl. apply Nat.add_le_mono_l. - apply le_0_n. - apply Z.mul_le_mono_pos_r. apply Pos2Z.is_pos. discriminate. -Qed. - -(* Find an equal negative real number, which rational sequence - stays below 0, so that it can be inversed. *) -Definition CRealNegShift (x : CReal) - : x < inject_Q 0 - -> { y : prod positive CReal - | x == (snd y) /\ forall n:positive, Qlt (proj1_sig (snd y) n) (-1 # fst y) }. -Proof. - intro xNeg. - pose proof (CRealLt_aboveSig x (inject_Q 0)). - pose proof (CRealShiftReal x). - pose proof (CRealShiftEqual x). - destruct xNeg as [n maj], x as [xn cau]; simpl in maj. - specialize (H n maj); simpl in H. - destruct (Qarchimedean (/ (0 - xn n - (2 # n)))) as [a _]. - remember (Pos.max n a~0) as k. - clear Heqk. clear maj. clear n. - exists (pair k (exist _ (fun n => xn (Pos.add n k)) (H0 k))). - split. apply H1. intro n. simpl. apply Qlt_minus_iff. - apply (Qlt_trans _ (-(2 # k) - xn (n + k)%positive)). - specialize (H (n + k)%positive). - unfold Qminus in H. rewrite Qplus_0_l in H. apply Qlt_minus_iff in H. - unfold Qminus. rewrite Qplus_comm. apply H. apply Pos2Nat.inj_le. - rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add. - apply Nat.add_le_mono_r. apply le_0_n. - apply Qplus_lt_l. - apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. - reflexivity. -Qed. - -Definition CRealPosShift (x : CReal) - : inject_Q 0 < x - -> { y : prod positive CReal - | x == (snd y) /\ forall n:positive, Qlt (1 # fst y) (proj1_sig (snd y) n) }. -Proof. - intro xPos. - pose proof (CRealLt_aboveSig (inject_Q 0) x). - pose proof (CRealShiftReal x). - pose proof (CRealShiftEqual x). - destruct xPos as [n maj], x as [xn cau]; simpl in maj. - simpl in H. specialize (H n). - destruct (Qarchimedean (/ (xn n - 0 - (2 # n)))) as [a _]. - specialize (H maj); simpl in H. - remember (Pos.max n a~0) as k. - clear Heqk. clear maj. clear n. - exists (pair k (exist _ (fun n => xn (Pos.add n k)) (H0 k))). - split. apply H1. intro n. simpl. apply Qlt_minus_iff. - rewrite <- Qlt_minus_iff. apply (Qlt_trans _ (2 # k)). - apply Z.mul_lt_mono_pos_r. simpl. apply Pos2Z.is_pos. - reflexivity. specialize (H (n + k)%positive). - unfold Qminus in H. rewrite Qplus_0_r in H. - apply H. apply Pos2Nat.inj_le. - rewrite <- (plus_0_l (Pos.to_nat k)). rewrite Pos2Nat.inj_add. - apply Nat.add_le_mono_r. apply le_0_n. +(* Find a positive index after which the Cauchy sequence proj1_sig x + stays above 0, so that it can be inverted. *) +Lemma CRealPosShift_correct + : forall (x : CReal) (xPos : 0 < x) (n : positive), + Pos.le (proj1_sig xPos) n + -> Qlt (1 # proj1_sig xPos) (proj1_sig x n). +Proof. + intros x xPos p pmaj. + destruct xPos as [n maj]; simpl in maj. + apply (CRealLt_0_aboveSig x n). + unfold proj1_sig in pmaj. + apply (Qlt_le_trans _ _ _ maj). + ring_simplify. apply Qle_refl. apply pmaj. Qed. -Lemma CReal_inv_neg : forall (yn : positive -> Q) (k : positive), - (QCauchySeq yn id) - -> (forall n : positive, yn n < -1 # k)%Q - -> QCauchySeq (fun n : positive => / yn (k ^ 2 * n)%positive) id. -Proof. - (* Prove the inverse sequence is Cauchy *) - intros yn k cau maj n p q H0 H1. - setoid_replace (/ yn (k ^ 2 * p)%positive - - / yn (k ^ 2 * q)%positive)%Q - with ((yn (k ^ 2 * q)%positive - - yn (k ^ 2 * p)%positive) - / (yn (k ^ 2 * q)%positive * - yn (k ^ 2 * p)%positive)). - + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive - - yn (k ^ 2 * p)%positive) +Lemma CReal_inv_pos_cauchy + : forall (x : CReal) (xPos : 0 < x) (k : positive), + (forall n:positive, Pos.le k n -> Qlt (1 # k) (proj1_sig x n)) + -> QCauchySeq (fun n : positive => / proj1_sig x (k ^ 2 * n)%positive). +Proof. + intros [xn xcau] xPos k maj. unfold proj1_sig. + intros n p q H0 H1. + setoid_replace (/ xn (k ^ 2 * p)%positive - / xn (k ^ 2 * q)%positive)%Q + with ((xn (k ^ 2 * q)%positive - + xn (k ^ 2 * p)%positive) + / (xn (k ^ 2 * q)%positive * + xn (k ^ 2 * p)%positive)). + + apply (Qle_lt_trans _ (Qabs (xn (k ^ 2 * q)%positive + - xn (k ^ 2 * p)%positive) / (1 # (k^2)))). assert (1 # k ^ 2 - < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q. + < Qabs (xn (k ^ 2 * q)%positive * xn (k ^ 2 * p)%positive))%Q. { rewrite Qabs_Qmult. unfold "^"%positive; simpl. rewrite factorDenom. rewrite Pos.mul_1_r. - apply (Qlt_trans _ ((1#k) * Qabs (yn (k * (k * 1) * p)%positive))). - apply Qmult_lt_l. reflexivity. rewrite Qabs_neg. - specialize (maj (k * (k * 1) * p)%positive). - apply Qlt_minus_iff in maj. apply Qlt_minus_iff. - rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj. - reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. - apply maj. discriminate. rewrite Pos.mul_1_r. - apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity. - rewrite Qabs_neg. - specialize (maj (k * k * p)%positive). - apply Qlt_minus_iff in maj. apply Qlt_minus_iff. - rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. - apply maj. reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. - apply maj. discriminate. - rewrite Qabs_neg. - specialize (maj (k * k * q)%positive). - apply Qlt_minus_iff in maj. apply Qlt_minus_iff. - rewrite Qplus_comm. setoid_replace (-(1#k))%Q with (-1 # k)%Q. apply maj. - reflexivity. apply (Qle_trans _ (-1 # k)). apply Zlt_le_weak. - apply maj. discriminate. } - unfold Qdiv. rewrite Qabs_Qmult. rewrite Qabs_Qinv. - rewrite Qmult_comm. rewrite <- (Qmult_comm (/ (1 # k ^ 2))). - apply Qmult_le_compat_r. apply Qlt_le_weak. - rewrite <- Qmult_1_l. apply Qlt_shift_div_r. - apply (Qlt_trans 0 (1 # k ^ 2)). reflexivity. apply H. - rewrite Qmult_comm. apply Qlt_shift_div_l. - reflexivity. rewrite Qmult_1_l. apply H. - apply Qabs_nonneg. simpl in maj. - specialize (cau (n * (k^2))%positive - (k ^ 2 * q)%positive - (k ^ 2 * p)%positive). - apply Qlt_shift_div_r. reflexivity. - apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau. - rewrite Pos.mul_comm. - unfold "^"%positive. simpl. - unfold id. rewrite Pos.mul_1_r. - rewrite <- Pos.mul_le_mono_l. exact H1. - unfold id. rewrite Pos.mul_comm. - apply Pos.mul_le_mono_l. exact H0. - rewrite factorDenom. apply Qle_refl. - + field. split. intro abs. - specialize (maj (k ^ 2 * p)%positive). - rewrite abs in maj. inversion maj. - intro abs. - specialize (maj (k ^ 2 * q)%positive). - rewrite abs in maj. inversion maj. -Qed. - -Lemma CReal_inv_pos : forall (yn : positive -> Q) (k : positive), - (QCauchySeq yn id) - -> (forall n : positive, 1 # k < yn n)%Q - -> QCauchySeq (fun n : positive => / yn (k ^ 2 * n)%positive) id. -Proof. - intros yn k cau maj n p q H0 H1. - setoid_replace (/ yn (k ^ 2 * p)%positive - - / yn (k ^ 2 * q)%positive)%Q - with ((yn (k ^ 2 * q)%positive - - yn (k ^ 2 * p)%positive) - / (yn (k ^ 2 * q)%positive * - yn (k ^ 2 * p)%positive)). - + apply (Qle_lt_trans _ (Qabs (yn (k ^ 2 * q)%positive - - yn (k ^ 2 * p)%positive) - / (1 # (k^2)))). - assert (1 # k ^ 2 - < Qabs (yn (k ^ 2 * q)%positive * yn (k ^ 2 * p)%positive))%Q. - { rewrite Qabs_Qmult. unfold "^"%positive; simpl. - rewrite factorDenom. rewrite Pos.mul_1_r. - apply (Qlt_trans _ ((1#k) * Qabs (yn (k * k * p)%positive))). + apply (Qlt_trans _ ((1#k) * Qabs (xn (k * k * p)%positive))). apply Qmult_lt_l. reflexivity. rewrite Qabs_pos. specialize (maj (k * k * p)%positive). - apply maj. apply (Qle_trans _ (1 # k)). + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. + apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. + rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. apply Qmult_lt_r. apply (Qlt_trans 0 (1#k)). reflexivity. rewrite Qabs_pos. specialize (maj (k * k * p)%positive). - apply maj. apply (Qle_trans _ (1 # k)). discriminate. + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. + apply (Qle_trans _ (1 # k)). discriminate. apply Zlt_le_weak. apply maj. + rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. rewrite Qabs_pos. specialize (maj (k * k * q)%positive). - apply maj. apply (Qle_trans _ (1 # k)). discriminate. - apply Zlt_le_weak. apply maj. } + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. + apply (Qle_trans _ (1 # k)). discriminate. + apply Zlt_le_weak. + apply maj. rewrite Pos.mul_comm, Pos.mul_assoc. apply belowMultiple. } unfold Qdiv. rewrite Qabs_Qmult. rewrite Qabs_Qinv. rewrite Qmult_comm. rewrite <- (Qmult_comm (/ (1 # k ^ 2))). apply Qmult_le_compat_r. apply Qlt_le_weak. @@ -1038,11 +980,11 @@ Proof. rewrite Qmult_comm. apply Qlt_shift_div_l. reflexivity. rewrite Qmult_1_l. apply H. apply Qabs_nonneg. simpl in maj. - specialize (cau (n * (k^2))%positive - (k ^ 2 * q)%positive - (k ^ 2 * p)%positive). + pose proof (xcau (n * (k^2))%positive + (k ^ 2 * q)%positive + (k ^ 2 * p)%positive). apply Qlt_shift_div_r. reflexivity. - apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply cau. + apply (Qlt_le_trans _ (1 # n * k ^ 2)). apply xcau. rewrite Pos.mul_comm. unfold id. apply Pos.mul_le_mono_l. exact H1. unfold id. rewrite Pos.mul_comm. @@ -1050,25 +992,35 @@ Proof. rewrite factorDenom. apply Qle_refl. + field. split. intro abs. specialize (maj (k ^ 2 * p)%positive). - rewrite abs in maj. inversion maj. + rewrite abs in maj. apply (Qlt_not_le (1#k) 0). + apply maj. unfold "^"%positive; simpl. rewrite <- Pos.mul_assoc. + rewrite Pos.mul_comm. apply belowMultiple. discriminate. intro abs. specialize (maj (k ^ 2 * q)%positive). - rewrite abs in maj. inversion maj. + rewrite abs in maj. apply (Qlt_not_le (1#k) 0). + apply maj. unfold "^"%positive; simpl. rewrite <- Pos.mul_assoc. + rewrite Pos.mul_comm. apply belowMultiple. discriminate. Qed. -Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal. +Definition CReal_inv_pos (x : CReal) (xPos : 0 < x) : CReal + := exist _ + (fun n : positive => / proj1_sig x (proj1_sig xPos ^ 2 * n)%positive) + (CReal_inv_pos_cauchy + x xPos (proj1_sig xPos) (CRealPosShift_correct x xPos)). + +Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. Proof. - destruct xnz as [xNeg | xPos]. - - destruct (CRealNegShift x xNeg) as [[k y] [_ maj]]. - destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj. - exists (fun n:positive => Qinv (yn (Pos.mul (k^2) n)%positive)). - apply (CReal_inv_neg yn). apply cau. apply maj. - - destruct (CRealPosShift x xPos) as [[k y] [_ maj]]. - destruct y as [yn cau]; unfold proj1_sig, snd, fst in maj. - exists (fun n => Qinv (yn (Pos.mul (k^2) n))). - apply (CReal_inv_pos yn). apply cau. apply maj. + intros x [n nmaj]. exists n. + apply (Qlt_le_trans _ _ _ nmaj). destruct x. simpl. + unfold Qminus. rewrite Qplus_0_l, Qplus_0_r. apply Qle_refl. Defined. +Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal + := match xnz with + | inl xNeg => - CReal_inv_pos (-x) (CReal_neg_lt_pos x xNeg) + | inr xPos => CReal_inv_pos x xPos + end. + Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : CReal_scope. Lemma CReal_inv_0_lt_compat @@ -1078,32 +1030,33 @@ Proof. intros. unfold CReal_inv. simpl. destruct rnz. - exfalso. apply CRealLt_asym in H. contradiction. - - destruct (CRealPosShift r c) as [[k rpos] [req maj]]. - clear req. destruct rpos as [rn cau]; simpl in maj. + - unfold CReal_inv_pos. + pose proof (CRealPosShift_correct r c) as maj. + destruct r as [xn cau]. unfold CRealLt; simpl. - destruct (Qarchimedean (rn 1%positive)) as [A majA]. + destruct (Qarchimedean (xn 1%positive)) as [A majA]. exists (2 * (A + 1))%positive. unfold Qminus. rewrite Qplus_0_r. - rewrite <- (Qmult_1_l (Qinv (rn (k * (k * 1) * (2 * (A + 1)))%positive))). - apply Qlt_shift_div_l. apply (Qlt_trans 0 (1#k)). reflexivity. - apply maj. rewrite <- (Qmult_inv_r (Z.pos A + 1 # 1)). + rewrite <- (Qmult_1_l (/ xn (proj1_sig c ^ 2 * (2 * (A + 1)))%positive)). + apply Qlt_shift_div_l. apply (Qlt_trans 0 (1# proj1_sig c)). reflexivity. + apply maj. unfold "^"%positive, Pos.iter. + rewrite <- Pos.mul_assoc, Pos.mul_comm. apply belowMultiple. + rewrite <- (Qmult_inv_r (Z.pos A + 1 # 1)). setoid_replace (2 # 2 * (A + 1))%Q with (Qinv (Z.pos A + 1 # 1)). 2: reflexivity. rewrite Qmult_comm. apply Qmult_lt_r. reflexivity. - rewrite Pos.mul_1_r. - rewrite <- (Qplus_lt_l _ _ (- rn 1%positive)). - apply (Qle_lt_trans _ (Qabs (rn (k * k * (2 * (A + 1)))%positive + - rn 1%positive))). + rewrite <- (Qplus_lt_l _ _ (- xn 1%positive)). + apply (Qle_lt_trans _ (Qabs (xn (proj1_sig c ^ 2 * (2 * (A + 1)))%positive + - xn 1%positive))). apply Qle_Qabs. apply (Qlt_le_trans _ 1). apply cau. - destruct (k * k * (2 * (A + 1)))%positive; discriminate. - apply Pos.le_refl. + apply Pos.le_1_l. apply Pos.le_1_l. rewrite <- Qinv_plus_distr. rewrite <- (Qplus_comm 1). rewrite <- Qplus_0_r. rewrite <- Qplus_assoc. rewrite <- Qplus_assoc. rewrite Qplus_le_r. rewrite Qplus_0_l. apply Qlt_le_weak. apply Qlt_minus_iff in majA. apply majA. intro abs. inversion abs. -Qed. +Defined. Lemma CReal_linear_shift : forall (x : CReal) (k : positive), - QCauchySeq (fun n => proj1_sig x (k * n)%positive) id. + QCauchySeq (fun n => proj1_sig x (k * n)%positive). Proof. intros [xn limx] k p n m H H0. unfold proj1_sig. apply limx. apply (Pos.le_trans _ n). apply H. @@ -1114,8 +1067,8 @@ Proof. Qed. Lemma CReal_linear_shift_eq : forall (x : CReal) (k : positive), - CRealEq x - (exist (fun n : positive -> Q => QCauchySeq n id) + x == + (exist (fun n : positive -> Q => QCauchySeq n) (fun n : positive => proj1_sig x (k * n)%positive) (CReal_linear_shift x k)). Proof. intros. apply CRealEq_diff. intro n. @@ -1128,106 +1081,50 @@ Proof. apply Z.mul_le_mono_nonneg_r. discriminate. discriminate. Qed. +Lemma CReal_inv_l_pos : forall (r:CReal) (rnz : 0 < r), + (CReal_inv_pos r rnz) * r == 1. +Proof. + intros r c. + unfold CReal_inv_pos. + pose proof (CRealPosShift_correct r c) as maj. + rewrite (CReal_mult_proper_l + _ r (exist _ (fun n => proj1_sig r (proj1_sig c ^ 2 * n)%positive) + (CReal_linear_shift r _))). + 2: rewrite <- CReal_linear_shift_eq; apply reflexivity. + apply CRealEq_diff. intro n. + destruct r as [rn limr]. + unfold CReal_mult, inject_Q, proj1_sig. + rewrite Qmult_comm, Qmult_inv_r. + unfold Qminus. rewrite Qplus_opp_r, Qabs_pos. + discriminate. apply Qle_refl. + unfold proj1_sig in maj. + intro abs. + specialize (maj ((let (a, _) := c in a) ^ 2 * + (2 * + Pos.max + (QCauchySeq_bound + (fun n : positive => Qinv (rn ((let (a, _) := c in a) ^ 2 * n))) id) + (QCauchySeq_bound + (fun n : positive => rn ((let (a, _) := c in a) ^ 2 * n)) id) * n))%positive). + simpl in maj. unfold proj1_sig in maj, abs. + rewrite abs in maj. clear abs. + apply (Qlt_not_le (1 # (let (a, _) := c in a)) 0). + apply maj. unfold "^"%positive, Pos.iter. + rewrite <- Pos.mul_assoc, Pos.mul_comm. apply belowMultiple. + discriminate. +Qed. + Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0), ((/ r) rnz) * r == 1. Proof. - intros. unfold CReal_inv; simpl. - destruct rnz. - - (* r < 0 *) destruct (CRealNegShift r c) as [[k rneg] [req maj]]. - simpl in req. apply CRealEq_diff. apply CRealEq_modindep. - apply (QSeqEquivEx_trans _ - (proj1_sig (CReal_mult ((let - (yn, cau) as s - return ((forall n : positive, proj1_sig s n < -1 # k) -> CReal) := rneg in - fun maj0 : forall n : positive, yn n < -1 # k => - exist (fun x : positive -> Q => QCauchySeq x id) - (fun n : positive => Qinv (yn (k * (k * 1) * n))%positive) - (CReal_inv_neg yn k cau maj0)) maj) rneg)))%Q. - + apply CRealEq_modindep. apply CRealEq_diff. - apply CReal_mult_proper_l. apply req. - + apply (QSeqEquivEx_trans _ - (proj1_sig (CReal_mult ((let - (yn, cau) as s - return ((forall n : positive, proj1_sig s n < -1 # k) -> CReal) := rneg in - fun maj0 : forall n : positive, yn n < -1 # k => - exist (fun x : positive -> Q => QCauchySeq x id) - (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive)) - (CReal_inv_neg yn k cau maj0)) maj) - (exist _ (fun n => proj1_sig rneg (k * (k * 1) * n)%positive) (CReal_linear_shift rneg _)))))%Q. - apply CRealEq_modindep. apply CRealEq_diff. - apply CReal_mult_proper_l. apply CReal_linear_shift_eq. - destruct r as [rn limr], rneg as [rnn limneg]; simpl. - pose proof (QCauchySeq_bounded_prop - (fun n : positive => Qinv (rnn (k * (k * 1) * n)%positive)) - id (CReal_inv_neg rnn k limneg maj)). - pose proof (QCauchySeq_bounded_prop - (fun n : positive => rnn (k * (k * 1) * n)%positive) - id - (CReal_linear_shift - (exist (fun x0 : positive -> Q => QCauchySeq x0 id) rnn limneg) - (k * (k * 1)))) ; simpl. - remember (QCauchySeq_bound - (fun n0 : positive => / rnn (k * (k * 1) * n0)%positive)%Q - id) as x. - remember (QCauchySeq_bound - (fun n0 : positive => rnn (k * (k * 1) * n0)%positive) - id) as x0. - exists (fun n => 1%positive). intros p n m H2 H3. rewrite Qmult_comm. - rewrite Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r. - reflexivity. intro abs. - unfold snd,fst, proj1_sig in maj. - specialize (maj (k * (k * 1) * (Pos.max x x0 * n)~0)%positive). - rewrite abs in maj. inversion maj. - - (* r > 0 *) destruct (CRealPosShift r c) as [[k rneg] [req maj]]. - simpl in req. apply CRealEq_diff. apply CRealEq_modindep. - apply (QSeqEquivEx_trans _ - (proj1_sig (CReal_mult ((let - (yn, cau) as s - return ((forall n : positive, 1 # k < proj1_sig s n) -> CReal) := rneg in - fun maj0 : forall n : positive, 1 # k < yn n => - exist (fun x : positive -> Q => QCauchySeq x id) - (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive)) - (CReal_inv_pos yn k cau maj0)) maj) rneg)))%Q. - + apply CRealEq_modindep. apply CRealEq_diff. - apply CReal_mult_proper_l. apply req. - + assert (le 1 (Pos.to_nat k * (Pos.to_nat k * 1))%nat). rewrite mult_1_r. - rewrite <- Pos2Nat.inj_mul. apply Pos2Nat.is_pos. - apply (QSeqEquivEx_trans _ - (proj1_sig (CReal_mult ((let - (yn, cau) as s - return ((forall n : positive, 1 # k < proj1_sig s n) -> CReal) := rneg in - fun maj0 : forall n : positive, 1 # k < yn n => - exist (fun x : positive -> Q => QCauchySeq x id) - (fun n : positive => Qinv (yn (k * (k * 1) * n)%positive)) - (CReal_inv_pos yn k cau maj0)) maj) - (exist _ (fun n => proj1_sig rneg (k * (k * 1) * n)%positive) (CReal_linear_shift rneg _)))))%Q. - apply CRealEq_modindep. apply CRealEq_diff. - apply CReal_mult_proper_l. apply CReal_linear_shift_eq. - destruct r as [rn limr], rneg as [rnn limneg]; simpl. - pose proof (QCauchySeq_bounded_prop - (fun n : positive => Qinv (rnn (k * (k * 1) * n)%positive)) - id (CReal_inv_pos rnn k limneg maj)). - pose proof (QCauchySeq_bounded_prop - (fun n : positive => rnn (k * (k * 1) * n)%positive) - id - (CReal_linear_shift - (exist (fun x0 : positive -> Q => QCauchySeq x0 id) rnn limneg) - (k * (k * 1)))) ; simpl. - remember (QCauchySeq_bound - (fun n0 : positive => / rnn (k * (k * 1) * n0)%positive) - id)%Q as x. - remember (QCauchySeq_bound - (fun n0 : positive => rnn (k * (k * 1) * n0)%positive) - id) as x0. - exists (fun n => 1%positive). intros p n m H2 H3. rewrite Qmult_comm. - rewrite Qmult_inv_r. unfold Qminus. rewrite Qplus_opp_r. - reflexivity. intro abs. - specialize (maj ((k * (k * 1) * (Pos.max x x0 * n)~0)%positive)). - simpl in maj. rewrite abs in maj. inversion maj. + intros. unfold CReal_inv. destruct rnz. + - rewrite <- CReal_opp_mult_distr_l, CReal_opp_mult_distr_r. + apply CReal_inv_l_pos. + - apply CReal_inv_l_pos. Qed. Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0), - r * ((/ r) rnz) == 1. + r * ((/ r) rnz) == 1. Proof. intros. rewrite CReal_mult_comm, CReal_inv_l. reflexivity. @@ -1328,18 +1225,22 @@ Proof. apply Qabs_Qle_condition. split. apply Qlt_le_weak. apply Qlt_minus_iff, (Qlt_trans _ (2#j)). reflexivity. apply jmaj. + apply (Pos.le_trans _ (2*j)). apply belowMultiple. + apply Pos.mul_le_mono_l. apply (Pos.le_trans _ (1 * Pos.max k (Pos.max i j))). rewrite Pos.mul_1_l. apply (Pos.le_trans _ (Pos.max i j) _ (Pos.le_max_r _ _)). apply Pos.le_max_r. - rewrite <- Pos.mul_le_mono_r. discriminate. + rewrite <- Pos.mul_le_mono_r. destruct (Pos.max a b); discriminate. apply Qlt_le_weak. apply Qlt_minus_iff, (Qlt_trans _ (2#i)). reflexivity. apply imaj. + apply (Pos.le_trans _ (2*i)). apply belowMultiple. + apply Pos.mul_le_mono_l. apply (Pos.le_trans _ (1 * Pos.max k (Pos.max i j))). rewrite Pos.mul_1_l. apply (Pos.le_trans _ (Pos.max i j) _ (Pos.le_max_l _ _)). apply Pos.le_max_r. - rewrite <- Pos.mul_le_mono_r. discriminate. + rewrite <- Pos.mul_le_mono_r. destruct (Pos.max a b); discriminate. - left. apply (CReal_mult_lt_reg_r (exist _ yn ycau) _ _ c). rewrite CReal_mult_0_l. exact H. - right. apply (CReal_mult_lt_reg_r (CReal_opp (exist _ yn ycau))). diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index 6f36e888ed..be844c413a 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -138,20 +138,20 @@ Proof. destruct x as [xn cau]. unfold CReal_abs, CReal_minus, CReal_plus, CReal_opp, inject_Q, proj1_sig in kmaj. apply (Qlt_not_le _ _ kmaj). clear kmaj. - unfold QCauchySeq, QSeqEquiv in cau. + unfold QCauchySeq in cau. rewrite <- (Qplus_le_l _ _ (1#n)). ring_simplify. unfold id in cau. destruct (Pos.lt_total (2*k) n). 2: destruct H. - specialize (cau k (2*k)%positive n). assert (k <= 2 * k)%positive. { apply (Pos.le_trans _ (1*k)). apply Pos.le_refl. apply Pos.mul_le_mono_r. discriminate. } - apply (Qle_trans _ (1#k)). apply Qlt_le_weak, cau. + apply (Qle_trans _ (1#k)). rewrite Qred_correct. apply Qlt_le_weak, cau. exact H0. apply (Pos.le_trans _ _ _ H0). apply Pos.lt_le_incl, H. rewrite <- (Qinv_plus_distr 1 1). apply (Qplus_le_l _ _ (-(1#k))). ring_simplify. discriminate. - subst n. rewrite Qplus_opp_r. discriminate. - specialize (cau n (2*k)%positive n). - apply (Qle_trans _ (1#n)). apply Qlt_le_weak, cau. + apply (Qle_trans _ (1#n)). rewrite Qred_correct. apply Qlt_le_weak, cau. apply Pos.lt_le_incl, H. apply Pos.le_refl. apply (Qplus_le_l _ _ (-(1#n))). ring_simplify. discriminate. Qed. @@ -160,7 +160,7 @@ Qed. Lemma Rcauchy_limit : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn), QCauchySeq (fun n : positive => - let (p, _) := xcau (4 * n)%positive in proj1_sig (xn p) (4 * n)%positive) id. + let (p, _) := xcau (4 * n)%positive in proj1_sig (xn p) (4 * n)%positive). Proof. intros xn xcau n p q H0 H1. destruct (xcau (4 * p)%positive) as [i imaj], @@ -225,33 +225,27 @@ Proof. let (p, _) := cau (4 * n)%positive in proj1_sig (xn p) (4 * n)%positive) (Rcauchy_limit xn cau)) (2*p)) as H. - simpl (inject_Q - (proj1_sig - (exist (fun x : positive -> Q => QCauchySeq x id) - (fun n : positive => - let (p, _) := cau (4 * n)%positive in - proj1_sig (xn p) (4 * n)%positive) (Rcauchy_limit xn cau)) - (2 * p)%positive)) in H. + unfold proj1_sig in H. pose proof (cau (2*p)%positive) as [k cv]. - destruct (cau (p~0~0~0)%positive) as [i imaj]. + destruct (cau (4 * (2 * p))%positive) as [i imaj]. (* The convergence modulus does not matter here, because a converging Cauchy sequence always converges to its limit with twice the Cauchy modulus. *) exists (max k i). intros j H0. setoid_replace (xn j - - exist (fun x : positive -> Q => QCauchySeq x id) + exist (fun x : positive -> Q => QCauchySeq x) (fun n : positive => let (p0, _) := cau (4 * n)%positive in proj1_sig (xn p0) (4 * n)%positive) (Rcauchy_limit xn cau)) with (xn j - inject_Q (proj1_sig (xn i) (p~0~0~0)%positive) + (inject_Q (proj1_sig (xn i) (p~0~0~0)%positive) - - exist (fun x : positive -> Q => QCauchySeq x id) + exist (fun x : positive -> Q => QCauchySeq x) (fun n : positive => let (p0, _) := cau (4 * n)%positive in proj1_sig (xn p0) (4 * n)%positive) (Rcauchy_limit xn cau))). 2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)). apply (CReal_le_trans _ (inject_Q (1#2*p) + inject_Q (1#2*p))). - apply CReal_plus_le_compat. + apply CReal_plus_le_compat. unfold proj1_sig in H. 2: rewrite CReal_abs_minus_sym; exact H. specialize (imaj j i (le_trans _ _ _ (Nat.le_max_r _ _) H0) (le_refl _)). apply (CReal_le_trans _ (inject_Q (1 # 4 * p) + inject_Q (1 # 4 * p))). diff --git a/theories/Reals/Rregisternames.v b/theories/Reals/Rregisternames.v index f09edef600..8b078f2cf3 100644 --- a/theories/Reals/Rregisternames.v +++ b/theories/Reals/Rregisternames.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Reals. +Require Import Raxioms Rfunctions Qreals. (*****************************************************************) (** Register names for use in plugins *) @@ -18,6 +18,9 @@ Register R as reals.R.type. Register R0 as reals.R.R0. Register R1 as reals.R.R1. Register Rle as reals.R.Rle. +Register Rgt as reals.R.Rgt. +Register Rlt as reals.R.Rlt. +Register Rge as reals.R.Rge. Register Rplus as reals.R.Rplus. Register Ropp as reals.R.Ropp. Register Rminus as reals.R.Rminus. @@ -26,5 +29,6 @@ Register Rinv as reals.R.Rinv. Register Rdiv as reals.R.Rdiv. Register IZR as reals.R.IZR. Register Rabs as reals.R.Rabs. -Register sqrt as reals.R.sqrt. Register powerRZ as reals.R.powerRZ. +Register pow as reals.R.pow. +Register Qreals.Q2R as reals.R.Q2R. diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index fac9cd1d6d..31d9f7f0ed 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -154,7 +154,7 @@ Qed. Lemma CPermutation_length_1 : forall a b, CPermutation [a] [b] -> a = b. Proof. intros; now apply Permutation_length_1, CPermutation_Permutation. Qed. -Lemma CPermutation_length_1_inv : forall l a, CPermutation [a] l -> l = [a]. +Lemma CPermutation_length_1_inv : forall a l, CPermutation [a] l -> l = [a]. Proof. intros; now apply Permutation_length_1_inv, CPermutation_Permutation. Qed. Lemma CPermutation_swap : forall a b, CPermutation [a; b] [b; a]. @@ -235,9 +235,8 @@ induction m as [| b m]; intros l HC. apply CPermutation_nil in HC; inversion HC. - symmetry in HC. destruct (CPermutation_vs_cons_inv HC) as [m1 [m2 [-> Heq]]]. - apply map_eq_app in Heq as [l1 [l1' [-> [-> Heq]]]]. - symmetry in Heq. - apply map_eq_cons in Heq as [a [l1'' [-> [-> ->]]]]. + apply map_eq_app in Heq as [l1 [l1' [-> [<- Heq]]]]. + apply map_eq_cons in Heq as [a [l1'' [-> [<- <-]]]]. exists (a :: l1'' ++ l1); split. + now simpl; rewrite map_app. + now rewrite app_comm_cons. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index ffef8a216d..1dd9285412 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -552,7 +552,6 @@ Proof. - symmetry in HP. destruct (Permutation_vs_cons_inv HP) as [l3 [l4 Heq]]. destruct (map_eq_app _ _ _ _ Heq) as [l1' [l2' [Heq1 [Heq2 Heq3]]]]; subst. - symmetry in Heq3. destruct (map_eq_cons _ _ Heq3) as [b [l1'' [Heq1' [Heq2' Heq3']]]]; subst. rewrite map_app in HP; simpl in HP. symmetry in HP. diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index 0ad79825d2..adffa1ded4 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -13,14 +13,15 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -Require Import Orders PeanoNat POrderedType BinNat BinInt +Require Import Orders BoolOrder PeanoNat POrderedType BinNat BinInt RelationPairs EqualitiesFacts. (** * Examples of Ordered Type structures. *) -(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *) +(** Ordered Type for [bool], [nat], [Positive], [N], [Z] with the usual order. *) +Module Bool_as_OT := BoolOrder.BoolOrd. Module Nat_as_OT := PeanoNat.Nat. Module Positive_as_OT := BinPos.Pos. Module N_as_OT := BinNat.N. @@ -30,8 +31,9 @@ Module Z_as_OT := BinInt.Z. Module OT_as_DT (O:OrderedType) <: DecidableType := O. -(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) +(** (Usual) Decidable Type for [bool], [nat], [positive], [N], [Z] *) +Module Bool_as_DT <: UsualDecidableType := Bool_as_OT. Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. Module N_as_DT <: UsualDecidableType := N_as_OT. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 0b3656f586..78b26c83ea 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -44,6 +44,7 @@ Register succ as num.Z.succ. Register pred as num.Z.pred. Register sub as num.Z.sub. Register mul as num.Z.mul. +Register pow as num.Z.pow. Register of_nat as num.Z.of_nat. (** When including property functors, only inline t eq zero one two *) diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 55b9ec4a44..c05ed9ebf4 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -208,7 +208,7 @@ Definition gtb x y := | _ => false end. -Fixpoint eqb x y := +Definition eqb x y := match x, y with | 0, 0 => true | pos p, pos q => Pos.eqb p q diff --git a/theories/extraction/ExtrHaskellString.v b/theories/extraction/ExtrHaskellString.v index 8c61f4e96b..80f527f51b 100644 --- a/theories/extraction/ExtrHaskellString.v +++ b/theories/extraction/ExtrHaskellString.v @@ -8,6 +8,8 @@ Require Import Ascii. Require Import String. Require Import Coq.Strings.Byte. +Require Export ExtrHaskellBasic. + (** * At the moment, Coq's extraction has no way to add extra import * statements to the extracted Haskell code. You will have to @@ -35,19 +37,19 @@ Extract Inductive ascii => "Prelude.Char" (Data.Bits.testBit (Data.Char.ord a) 5) (Data.Bits.testBit (Data.Char.ord a) 6) (Data.Bits.testBit (Data.Char.ord a) 7))". -Extract Inlined Constant Ascii.ascii_dec => "(Prelude.==)". -Extract Inlined Constant Ascii.eqb => "(Prelude.==)". +Extract Inlined Constant Ascii.ascii_dec => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)". +Extract Inlined Constant Ascii.eqb => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)". Extract Inductive string => "Prelude.String" [ "([])" "(:)" ]. -Extract Inlined Constant String.string_dec => "(Prelude.==)". -Extract Inlined Constant String.eqb => "(Prelude.==)". +Extract Inlined Constant String.string_dec => "((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)". +Extract Inlined Constant String.eqb => "((Prelude.==) :: Prelude.String -> Prelude.String -> Prelude.Bool)". (* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *) Extract Inductive byte => "Prelude.Char" ["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"]. -Extract Inlined Constant Byte.eqb => "(Prelude.==)". -Extract Inlined Constant Byte.byte_eq_dec => "(Prelude.==)". +Extract Inlined Constant Byte.eqb => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)". +Extract Inlined Constant Byte.byte_eq_dec => "((Prelude.==) :: Prelude.Char -> Prelude.Char -> Prelude.Bool)". Extract Inlined Constant Ascii.ascii_of_byte => "(\x -> x)". Extract Inlined Constant Ascii.byte_of_ascii => "(\x -> x)". diff --git a/theories/extraction/ExtrOCamlFloats.v b/theories/extraction/ExtrOCamlFloats.v index 02f4b2898b..8d01620ef2 100644 --- a/theories/extraction/ExtrOCamlFloats.v +++ b/theories/extraction/ExtrOCamlFloats.v @@ -14,10 +14,10 @@ Note: the extraction of primitive floats relies on Coq's internal file kernel/float64.ml, so make sure the corresponding binary is available when linking the extracted OCaml code. -For example, if you build a (_CoqProject + coq_makefile)-based project +For example, if you build a ("_CoqProject" + coq_makefile)-based project and if you created an empty subfolder "extracted" and a file "test.v" containing [Cd "extracted". Separate Extraction function_to_extract.], -you will just need to add in the _CoqProject: [test.v], [-I extracted] +you will just need to add in the "_CoqProject" file: [test.v], [-I extracted] and the list of [extracted/*.ml] and [extracted/*.mli] files, then add [CAMLFLAGS += -w -33] in the Makefile.local file. *) diff --git a/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v index 7740bb41d9..29bd732c78 100644 --- a/theories/extraction/ExtrOcamlBigIntConv.v +++ b/theories/extraction/ExtrOcamlBigIntConv.v @@ -45,14 +45,14 @@ Fixpoint bigint_of_pos p := | xI p => bigint_succ (bigint_twice (bigint_of_pos p)) end. -Fixpoint bigint_of_z z := +Definition bigint_of_z z := match z with | Z0 => bigint_zero | Zpos p => bigint_of_pos p | Zneg p => bigint_opp (bigint_of_pos p) end. -Fixpoint bigint_of_n n := +Definition bigint_of_n n := match n with | N0 => bigint_zero | Npos p => bigint_of_pos p diff --git a/theories/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v index a5be08ece4..d9c88defa5 100644 --- a/theories/extraction/ExtrOcamlIntConv.v +++ b/theories/extraction/ExtrOcamlIntConv.v @@ -42,14 +42,14 @@ Fixpoint int_of_pos p := | xI p => int_succ (int_twice (int_of_pos p)) end. -Fixpoint int_of_z z := +Definition int_of_z z := match z with | Z0 => int_zero | Zpos p => int_of_pos p | Zneg p => int_opp (int_of_pos p) end. -Fixpoint int_of_n n := +Definition int_of_n n := match n with | N0 => int_zero | Npos p => int_of_pos p diff --git a/theories/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v index bd8490d796..2e50481b13 100644 --- a/theories/micromega/DeclConstant.v +++ b/theories/micromega/DeclConstant.v @@ -35,6 +35,7 @@ Require Import List. (** Ground terms (see [GT] below) are built inductively from declared constants. *) Class DeclaredConstant {T : Type} (F : T). +Register DeclaredConstant as micromega.DeclaredConstant.type. Class GT {T : Type} (F : T). diff --git a/theories/micromega/EnvRing.v b/theories/micromega/EnvRing.v index 28c7e8c554..7bef11e89a 100644 --- a/theories/micromega/EnvRing.v +++ b/theories/micromega/EnvRing.v @@ -31,6 +31,14 @@ Inductive PExpr {C} : Type := | PEpow : PExpr -> N -> PExpr. Arguments PExpr : clear implicits. +Register PEc as micromega.PExpr.PEc. +Register PEX as micromega.PExpr.PEX. +Register PEadd as micromega.PExpr.PEadd. +Register PEsub as micromega.PExpr.PEsub. +Register PEmul as micromega.PExpr.PEmul. +Register PEopp as micromega.PExpr.PEopp. +Register PEpow as micromega.PExpr.PEpow. + (* Definition of multivariable polynomials with coefficients in C : Type [Pol] represents [X1 ... Xn]. The representation is Horner's where a [n] variable polynomial @@ -60,6 +68,10 @@ Inductive Pol {C} : Type := | PX : Pol -> positive -> Pol -> Pol. Arguments Pol : clear implicits. +Register Pc as micromega.Pol.Pc. +Register Pinj as micromega.Pol.Pinj. +Register PX as micromega.Pol.PX. + Section MakeRingPol. (* Ring elements *) diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v index 22cef50e0d..5c8cece845 100644 --- a/theories/micromega/Lra.v +++ b/theories/micromega/Lra.v @@ -20,6 +20,7 @@ Require Import Rdefinitions. Require Import RingMicromega. Require Import VarMap. Require Coq.micromega.Tauto. +Require Import Rregisternames. Declare ML Module "micromega_plugin". Ltac rchange := diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v index e28de1a620..1fbc5a648a 100644 --- a/theories/micromega/QMicromega.v +++ b/theories/micromega/QMicromega.v @@ -154,6 +154,9 @@ Qed. Definition QWitness := Psatz Q. +Register QWitness as micromega.QWitness.type. + + Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qeq_bool Qle_bool. Require Import List. diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v index a67c273c7f..fd8903eac9 100644 --- a/theories/micromega/RMicromega.v +++ b/theories/micromega/RMicromega.v @@ -150,7 +150,17 @@ Inductive Rcst := | CInv (r : Rcst) | COpp (r : Rcst). - +Register Rcst as micromega.Rcst.type. +Register C0 as micromega.Rcst.C0. +Register C1 as micromega.Rcst.C1. +Register CQ as micromega.Rcst.CQ. +Register CZ as micromega.Rcst.CZ. +Register CPlus as micromega.Rcst.CPlus. +Register CMinus as micromega.Rcst.CMinus. +Register CMult as micromega.Rcst.CMult. +Register CPow as micromega.Rcst.CPow. +Register CInv as micromega.Rcst.CInv. +Register COpp as micromega.Rcst.COpp. Definition z_of_exp (z : Z + nat) := match z with diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v index 04de9509ac..fb7fbcf80b 100644 --- a/theories/micromega/RingMicromega.v +++ b/theories/micromega/RingMicromega.v @@ -298,6 +298,15 @@ Inductive Psatz : Type := | PsatzC : C -> Psatz | PsatzZ : Psatz. +Register PsatzIn as micromega.Psatz.PsatzIn. +Register PsatzSquare as micromega.Psatz.PsatzSquare. +Register PsatzMulC as micromega.Psatz.PsatzMulC. +Register PsatzMulE as micromega.Psatz.PsatzMulE. +Register PsatzAdd as micromega.Psatz.PsatzAdd. +Register PsatzC as micromega.Psatz.PsatzC. +Register PsatzZ as micromega.Psatz.PsatzZ. + + (** Given a list [l] of NFormula and an extended polynomial expression [e], if [eval_Psatz l e] succeeds (= Some f) then [f] is a logic consequence of the conjunction of the formulae in l. @@ -672,6 +681,13 @@ Inductive Op2 : Set := (* binary relations *) | OpLt | OpGt. +Register OpEq as micromega.Op2.OpEq. +Register OpNEq as micromega.Op2.OpNEq. +Register OpLe as micromega.Op2.OpLe. +Register OpGe as micromega.Op2.OpGe. +Register OpLt as micromega.Op2.OpLt. +Register OpGt as micromega.Op2.OpGt. + Definition eval_op2 (o : Op2) : R -> R -> Prop := match o with | OpEq => req @@ -686,12 +702,15 @@ Definition eval_pexpr : PolEnv -> PExpr C -> R := PEeval rplus rtimes rminus ropp phi pow_phi rpow. #[universes(template)] -Record Formula (T:Type) : Type := { +Record Formula (T:Type) : Type := Build_Formula{ Flhs : PExpr T; Fop : Op2; Frhs : PExpr T }. +Register Formula as micromega.Formula.type. +Register Build_Formula as micromega.Formula.Build_Formula. + Definition eval_formula (env : PolEnv) (f : Formula C) : Prop := let (lhs, op, rhs) := f in (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs). diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index a3e3cc3e9d..6e89089355 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -37,6 +37,16 @@ Section S. | N : GFormula -> GFormula | I : GFormula -> option AF -> GFormula -> GFormula. + Register TT as micromega.GFormula.TT. + Register FF as micromega.GFormula.FF. + Register X as micromega.GFormula.X. + Register A as micromega.GFormula.A. + Register Cj as micromega.GFormula.Cj. + Register D as micromega.GFormula.D. + Register N as micromega.GFormula.N. + Register I as micromega.GFormula.I. + + Section MAPX. Variable F : TX -> TX. @@ -137,6 +147,8 @@ End S. (** Typical boolean formulae *) Definition BFormula (A : Type) := @GFormula A Prop unit unit. +Register BFormula as micromega.BFormula.type. + Section MAPATOMS. Context {TA TA':Type}. Context {TX : Type}. diff --git a/theories/micromega/VarMap.v b/theories/micromega/VarMap.v index c2472f6303..e28c27f400 100644 --- a/theories/micromega/VarMap.v +++ b/theories/micromega/VarMap.v @@ -33,6 +33,11 @@ Inductive t {A} : Type := | Branch : t -> A -> t -> t . Arguments t : clear implicits. +Register Branch as micromega.VarMap.Branch. +Register Elt as micromega.VarMap.Elt. +Register Empty as micromega.VarMap.Empty. +Register t as micromega.VarMap.type. + Section MakeVarMap. Variable A : Type. diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v index efb263faf3..bff9671fee 100644 --- a/theories/micromega/ZMicromega.v +++ b/theories/micromega/ZMicromega.v @@ -564,10 +564,14 @@ Inductive ZArithProof := . (*| SplitProof : PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*) +Register ZArithProof as micromega.ZArithProof.type. +Register DoneProof as micromega.ZArithProof.DoneProof. +Register RatProof as micromega.ZArithProof.RatProof. +Register CutProof as micromega.ZArithProof.CutProof. +Register EnumProof as micromega.ZArithProof.EnumProof. +Register ExProof as micromega.ZArithProof.ExProof. -(* n/d <= x -> d*x - n >= 0 *) - (* In order to compute the 'cut', we need to express a polynomial P as a * Q + b. - b is the constant diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index 521ac61e18..5b15dc072a 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -42,6 +42,9 @@ Instance Op_lt : BinRel lt := {| TR := Z.lt; TRInj := Nat2Z.inj_lt |}. Add BinRel Op_lt. +Instance Op_Nat_lt : BinRel Nat.lt := Op_lt. +Add BinRel Op_Nat_lt. + Instance Op_gt : BinRel gt := {| TR := Z.gt; TRInj := Nat2Z.inj_gt |}. Add BinRel Op_gt. @@ -50,10 +53,16 @@ Instance Op_le : BinRel le := {| TR := Z.le; TRInj := Nat2Z.inj_le |}. Add BinRel Op_le. +Instance Op_Nat_le : BinRel Nat.le := Op_le. +Add BinRel Op_Nat_le. + Instance Op_eq_nat : BinRel (@eq nat) := {| TR := @eq Z ; TRInj := fun x y : nat => iff_sym (Nat2Z.inj_iff x y) |}. Add BinRel Op_eq_nat. +Instance Op_Nat_eq : BinRel (Nat.eq) := Op_eq_nat. +Add BinRel Op_Nat_eq. + (* zify_nat_op *) Instance Op_plus : BinOp Nat.add := {| TBOp := Z.add; TBOpInj := Nat2Z.inj_add |}. diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v index 93b84f3a02..70180f47c7 100644 --- a/theories/nsatz/Nsatz.v +++ b/theories/nsatz/Nsatz.v @@ -9,9 +9,9 @@ (************************************************************************) (* - Tactic nsatz: proofs of polynomials equalities in an integral domain + Tactic nsatz: proofs of polynomials equalities in an integral domain (commutative ring without zero divisor). - + Examples: see test-suite/success/Nsatz.v Reification is done using type classes, defined in Ncring_tac.v @@ -33,416 +33,9 @@ Require Import DiscrR. Require Import ZArith. Require Import Lia. -Declare ML Module "nsatz_plugin". - -Section nsatz1. - -Context {R:Type}`{Rid:Integral_domain R}. - -Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y. -intros x y H; setoid_replace x with ((x - y) + y); simpl; - [setoid_rewrite H | idtac]; simpl. cring. cring. -Qed. - -Lemma psos_r1: forall x y, x == y -> x - y == 0. -intros x y H; simpl; setoid_rewrite H; simpl; cring. -Qed. - -Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0). -intros. -intro; apply H. -simpl; setoid_replace x with ((x - y) + y). simpl. -setoid_rewrite H0. -simpl; cring. -simpl. simpl; cring. -Qed. - -(* adpatation du code de Benjamin aux setoides *) -Export Ring_polynom. -Export InitialRing. - -Definition PolZ := Pol Z. -Definition PEZ := PExpr Z. - -Definition P0Z : PolZ := P0 (C:=Z) 0%Z. - -Definition PolZadd : PolZ -> PolZ -> PolZ := - @Padd Z 0%Z Z.add Zeq_bool. - -Definition PolZmul : PolZ -> PolZ -> PolZ := - @Pmul Z 0%Z 1%Z Z.add Z.mul Zeq_bool. - -Definition PolZeq := @Peq Z Zeq_bool. - -Definition norm := - @norm_aux Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool. - -Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := - match la, lp with - | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp) - | _, _ => P0Z - end. - -Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := - match lla with - | List.nil => lp - | la::lla => compute_list lla ((mult_l la lp)::lp) - end. - -Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := - let (lla, lq) := certif in - let lp := List.map norm lpe in - PolZeq (norm qe) (mult_l lq (compute_list lla lp)). - - -(* Correction *) -Definition PhiR : list R -> PolZ -> R := - (Pphi ring0 add mul - (InitialRing.gen_phiZ ring0 ring1 add mul opp)). - -Definition PEevalR : list R -> PEZ -> R := - PEeval ring0 ring1 add mul sub opp - (gen_phiZ ring0 ring1 add mul opp) - N.to_nat pow. - -Lemma P0Z_correct : forall l, PhiR l P0Z = 0. -Proof. trivial. Qed. - -Lemma Rext: ring_eq_ext add mul opp _==_. -Proof. -constructor; solve_proper. -Qed. - -Lemma Rset : Setoid_Theory R _==_. -apply ring_setoid. -Qed. - -Definition Rtheory:ring_theory ring0 ring1 add mul sub opp _==_. -apply mk_rt. -apply ring_add_0_l. -apply ring_add_comm. -apply ring_add_assoc. -apply ring_mul_1_l. -apply cring_mul_comm. -apply ring_mul_assoc. -apply ring_distr_l. -apply ring_sub_def. -apply ring_opp_def. -Defined. - -Lemma PolZadd_correct : forall P' P l, - PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')). -Proof. -unfold PolZadd, PhiR. intros. simpl. - refine (Padd_ok Rset Rext (Rth_ARth Rset Rext Rtheory) - (gen_phiZ_morph Rset Rext Rtheory) _ _ _). -Qed. - -Lemma PolZmul_correct : forall P P' l, - PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')). -Proof. -unfold PolZmul, PhiR. intros. - refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext Rtheory) - (gen_phiZ_morph Rset Rext Rtheory) _ _ _). -Qed. - -Lemma R_power_theory - : Ring_theory.power_theory ring1 mul _==_ N.to_nat pow. -apply Ring_theory.mkpow_th. unfold pow. intros. rewrite Nnat.N2Nat.id. -reflexivity. Qed. - -Lemma norm_correct : - forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). -Proof. - intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext Rtheory) - (gen_phiZ_morph Rset Rext Rtheory) R_power_theory). -Qed. - -Lemma PolZeq_correct : forall P P' l, - PolZeq P P' = true -> - PhiR l P == PhiR l P'. -Proof. - intros;apply - (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext Rtheory));trivial. -Qed. - -Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := - match l with - | List.nil => True - | a::l => Interp a == 0 /\ Cond0 A Interp l - end. - -Lemma mult_l_correct : forall l la lp, - Cond0 PolZ (PhiR l) lp -> - PhiR l (mult_l la lp) == 0. -Proof. - induction la;simpl;intros. cring. - destruct lp;trivial. simpl. cring. - simpl in H;destruct H. - rewrite PolZadd_correct. - simpl. rewrite PolZmul_correct. simpl. rewrite H. - rewrite IHla. cring. trivial. -Qed. - -Lemma compute_list_correct : forall l lla lp, - Cond0 PolZ (PhiR l) lp -> - Cond0 PolZ (PhiR l) (compute_list lla lp). -Proof. - induction lla;simpl;intros;trivial. - apply IHlla;simpl;split;trivial. - apply mult_l_correct;trivial. -Qed. - -Lemma check_correct : - forall l lpe qe certif, - check lpe qe certif = true -> - Cond0 PEZ (PEevalR l) lpe -> - PEevalR l qe == 0. -Proof. - unfold check;intros l lpe qe (lla, lq) H2 H1. - apply PolZeq_correct with (l:=l) in H2. - rewrite norm_correct, H2. - apply mult_l_correct. - apply compute_list_correct. - clear H2 lq lla qe;induction lpe;simpl;trivial. - simpl in H1;destruct H1. - rewrite <- norm_correct;auto. -Qed. - -(* fin *) - -Definition R2:= 1 + 1. - -Fixpoint IPR p {struct p}: R := - match p with - xH => ring1 - | xO xH => 1+1 - | xO p1 => R2*(IPR p1) - | xI xH => 1+(1+1) - | xI p1 => 1+(R2*(IPR p1)) - end. - -Definition IZR1 z := - match z with Z0 => 0 - | Zpos p => IPR p - | Zneg p => -(IPR p) - end. - -Fixpoint interpret3 t fv {struct t}: R := - match t with - | (PEadd t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 + v2) - | (PEmul t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 * v2) - | (PEsub t1 t2) => - let v1 := interpret3 t1 fv in - let v2 := interpret3 t2 fv in (v1 - v2) - | (PEopp t1) => - let v1 := interpret3 t1 fv in (-v1) - | (PEpow t1 t2) => - let v1 := interpret3 t1 fv in pow v1 (N.to_nat t2) - | (PEc t1) => (IZR1 t1) - | PEO => 0 - | PEI => 1 - | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0 - end. - - -End nsatz1. - -Ltac equality_to_goal H x y:= - (* eliminate trivial hypotheses, but it takes time!: - let h := fresh "nH" in - (assert (h:equality x y); - [solve [cring] | clear H; clear h]) - || *) try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) -. - -Ltac equalities_to_goal := - lazymatch goal with - | H: (_ ?x ?y) |- _ => equality_to_goal H x y - | H: (_ _ ?x ?y) |- _ => equality_to_goal H x y - | H: (_ _ _ ?x ?y) |- _ => equality_to_goal H x y - | H: (_ _ _ _ ?x ?y) |- _ => equality_to_goal H x y -(* extension possible :-) *) - | H: (?x == ?y) |- _ => equality_to_goal H x y - end. - -(* lp est incluse dans fv. La met en tete. *) - -Ltac parametres_en_tete fv lp := - match fv with - | (@nil _) => lp - | (@cons _ ?x ?fv1) => - let res := AddFvTail x lp in - parametres_en_tete fv1 res - end. - -Ltac append1 a l := - match l with - | (@nil _) => constr:(cons a l) - | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l') - end. - -Ltac rev l := - match l with - |(@nil _) => l - | (cons ?x ?l) => let l' := rev l in append1 x l' - end. - -Ltac nsatz_call_n info nparam p rr lp kont := -(* idtac "Trying power: " rr;*) - let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in -(* idtac "calcul...";*) - nsatz_compute ll; -(* idtac "done";*) - match goal with - | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => - intros _; - let lci := fresh "lci" in - set (lci:=lci0); - let lq := fresh "lq" in - set (lq:=lq0); - kont c rr lq lci - end. - -Ltac nsatz_call radicalmax info nparam p lp kont := - let rec try_n n := - lazymatch n with - | 0%N => fail - | _ => - (let r := eval compute in (N.sub radicalmax (N.pred n)) in - nsatz_call_n info nparam p r lp kont) || - let n' := eval compute in (N.pred n) in try_n n' - end in - try_n radicalmax. - - -Ltac lterm_goal g := - match g with - ?b1 == ?b2 => constr:(b1::b2::nil) - | ?b1 == ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) - end. - -Ltac reify_goal l le lb:= - match le with - nil => idtac - | ?e::?le1 => - match lb with - ?b::?lb1 => (* idtac "b="; idtac b;*) - let x := fresh "B" in - set (x:= b) at 1; - change x with (interpret3 e l); - clear x; - reify_goal l le1 lb1 - end - end. - -Ltac get_lpol g := - match g with - (interpret3 ?p _) == _ => constr:(p::nil) - | (interpret3 ?p _) == _ -> ?g => - let l := get_lpol g in constr:(p::l) - end. - -Ltac nsatz_generic radicalmax info lparam lvar := - let nparam := eval compute in (Z.of_nat (List.length lparam)) in - match goal with - |- ?g => let lb := lterm_goal g in - match (match lvar with - |(@nil _) => - match lparam with - |(@nil _) => - let r := eval red in (list_reifyl (lterm:=lb)) in r - |_ => - match eval red in (list_reifyl (lterm:=lb)) with - |(?fv, ?le) => - let fv := parametres_en_tete fv lparam in - (* we reify a second time, with the good order - for variables *) - let r := eval red in - (list_reifyl (lterm:=lb) (lvar:=fv)) in r - end - end - |_ => - let fv := parametres_en_tete lvar lparam in - let r := eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) in r - end) with - |(?fv, ?le) => - reify_goal fv le lb ; - match goal with - |- ?g => - let lp := get_lpol g in - let lpol := eval compute in (List.rev lp) in - intros; - - let SplitPolyList kont := - match lpol with - | ?p2::?lp2 => kont p2 lp2 - | _ => idtac "polynomial not in the ideal" - end in - - SplitPolyList ltac:(fun p lp => - let p21 := fresh "p21" in - let lp21 := fresh "lp21" in - set (p21:=p) ; - set (lp21:=lp); -(* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) - nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => - let q := fresh "q" in - set (q := PEmul c (PEpow p21 r)); - let Hg := fresh "Hg" in - assert (Hg:check lp21 q (lci,lq) = true); - [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" - | let Hg2 := fresh "Hg" in - assert (Hg2: (interpret3 q fv) == 0); - [ (*simpl*) idtac; - generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg); - let cc := fresh "H" in - (*simpl*) idtac; intro cc; apply cc; clear cc; - (*simpl*) idtac; - repeat (split;[assumption|idtac]); exact I - | (*simpl in Hg2;*) (*simpl*) idtac; - apply Rintegral_domain_pow with (interpret3 c fv) (N.to_nat r); - (*simpl*) idtac; - try apply integral_domain_one_zero; - try apply integral_domain_minus_one_zero; - try trivial; - try exact integral_domain_one_zero; - try exact integral_domain_minus_one_zero - || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation, - one, one_notation, multiplication, mul_notation, zero, zero_notation; - discrR || lia ]) - || ((*simpl*) idtac) || idtac "could not prove discrimination result" - ] - ] -) -) -end end end . - -Ltac nsatz_default:= - intros; - try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); - match goal with |- (@equality ?r _ _ _) => - repeat equalities_to_goal; - nsatz_generic 6%N 1%Z (@nil r) (@nil r) - end. - -Tactic Notation "nsatz" := nsatz_default. - -Tactic Notation "nsatz" "with" - "radicalmax" ":=" constr(radicalmax) - "strategy" ":=" constr(info) - "parameters" ":=" constr(lparam) - "variables" ":=" constr(lvar):= - intros; - try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); - match goal with |- (@equality ?r _ _ _) => - repeat equalities_to_goal; - nsatz_generic radicalmax info lparam lvar - end. +Require Export NsatzTactic. +(** Make use of [discrR] in [nsatz] *) +Ltac nsatz_internal_discrR ::= discrR. (* Real numbers *) Require Import Reals. @@ -462,7 +55,7 @@ try (try apply Rsth; intros; try rewrite H; try rewrite H0; reflexivity)). exact Rplus_0_l. exact Rplus_comm. symmetry. apply Rplus_assoc. exact Rmult_1_l. exact Rmult_1_r. symmetry. apply Rmult_assoc. - exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l. + exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l. exact Rplus_opp_r. Defined. @@ -479,8 +72,8 @@ Qed. Instance Rcri: (Cring (Rr:=Rri)). red. exact Rmult_comm. Defined. -Instance Rdi : (Integral_domain (Rcr:=Rcri)). -constructor. +Instance Rdi : (Integral_domain (Rcr:=Rcri)). +constructor. exact Rmult_integral. exact R_one_zero. Defined. (* Rational numbers *) @@ -491,14 +84,14 @@ Defined. Instance Qri : (Ring (Ro:=Qops)). constructor. -try apply Q_Setoid. -apply Qplus_comp. -apply Qmult_comp. -apply Qminus_comp. +try apply Q_Setoid. +apply Qplus_comp. +apply Qmult_comp. +apply Qminus_comp. apply Qopp_comp. exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc. exact Qmult_1_l. exact Qmult_1_r. apply Qmult_assoc. - apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. + apply Qmult_plus_distr_l. intros. apply Qmult_plus_distr_r. reflexivity. exact Qplus_opp_r. Defined. @@ -508,8 +101,8 @@ Proof. unfold Qeq. simpl. lia. Qed. Instance Qcri: (Cring (Rr:=Qri)). red. exact Qmult_comm. Defined. -Instance Qdi : (Integral_domain (Rcr:=Qcri)). -constructor. +Instance Qdi : (Integral_domain (Rcr:=Qcri)). +constructor. exact Qmult_integral. exact Q_one_zero. Defined. (* Integers *) @@ -519,7 +112,6 @@ Proof. lia. Qed. Instance Zcri: (Cring (Rr:=Zr)). red. exact Z.mul_comm. Defined. -Instance Zdi : (Integral_domain (Rcr:=Zcri)). -constructor. +Instance Zdi : (Integral_domain (Rcr:=Zcri)). +constructor. exact Zmult_integral. exact Z_one_zero. Defined. - diff --git a/theories/nsatz/NsatzTactic.v b/theories/nsatz/NsatzTactic.v new file mode 100644 index 0000000000..db7dab2c46 --- /dev/null +++ b/theories/nsatz/NsatzTactic.v @@ -0,0 +1,449 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* + Tactic nsatz: proofs of polynomials equalities in an integral domain +(commutative ring without zero divisor). + +Examples: see test-suite/success/Nsatz.v + +Reification is done using type classes, defined in Ncring_tac.v + +*) + +Require Import List. +Require Import Setoid. +Require Import BinPos. +Require Import BinList. +Require Import Znumtheory. +Require Export Morphisms Setoid Bool. +Require Export Algebra_syntax. +Require Export Ncring. +Require Export Ncring_initial. +Require Export Ncring_tac. +Require Export Integral_domain. +Require Import ZArith. +Require Import Lia. + +Declare ML Module "nsatz_plugin". + +Section nsatz1. + +Context {R:Type}`{Rid:Integral_domain R}. + +Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y. +intros x y H; setoid_replace x with ((x - y) + y); simpl; + [setoid_rewrite H | idtac]; simpl. cring. cring. +Qed. + +Lemma psos_r1: forall x y, x == y -> x - y == 0. +intros x y H; simpl; setoid_rewrite H; simpl; cring. +Qed. + +Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0). +intros. +intro; apply H. +simpl; setoid_replace x with ((x - y) + y). simpl. +setoid_rewrite H0. +simpl; cring. +simpl. simpl; cring. +Qed. + +(* adpatation du code de Benjamin aux setoides *) +Export Ring_polynom. +Export InitialRing. + +Definition PolZ := Pol Z. +Definition PEZ := PExpr Z. + +Definition P0Z : PolZ := P0 (C:=Z) 0%Z. + +Definition PolZadd : PolZ -> PolZ -> PolZ := + @Padd Z 0%Z Z.add Zeq_bool. + +Definition PolZmul : PolZ -> PolZ -> PolZ := + @Pmul Z 0%Z 1%Z Z.add Z.mul Zeq_bool. + +Definition PolZeq := @Peq Z Zeq_bool. + +Definition norm := + @norm_aux Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool. + +Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ := + match la, lp with + | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp) + | _, _ => P0Z + end. + +Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) := + match lla with + | List.nil => lp + | la::lla => compute_list lla ((mult_l la lp)::lp) + end. + +Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) := + let (lla, lq) := certif in + let lp := List.map norm lpe in + PolZeq (norm qe) (mult_l lq (compute_list lla lp)). + + +(* Correction *) +Definition PhiR : list R -> PolZ -> R := + (Pphi ring0 add mul + (InitialRing.gen_phiZ ring0 ring1 add mul opp)). + +Definition PEevalR : list R -> PEZ -> R := + PEeval ring0 ring1 add mul sub opp + (gen_phiZ ring0 ring1 add mul opp) + N.to_nat pow. + +Lemma P0Z_correct : forall l, PhiR l P0Z = 0. +Proof. trivial. Qed. + +Lemma Rext: ring_eq_ext add mul opp _==_. +Proof. +constructor; solve_proper. +Qed. + +Lemma Rset : Setoid_Theory R _==_. +apply ring_setoid. +Qed. + +Definition Rtheory:ring_theory ring0 ring1 add mul sub opp _==_. +apply mk_rt. +apply ring_add_0_l. +apply ring_add_comm. +apply ring_add_assoc. +apply ring_mul_1_l. +apply cring_mul_comm. +apply ring_mul_assoc. +apply ring_distr_l. +apply ring_sub_def. +apply ring_opp_def. +Defined. + +Lemma PolZadd_correct : forall P' P l, + PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')). +Proof. +unfold PolZadd, PhiR. intros. simpl. + refine (Padd_ok Rset Rext (Rth_ARth Rset Rext Rtheory) + (gen_phiZ_morph Rset Rext Rtheory) _ _ _). +Qed. + +Lemma PolZmul_correct : forall P P' l, + PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')). +Proof. +unfold PolZmul, PhiR. intros. + refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext Rtheory) + (gen_phiZ_morph Rset Rext Rtheory) _ _ _). +Qed. + +Lemma R_power_theory + : Ring_theory.power_theory ring1 mul _==_ N.to_nat pow. +apply Ring_theory.mkpow_th. unfold pow. intros. rewrite Nnat.N2Nat.id. +reflexivity. Qed. + +Lemma norm_correct : + forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe). +Proof. + intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext Rtheory) + (gen_phiZ_morph Rset Rext Rtheory) R_power_theory). +Qed. + +Lemma PolZeq_correct : forall P P' l, + PolZeq P P' = true -> + PhiR l P == PhiR l P'. +Proof. + intros;apply + (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext Rtheory));trivial. +Qed. + +Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop := + match l with + | List.nil => True + | a::l => Interp a == 0 /\ Cond0 A Interp l + end. + +Lemma mult_l_correct : forall l la lp, + Cond0 PolZ (PhiR l) lp -> + PhiR l (mult_l la lp) == 0. +Proof. + induction la;simpl;intros. cring. + destruct lp;trivial. simpl. cring. + simpl in H;destruct H. + rewrite PolZadd_correct. + simpl. rewrite PolZmul_correct. simpl. rewrite H. + rewrite IHla. cring. trivial. +Qed. + +Lemma compute_list_correct : forall l lla lp, + Cond0 PolZ (PhiR l) lp -> + Cond0 PolZ (PhiR l) (compute_list lla lp). +Proof. + induction lla;simpl;intros;trivial. + apply IHlla;simpl;split;trivial. + apply mult_l_correct;trivial. +Qed. + +Lemma check_correct : + forall l lpe qe certif, + check lpe qe certif = true -> + Cond0 PEZ (PEevalR l) lpe -> + PEevalR l qe == 0. +Proof. + unfold check;intros l lpe qe (lla, lq) H2 H1. + apply PolZeq_correct with (l:=l) in H2. + rewrite norm_correct, H2. + apply mult_l_correct. + apply compute_list_correct. + clear H2 lq lla qe;induction lpe;simpl;trivial. + simpl in H1;destruct H1. + rewrite <- norm_correct;auto. +Qed. + +(* fin *) + +Definition R2:= 1 + 1. + +Fixpoint IPR p {struct p}: R := + match p with + xH => ring1 + | xO xH => 1+1 + | xO p1 => R2*(IPR p1) + | xI xH => 1+(1+1) + | xI p1 => 1+(R2*(IPR p1)) + end. + +Definition IZR1 z := + match z with Z0 => 0 + | Zpos p => IPR p + | Zneg p => -(IPR p) + end. + +Fixpoint interpret3 t fv {struct t}: R := + match t with + | (PEadd t1 t2) => + let v1 := interpret3 t1 fv in + let v2 := interpret3 t2 fv in (v1 + v2) + | (PEmul t1 t2) => + let v1 := interpret3 t1 fv in + let v2 := interpret3 t2 fv in (v1 * v2) + | (PEsub t1 t2) => + let v1 := interpret3 t1 fv in + let v2 := interpret3 t2 fv in (v1 - v2) + | (PEopp t1) => + let v1 := interpret3 t1 fv in (-v1) + | (PEpow t1 t2) => + let v1 := interpret3 t1 fv in pow v1 (N.to_nat t2) + | (PEc t1) => (IZR1 t1) + | PEO => 0 + | PEI => 1 + | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0 + end. + + +End nsatz1. + +Ltac equality_to_goal H x y:= + (* eliminate trivial hypotheses, but it takes time!: + let h := fresh "nH" in + (assert (h:equality x y); + [solve [cring] | clear H; clear h]) + || *) try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) +. + +Ltac equalities_to_goal := + lazymatch goal with + | H: (_ ?x ?y) |- _ => equality_to_goal H x y + | H: (_ _ ?x ?y) |- _ => equality_to_goal H x y + | H: (_ _ _ ?x ?y) |- _ => equality_to_goal H x y + | H: (_ _ _ _ ?x ?y) |- _ => equality_to_goal H x y +(* extension possible :-) *) + | H: (?x == ?y) |- _ => equality_to_goal H x y + end. + +(* lp est incluse dans fv. La met en tete. *) + +Ltac parametres_en_tete fv lp := + match fv with + | (@nil _) => lp + | (@cons _ ?x ?fv1) => + let res := AddFvTail x lp in + parametres_en_tete fv1 res + end. + +Ltac append1 a l := + match l with + | (@nil _) => constr:(cons a l) + | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l') + end. + +Ltac rev l := + match l with + |(@nil _) => l + | (cons ?x ?l) => let l' := rev l in append1 x l' + end. + +Ltac nsatz_call_n info nparam p rr lp kont := +(* idtac "Trying power: " rr;*) + let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in +(* idtac "calcul...";*) + nsatz_compute ll; +(* idtac "done";*) + match goal with + | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => + intros _; + let lci := fresh "lci" in + set (lci:=lci0); + let lq := fresh "lq" in + set (lq:=lq0); + kont c rr lq lci + end. + +Ltac nsatz_call radicalmax info nparam p lp kont := + let rec try_n n := + lazymatch n with + | 0%N => fail + | _ => + (let r := eval compute in (N.sub radicalmax (N.pred n)) in + nsatz_call_n info nparam p r lp kont) || + let n' := eval compute in (N.pred n) in try_n n' + end in + try_n radicalmax. + + +Ltac lterm_goal g := + match g with + ?b1 == ?b2 => constr:(b1::b2::nil) + | ?b1 == ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l) + end. + +Ltac reify_goal l le lb:= + match le with + nil => idtac + | ?e::?le1 => + match lb with + ?b::?lb1 => (* idtac "b="; idtac b;*) + let x := fresh "B" in + set (x:= b) at 1; + change x with (interpret3 e l); + clear x; + reify_goal l le1 lb1 + end + end. + +Ltac get_lpol g := + match g with + (interpret3 ?p _) == _ => constr:(p::nil) + | (interpret3 ?p _) == _ -> ?g => + let l := get_lpol g in constr:(p::l) + end. + +(** We only make use of [discrR] if [nsatz] support for reals is + loaded. To do this, we redefine this tactic in Nsatz.v to make + use of real discrimination. *) +Ltac nsatz_internal_discrR := idtac. + +Ltac nsatz_generic radicalmax info lparam lvar := + let nparam := eval compute in (Z.of_nat (List.length lparam)) in + match goal with + |- ?g => let lb := lterm_goal g in + match (match lvar with + |(@nil _) => + match lparam with + |(@nil _) => + let r := eval red in (list_reifyl (lterm:=lb)) in r + |_ => + match eval red in (list_reifyl (lterm:=lb)) with + |(?fv, ?le) => + let fv := parametres_en_tete fv lparam in + (* we reify a second time, with the good order + for variables *) + let r := eval red in + (list_reifyl (lterm:=lb) (lvar:=fv)) in r + end + end + |_ => + let fv := parametres_en_tete lvar lparam in + let r := eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) in r + end) with + |(?fv, ?le) => + reify_goal fv le lb ; + match goal with + |- ?g => + let lp := get_lpol g in + let lpol := eval compute in (List.rev lp) in + intros; + + let SplitPolyList kont := + match lpol with + | ?p2::?lp2 => kont p2 lp2 + | _ => idtac "polynomial not in the ideal" + end in + + SplitPolyList ltac:(fun p lp => + let p21 := fresh "p21" in + let lp21 := fresh "lp21" in + set (p21:=p) ; + set (lp21:=lp); +(* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) + nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + let q := fresh "q" in + set (q := PEmul c (PEpow p21 r)); + let Hg := fresh "Hg" in + assert (Hg:check lp21 q (lci,lq) = true); + [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate" + | let Hg2 := fresh "Hg" in + assert (Hg2: (interpret3 q fv) == 0); + [ (*simpl*) idtac; + generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg); + let cc := fresh "H" in + (*simpl*) idtac; intro cc; apply cc; clear cc; + (*simpl*) idtac; + repeat (split;[assumption|idtac]); exact I + | (*simpl in Hg2;*) (*simpl*) idtac; + apply Rintegral_domain_pow with (interpret3 c fv) (N.to_nat r); + (*simpl*) idtac; + try apply integral_domain_one_zero; + try apply integral_domain_minus_one_zero; + try trivial; + try exact integral_domain_one_zero; + try exact integral_domain_minus_one_zero + || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation, + one, one_notation, multiplication, mul_notation, zero, zero_notation; + nsatz_internal_discrR || lia ]) + || ((*simpl*) idtac) || idtac "could not prove discrimination result" + ] + ] +) +) +end end end . + +Ltac nsatz_default:= + intros; + try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); + match goal with |- (@equality ?r _ _ _) => + repeat equalities_to_goal; + nsatz_generic 6%N 1%Z (@nil r) (@nil r) + end. + +Tactic Notation "nsatz" := nsatz_default. + +Tactic Notation "nsatz" "with" + "radicalmax" ":=" constr(radicalmax) + "strategy" ":=" constr(info) + "parameters" ":=" constr(lparam) + "variables" ":=" constr(lvar):= + intros; + try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _); + match goal with |- (@equality ?r _ _ _) => + repeat equalities_to_goal; + nsatz_generic radicalmax info lparam lvar + end. |