diff options
Diffstat (limited to 'theories')
36 files changed, 795 insertions, 502 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..c3c69f46f3 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -517,18 +517,20 @@ Section Elts. exists (a::l1); exists l2; simpl; split; now f_equal. Qed. - Lemma nth_ext : forall l l' d, length l = length l' -> - (forall n, nth n l d = nth n l' d) -> l = l'. + Lemma nth_ext : forall l l' d d', length l = length l' -> + (forall n, n < length l -> nth n l d = nth n l' d') -> l = l'. Proof. - induction l; intros l' d Hlen Hnth; destruct l' as [| b l']. + induction l; intros l' d d' Hlen Hnth; destruct l' as [| b l']. - reflexivity. - inversion Hlen. - inversion Hlen. - change a with (nth 0 (a :: l) d). - change b with (nth 0 (b :: l') d). + change b with (nth 0 (b :: l') d'). rewrite Hnth; f_equal. - apply IHl with d; [ now inversion Hlen | ]. - intros n; apply (Hnth (S n)). + + apply IHl with d d'; [ now inversion Hlen | ]. + intros n Hlen'; apply (Hnth (S n)). + now simpl; apply lt_n_S. + + simpl; apply Nat.lt_0_succ. Qed. (** Results about [nth_error] *) @@ -1141,7 +1143,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 +1151,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. @@ -2008,6 +2010,9 @@ Section SetIncl. now apply incl_cons_inv in Hin. Qed. + Lemma incl_filter f l : incl (filter f l) l. + Proof. intros x Hin; now apply filter_In in Hin. Qed. + Lemma remove_incl (eq_dec : forall x y : A, {x = y} + {x <> y}) : forall l1 l2 x, incl l1 l2 -> incl (remove eq_dec x l1) (remove eq_dec x l2). Proof. @@ -2018,8 +2023,15 @@ Section SetIncl. End SetIncl. +Lemma incl_map A B (f : A -> B) l1 l2 : incl l1 l2 -> incl (map f l1) (map f l2). +Proof. + intros Hincl x Hinx. + destruct (proj1 (in_map_iff _ _ _) Hinx) as [y [<- Hiny]]. + apply in_map; intuition. +Qed. + Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons - incl_app: datatypes. + incl_app incl_map: datatypes. (**************************************) @@ -2412,6 +2424,15 @@ Section ReDun. now apply Hnin, in_rev. Qed. + Lemma NoDup_filter f l : NoDup l -> NoDup (filter f l). + Proof. + induction l; simpl; intros Hnd; auto. + apply NoDup_cons_iff in Hnd. + destruct (f a); [ | intuition ]. + apply NoDup_cons_iff; split; intuition. + apply filter_In in H; intuition. + Qed. + (** Effective computation of a list without duplicates *) Hypothesis decA: forall x y : A, {x = y} + {x <> y}. @@ -2947,6 +2968,10 @@ Section Exists_Forall. now apply neg_Forall_Exists_neg. Defined. + Lemma incl_Forall_in_iff l l' : + incl l l' <-> Forall (fun x => In x l') l. + Proof. now rewrite Forall_forall; split. Qed. + End Exists_Forall. Hint Constructors Exists : core. 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/Abstract/ConstructiveAbs.v b/theories/Reals/Abstract/ConstructiveAbs.v index d357ad2d54..31397cbddd 100644 --- a/theories/Reals/Abstract/ConstructiveAbs.v +++ b/theories/Reals/Abstract/ConstructiveAbs.v @@ -57,11 +57,11 @@ Proof. - pose proof (CRabs_def R x (CRabs R x)) as [_ H1]. apply H1, CRle_refl. - rewrite <- CRabs_def. split. apply CRle_refl. - apply (CRle_trans _ (CRzero R)). 2: exact H. - apply (CRle_trans _ (CRopp R (CRzero R))). + apply (CRle_trans _ 0). 2: exact H. + apply (CRle_trans _ (CRopp R 0)). intro abs. apply CRopp_lt_cancel in abs. contradiction. - apply (CRplus_le_reg_l (CRzero R)). - apply (CRle_trans _ (CRzero R)). apply CRplus_opp_r. + apply (CRplus_le_reg_l 0). + apply (CRle_trans _ 0). apply CRplus_opp_r. apply CRplus_0_r. Qed. @@ -164,8 +164,7 @@ Lemma CR_of_Q_abs : forall {R : ConstructiveReals} (q : Q), Proof. intros. destruct (Qlt_le_dec 0 q). - apply (CReq_trans _ (CR_of_Q R q)). - apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_le. apply Qlt_le_weak, q0. + apply CRabs_right. apply CR_of_Q_le. apply Qlt_le_weak, q0. apply CR_of_Q_morph. symmetry. apply Qabs_pos, Qlt_le_weak, q0. - apply (CReq_trans _ (CR_of_Q R (-q))). apply (CReq_trans _ (CRabs R (CRopp R (CR_of_Q R q)))). @@ -173,8 +172,7 @@ Proof. 2: apply CR_of_Q_morph; symmetry; apply Qabs_neg, q0. apply (CReq_trans _ (CRopp R (CR_of_Q R q))). 2: apply CReq_sym, CR_of_Q_opp. - apply CRabs_right. apply (CRle_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. + apply CRabs_right. apply (CRle_trans _ (CR_of_Q R (-q))). apply CR_of_Q_le. apply (Qplus_le_l _ _ q). ring_simplify. exact q0. apply CR_of_Q_opp. @@ -206,14 +204,14 @@ Proof. destruct (CR_Q_dense R _ _ neg) as [q [H0 H1]]. destruct (Qlt_le_dec 0 q). - destruct (s (CR_of_Q R (-q)) x 0). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. + apply CR_of_Q_lt. apply (Qplus_lt_l _ _ q). ring_simplify. exact q0. exfalso. pose proof (CRabs_def R x (CR_of_Q R q)) as [H2 _]. apply H2. clear H2. split. apply CRlt_asym, H0. 2: exact H1. rewrite <- Qopp_involutive, CR_of_Q_opp. apply CRopp_ge_le_contravar, CRlt_asym, c. exact c. - apply (CRlt_le_trans _ _ _ H0). - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. exact q0. + apply CR_of_Q_le. exact q0. Qed. @@ -339,24 +337,23 @@ Proof. left; apply CR_of_Q_pos; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr, CRplus_assoc, <- (CRplus_assoc y). rewrite CRplus_opp_r, CRplus_0_l, CRopp_involutive. reflexivity. apply (CRmult_lt_compat_r (CR_of_Q R 2)) in H. 2: apply CR_of_Q_pos; reflexivity. - rewrite CRmult_assoc, <- CR_of_Q_mult in H. - setoid_replace ((1 # 2) * 2)%Q with 1%Q in H. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r in H. - rewrite CRmult_comm, (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_r, - CRmult_1_l in H. - intro abs. rewrite CRabs_left in H. - unfold CRminus in H. - rewrite CRopp_involutive, CRplus_comm in H. - rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l in H. - rewrite CRplus_0_l in H. exact (CRlt_asym _ _ H H). - apply CRlt_asym, abs. + intro abs. contradict H. + apply (CRle_trans _ (x + y - CRabs R (y - x))). + rewrite CRabs_left. 2: apply CRlt_asym, abs. + unfold CRminus. rewrite CRopp_involutive, CRplus_comm. + rewrite CRplus_assoc, <- (CRplus_assoc (-x)), CRplus_opp_l. + rewrite CRplus_0_l, (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. + rewrite CRmult_1_r. apply CRle_refl. + rewrite CRmult_assoc, <- CR_of_Q_mult. + setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. + rewrite CRmult_1_r. apply CRle_refl. Qed. Add Parametric Morphism {R : ConstructiveReals} : CRmin @@ -383,11 +380,11 @@ Lemma CRmin_l : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_r (CRabs _ (y + - x)+ -x)). rewrite CRplus_assoc, <- (CRplus_assoc (-CRabs _ (y + - x))). @@ -401,11 +398,11 @@ Lemma CRmin_r : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x). unfold CRminus. rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). @@ -451,15 +448,15 @@ Proof. intros. unfold CRmin. unfold CRminus. setoid_replace (x + z + - (x + y)) with (z-y). apply (CRmult_eq_reg_r (CR_of_Q _ 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. rewrite (CRplus_comm x). apply CRplus_assoc. @@ -474,11 +471,11 @@ Lemma CRmin_left : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_right. unfold CRminus. rewrite CRopp_plus_distr. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. apply CRopp_involutive. @@ -491,11 +488,11 @@ Lemma CRmin_right : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRabs_left. unfold CRminus. do 2 rewrite CRopp_plus_distr. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. @@ -510,10 +507,10 @@ Lemma CRmin_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_lt_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_lt_reg_l _ (CRabs _ (y - x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x))). @@ -526,7 +523,7 @@ Proof. apply (CRplus_lt_reg_l R (-x)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply CRopp_gt_lt_contravar, H. @@ -537,7 +534,7 @@ Proof. apply (CRplus_lt_reg_l R (-y)). rewrite CRopp_mult_distr_l. rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym. apply CRopp_gt_lt_contravar, H0. @@ -552,12 +549,12 @@ Proof. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - y) - CRabs _ (a - x))) * CR_of_Q R (1 # 2))). rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). - 2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - y) - CRabs _ (a - x)))). apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l. @@ -568,11 +565,11 @@ Proof. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. - rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl. + rewrite CRmult_1_r. apply CRle_refl. unfold CRminus. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite <- CRplus_assoc. rewrite CRplus_comm, CRopp_plus_distr. @@ -587,10 +584,10 @@ Lemma CRmin_glb : forall {R : ConstructiveReals} (x y z:CRcarrier R), Proof. intros. unfold CRmin. apply (CRmult_le_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_le_reg_l (CRabs _ (y-x) - (z*CR_of_Q R 2))). unfold CRminus. rewrite CRplus_assoc, CRplus_opp_l, CRplus_0_r. rewrite (CRplus_comm (CRabs R (y + - x) + - (z * CR_of_Q R 2))). @@ -601,13 +598,13 @@ Proof. rewrite CRopp_involutive, (CRplus_comm y), CRplus_assoc. apply CRplus_le_compat_l, (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; exact H0. - rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite CRopp_mult_distr_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_compat; apply CRopp_ge_le_contravar; exact H. Qed. @@ -673,11 +670,11 @@ Lemma CRmax_lub : forall {R : ConstructiveReals} (x y z:CRcarrier R), x <= z -> y <= z -> CRmax x y <= z. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_le_reg_l (-x-y)). rewrite <- CRplus_assoc. unfold CRminus. rewrite <- CRopp_plus_distr, CRplus_opp_l, CRplus_0_l. @@ -687,14 +684,14 @@ Proof. rewrite (CRplus_comm x), CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRopp_plus_distr. apply CRplus_le_compat; apply CRopp_ge_le_contravar; assumption. - rewrite (CRplus_comm y), CRopp_plus_distr, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. apply CRplus_le_compat; assumption. Qed. @@ -702,12 +699,12 @@ Lemma CRmax_l : forall {R : ConstructiveReals} (x y : CRcarrier R), x <= CRmax x y. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q R 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q R 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus, CR_of_Q_one. + rewrite CRmult_1_r. + setoid_replace 2%Q with (1+1)%Q. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_l, CRmult_1_r, CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-y)). @@ -720,12 +717,12 @@ Lemma CRmax_r : forall {R : ConstructiveReals} (x y : CRcarrier R), y <= CRmax x y. Proof. intros. unfold CRmax. - apply (CRmult_le_reg_r (CR_of_Q _ 2)). rewrite <- CR_of_Q_zero. + apply (CRmult_le_reg_r (CR_of_Q _ 2)). apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x). rewrite CRplus_assoc. apply CRplus_le_compat_l. apply (CRplus_le_reg_l (-x)). @@ -754,14 +751,14 @@ Proof. intros. unfold CRmax. setoid_replace (x + z - (x + y)) with (z-y). apply (CRmult_eq_reg_r (CR_of_Q _ 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_plus_distr_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRmult_1_r. do 3 rewrite (CRplus_assoc x). apply CRplus_morph. reflexivity. do 2 rewrite <- CRplus_assoc. apply CRplus_morph. 2: reflexivity. @@ -777,11 +774,11 @@ Lemma CRmax_left : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRabs_left. unfold CRminus. rewrite CRopp_plus_distr, CRopp_involutive. rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. reflexivity. @@ -793,11 +790,11 @@ Lemma CRmax_right : forall {R : ConstructiveReals} (x y : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_eq_reg_r (CR_of_Q R 2)). - left. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + left. apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. - rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. + rewrite (CR_of_Q_plus _ 1 1), CRmult_plus_distr_l, CRmult_1_r. rewrite (CRplus_comm x y). rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRabs_right. unfold CRminus. rewrite CRplus_comm. @@ -812,12 +809,12 @@ Proof. rewrite (CRabs_morph _ ((x - y + (CRabs _ (a - x) - CRabs _ (a - y))) * CR_of_Q R (1 # 2))). rewrite CRabs_mult, (CRabs_right (CR_of_Q R (1 # 2))). - 2: rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply CR_of_Q_le; discriminate. apply (CRle_trans _ ((CRabs _ (x - y) * 1 + CRabs _ (x-y) * 1) * CR_of_Q R (1 # 2))). apply CRmult_le_compat_r. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. apply (CRle_trans _ (CRabs _ (x - y) + CRabs _ (CRabs _ (a - x) - CRabs _ (a - y)))). apply CRabs_triang. rewrite CRmult_1_r. apply CRplus_le_compat_l. @@ -829,11 +826,11 @@ Proof. rewrite CRplus_comm, CRopp_plus_distr, <- CRplus_assoc. rewrite CRplus_opp_r, CRopp_involutive, CRplus_0_l. reflexivity. - rewrite <- CRmult_plus_distr_l, <- CR_of_Q_one. + rewrite <- CRmult_plus_distr_l. rewrite <- (CR_of_Q_plus R 1 1). rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 + 1) * (1 # 2))%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply CRle_refl. + rewrite CRmult_1_r. apply CRle_refl. unfold CRminus. rewrite CRopp_mult_distr_l. rewrite <- CRmult_plus_distr_r. apply CRmult_morph. 2: reflexivity. do 4 rewrite CRplus_assoc. apply CRplus_morph. reflexivity. @@ -849,10 +846,10 @@ Lemma CRmax_lub_lt : forall {R : ConstructiveReals} (x y z : CRcarrier R), Proof. intros. unfold CRmax. apply (CRmult_lt_reg_r (CR_of_Q R 2)). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt; reflexivity. + apply CR_of_Q_lt; reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. apply (CRplus_lt_reg_l _ (-y -x)). unfold CRminus. rewrite CRplus_assoc, <- (CRplus_assoc (-x)), <- (CRplus_assoc (-x)). rewrite CRplus_opp_l, CRplus_0_l, <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. @@ -861,14 +858,14 @@ Proof. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ y). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym, H0. exact H0. - rewrite CRopp_plus_distr, CRopp_involutive. rewrite CRplus_assoc. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l _ x). rewrite <- CRplus_assoc, CRplus_opp_r, CRplus_0_l. - rewrite (CR_of_Q_plus R 1 1), CR_of_Q_one, CRmult_plus_distr_l. + rewrite (CR_of_Q_plus R 1 1), CRmult_plus_distr_l. rewrite CRmult_1_r. apply CRplus_le_lt_compat. apply CRlt_asym, H. exact H. Qed. diff --git a/theories/Reals/Abstract/ConstructiveLUB.v b/theories/Reals/Abstract/ConstructiveLUB.v index 4ae24de154..1c19c6aa40 100644 --- a/theories/Reals/Abstract/ConstructiveLUB.v +++ b/theories/Reals/Abstract/ConstructiveLUB.v @@ -108,7 +108,7 @@ Proof. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos2Nat.inj_le. rewrite Nat2Pos.id. apply le_S, H0. discriminate. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. Qed. Lemma is_upper_bound_dec : @@ -272,7 +272,7 @@ Proof. apply CR_of_Q_pos. reflexivity. rewrite CRmult_assoc, <- CR_of_Q_mult, (CR_of_Q_plus R 1 1). setoid_replace ((1 # 2) * 2)%Q with 1%Q. 2: reflexivity. - rewrite CR_of_Q_one, CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. + rewrite CRmult_plus_distr_l, CRmult_1_r, CRmult_1_r. apply CRplus_lt_compat_r. exact H0. } destruct (CR_cv_open_below _ _ l lcv H1) as [p pmaj]. assert (0 < (l-CR_of_Q R r) * CR_of_Q R (1#2)). @@ -280,7 +280,6 @@ Proof. apply CRplus_lt_compat_r. exact H0. apply CR_of_Q_pos. reflexivity. } destruct (CRup_nat (CRinv R _ (inr H2))) as [i imaj]. destruct i. exfalso. simpl in imaj. - rewrite CR_of_Q_zero in imaj. exact (CRlt_asym _ _ imaj (CRinv_0_lt_compat R _ (inr H2) H2)). specialize (pmaj (max (S i) (S p)) (le_trans p (S p) _ (le_S p p (le_refl p)) (Nat.le_max_r (S i) (S p)))). unfold proj1_sig in pmaj. @@ -309,7 +308,7 @@ Proof. CR_of_Q R (1 # Pos.of_nat (S i)))). apply CRlt_asym, imaj. rewrite CRmult_assoc, <- CR_of_Q_mult. setoid_replace ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i)))%Q with 1%Q. - rewrite CR_of_Q_one, CRmult_1_r. + rewrite CRmult_1_r. unfold CRminus. rewrite CRmult_plus_distr_r, (CRplus_comm (-CR_of_Q R r)). rewrite (CRplus_comm (CR_of_Q R r)), CRmult_plus_distr_r. rewrite CRplus_assoc. apply CRplus_le_compat_l. diff --git a/theories/Reals/Abstract/ConstructiveLimits.v b/theories/Reals/Abstract/ConstructiveLimits.v index 4a40cc8cb3..64dcd2e1ec 100644 --- a/theories/Reals/Abstract/ConstructiveLimits.v +++ b/theories/Reals/Abstract/ConstructiveLimits.v @@ -89,7 +89,7 @@ Lemma CR_cv_unique : forall {R : ConstructiveReals} (xn : nat -> CRcarrier R) -> CR_cv R xn b -> a == b. Proof. - intros. assert (CR_cv R (fun _ => CRzero R) (CRminus R b a)). + intros. assert (CR_cv R (fun _ => 0) (CRminus R b a)). { apply (CR_cv_extens (fun n => CRminus R (xn n) (xn n))). intro n. unfold CRminus. apply CRplus_opp_r. apply CR_cv_plus. exact H0. apply CR_cv_opp, H. } @@ -111,8 +111,7 @@ Proof. rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. apply (Qplus_lt_l _ _ q). ring_simplify. - apply (lt_CR_of_Q R q 0). apply (CRlt_le_trans _ (CRzero R) _ H). - apply CR_of_Q_zero. + apply (lt_CR_of_Q R q 0). exact H. apply (CRlt_le_trans _ (CRopp R z)). apply (CRle_lt_trans _ (CRopp R (CR_of_Q R q))). apply CR_of_Q_opp. apply CRopp_gt_lt_contravar, H0. @@ -131,8 +130,7 @@ Proof. setoid_replace ((Z.pos p # 1) * (1 # p))%Q with 1%Q in pmaj. rewrite Qmult_1_r in pmaj. exact pmaj. unfold Qeq, Qnum, Qden; simpl. do 2 rewrite Pos.mul_1_r. reflexivity. - apply (lt_CR_of_Q R 0 q). apply (CRle_lt_trans _ (CRzero R)). - 2: exact H0. apply CR_of_Q_zero. + apply (lt_CR_of_Q R 0 q). exact H0. apply (CRlt_le_trans _ _ _ H). apply (CRle_trans _ (CRabs R (CRopp R z))). apply (CRle_trans _ (CRabs R z)). @@ -140,10 +138,7 @@ Proof. apply H1. apply CRle_refl. apply CRabs_opp. apply CRabs_morph. unfold CRminus. symmetry. apply CRplus_0_l. - subst z. apply (CRplus_eq_reg_l (CRopp R a)). - apply (CReq_trans _ (CRzero R)). apply CRplus_opp_l. - destruct (CRisRing R). - apply (CReq_trans _ (CRplus R b (CRopp R a))). apply CReq_sym, H. - apply Radd_comm. + rewrite CRplus_opp_l, CRplus_comm. symmetry. exact H. Qed. Lemma CR_cv_eq : forall {R : ConstructiveReals} @@ -196,7 +191,7 @@ Lemma Un_cv_nat_real : forall {R : ConstructiveReals} Proof. intros. destruct (CR_archimedean R (CRinv R eps (inr H0))) as [k kmaj]. assert (0 < CR_of_Q R (Z.pos k # 1)). - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } specialize (H k) as [p pmaj]. exists p. intros. apply (CRle_lt_trans _ (CR_of_Q R (1 # k))). @@ -204,7 +199,7 @@ Proof. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos k # 1))). exact H1. rewrite <- CR_of_Q_mult. apply (CRle_lt_trans _ 1). - rewrite <- CR_of_Q_one. apply CR_of_Q_le. + apply CR_of_Q_le. unfold Qle; simpl. do 2 rewrite Pos.mul_1_r. apply Z.le_refl. apply (CRmult_lt_reg_r (CRinv R eps (inr H0))). apply CRinv_0_lt_compat, H0. rewrite CRmult_1_l, CRmult_assoc. @@ -220,7 +215,7 @@ Lemma Un_cv_real_nat : forall {R : ConstructiveReals} Proof. intros. intros n. specialize (H (CR_of_Q R (1#n))) as [p pmaj]. - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CR_of_Q_lt. reflexivity. exists p. intros. apply CRlt_asym. apply pmaj. apply H. Qed. @@ -288,12 +283,12 @@ Proof. setoid_replace (1 # n * x)%Q with ((1 # n) *(1# x))%Q. 2: reflexivity. rewrite <- (CRmult_1_r (CR_of_Q R (1#n))). rewrite CR_of_Q_mult, CRmult_assoc. - apply CRmult_le_compat_l. rewrite <- CR_of_Q_zero. + apply CRmult_le_compat_l. apply CR_of_Q_le. discriminate. intro abs. apply (CRmult_lt_compat_l (CR_of_Q R (Z.pos x #1))) in abs. rewrite CRmult_1_r, <- CRmult_assoc, <- CR_of_Q_mult in abs. rewrite (CR_of_Q_morph R ((Z.pos x # 1) * (1 # x))%Q 1%Q) in abs. - rewrite CR_of_Q_one, CRmult_1_l in abs. + rewrite CRmult_1_l in abs. apply (CRlt_asym _ _ abs), (CRlt_trans _ (1 + CRabs R a)). 2: exact c. rewrite <- CRplus_0_l, <- CRplus_assoc. apply CRplus_lt_compat_r. rewrite CRplus_0_r. apply CRzero_lt_one. @@ -310,7 +305,7 @@ Lemma CR_cv_const : forall {R : ConstructiveReals} (a : CRcarrier R), Proof. intros a p. exists O. intros. unfold CRminus. rewrite CRplus_opp_r. - rewrite CRabs_right. rewrite <- CR_of_Q_zero. + rewrite CRabs_right. apply CR_of_Q_le. discriminate. apply CRle_refl. Qed. @@ -633,7 +628,7 @@ Lemma CR_double : forall {R : ConstructiveReals} (x:CRcarrier R), CR_of_Q R 2 * x == x + x. Proof. intros R x. rewrite (CR_of_Q_morph R 2 (1+1)). - 2: reflexivity. rewrite CR_of_Q_plus, CR_of_Q_one. + 2: reflexivity. rewrite CR_of_Q_plus. rewrite CRmult_plus_distr_r, CRmult_1_l. reflexivity. Qed. @@ -641,7 +636,7 @@ Lemma GeoCvZero : forall {R : ConstructiveReals}, CR_cv R (fun n:nat => CRpow (CR_of_Q R (1#2)) n) 0. Proof. intro R. assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). - { induction n. unfold INR; simpl. rewrite CR_of_Q_zero. + { induction n. unfold INR; simpl. apply CRzero_lt_one. unfold INR. fold (1+n)%nat. rewrite Nat2Z.inj_add. rewrite (CR_of_Q_morph R _ ((Z.of_nat 1 # 1) + (Z.of_nat n #1))). @@ -651,29 +646,29 @@ Proof. with (CR_of_Q R 2 * CRpow (CR_of_Q R 2) n). 2: reflexivity. rewrite CR_double. apply CRplus_le_lt_compat. - 2: exact IHn. simpl. rewrite CR_of_Q_one. - apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. } + 2: exact IHn. simpl. + apply pow_R1_Rle. apply CR_of_Q_le. discriminate. } intros p. exists (Pos.to_nat p). intros. unfold CRminus. rewrite CRopp_0. rewrite CRplus_0_r. rewrite CRabs_right. - 2: apply pow_le; rewrite <- CR_of_Q_zero; apply CR_of_Q_le; discriminate. + 2: apply pow_le; apply CR_of_Q_le; discriminate. apply CRlt_asym. apply (CRmult_lt_reg_l (CR_of_Q R (Z.pos p # 1))). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult. + apply CR_of_Q_lt. reflexivity. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((Z.pos p # 1) * (1 # p)) 1). 2: unfold Qmult, Qeq, Qnum, Qden; ring_simplify; reflexivity. apply (CRmult_lt_reg_r (CRpow (CR_of_Q R 2) i)). - apply pow_lt. simpl. rewrite <- CR_of_Q_zero. + apply pow_lt. simpl. apply CR_of_Q_lt. reflexivity. rewrite CRmult_assoc. rewrite pow_mult. rewrite (pow_proper (CR_of_Q R (1 # 2) * CR_of_Q R 2) 1), pow_one. - rewrite CRmult_1_r, CR_of_Q_one, CRmult_1_l. + rewrite CRmult_1_r, CRmult_1_l. apply (CRle_lt_trans _ (INR i)). 2: exact (H i). clear H. apply CR_of_Q_le. unfold Qle,Qnum,Qden. do 2 rewrite Z.mul_1_r. rewrite <- positive_nat_Z. apply Nat2Z.inj_le, H0. rewrite <- CR_of_Q_mult. setoid_replace ((1#2)*2)%Q with 1%Q. - apply CR_of_Q_one. reflexivity. + reflexivity. reflexivity. Qed. Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), @@ -681,9 +676,9 @@ Lemma GeoFiniteSum : forall {R : ConstructiveReals} (n:nat), Proof. induction n. - unfold CRsum, CRpow. simpl (1%ConstructiveReals). - unfold CRminus. rewrite (CR_of_Q_morph R _ (1+1)). - rewrite CR_of_Q_plus, CR_of_Q_one, CRplus_assoc. - rewrite CRplus_opp_r, CRplus_0_r. reflexivity. reflexivity. + unfold CRminus. rewrite (CR_of_Q_plus R 1 1). + rewrite CRplus_assoc. + rewrite CRplus_opp_r, CRplus_0_r. reflexivity. - setoid_replace (CRsum (CRpow (CR_of_Q R (1 # 2))) (S n)) with (CRsum (CRpow (CR_of_Q R (1 # 2))) n + CRpow (CR_of_Q R (1 # 2)) (S n)). 2: reflexivity. @@ -701,7 +696,7 @@ Proof. 2: reflexivity. rewrite <- CRmult_assoc, <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. - rewrite CR_of_Q_one. apply CRmult_1_l. reflexivity. + apply CRmult_1_l. reflexivity. Qed. Lemma GeoHalfBelowTwo : forall {R : ConstructiveReals} (n:nat), @@ -710,7 +705,7 @@ Proof. intros. rewrite <- (CRplus_0_r (CR_of_Q R 2)), GeoFiniteSum. apply CRplus_lt_compat_l. rewrite <- CRopp_0. apply CRopp_gt_lt_contravar. - apply pow_lt. rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply pow_lt. apply CR_of_Q_lt. reflexivity. Qed. Lemma GeoHalfTwo : forall {R : ConstructiveReals}, @@ -720,35 +715,35 @@ Proof. apply (CR_cv_eq _ (fun n => CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) n)). - intro n. rewrite GeoFiniteSum. reflexivity. - assert (forall n:nat, INR n < CRpow (CR_of_Q R 2) n). - { induction n. unfold INR; simpl. rewrite CR_of_Q_zero. + { induction n. unfold INR; simpl. apply CRzero_lt_one. apply (CRlt_le_trans _ (CRpow (CR_of_Q R 2) n + 1)). unfold INR. rewrite Nat2Z.inj_succ, <- Z.add_1_l. rewrite (CR_of_Q_morph R _ (1 + (Z.of_nat n #1))). 2: symmetry; apply Qinv_plus_distr. rewrite CR_of_Q_plus. - rewrite CRplus_comm. rewrite CR_of_Q_one. + rewrite CRplus_comm. apply CRplus_lt_compat_r, IHn. setoid_replace (CRpow (CR_of_Q R 2) (S n)) with (CRpow (CR_of_Q R 2) n + CRpow (CR_of_Q R 2) n). apply CRplus_le_compat. apply CRle_refl. - apply pow_R1_Rle. rewrite <- CR_of_Q_one. apply CR_of_Q_le. discriminate. + apply pow_R1_Rle. apply CR_of_Q_le. discriminate. rewrite <- CR_double. reflexivity. } intros n. exists (Pos.to_nat n). intros. setoid_replace (CR_of_Q R 2 - CRpow (CR_of_Q R (1 # 2)) i - CR_of_Q R 2) with (- CRpow (CR_of_Q R (1 # 2)) i). rewrite CRabs_opp. rewrite CRabs_right. assert (0 < CR_of_Q R 2). - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } rewrite (pow_proper _ (CRinv R (CR_of_Q R 2) (inr H1))). rewrite pow_inv. apply CRlt_asym. apply (CRmult_lt_reg_l (CRpow (CR_of_Q R 2) i)). apply pow_lt, H1. rewrite CRinv_r. apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n#1))). - rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CR_of_Q_lt. reflexivity. rewrite CRmult_1_l, CRmult_assoc. rewrite <- CR_of_Q_mult. rewrite (CR_of_Q_morph R ((1 # n) * (Z.pos n # 1)) 1). 2: reflexivity. - rewrite CR_of_Q_one, CRmult_1_r. apply (CRle_lt_trans _ (INR i)). + rewrite CRmult_1_r. apply (CRle_lt_trans _ (INR i)). 2: apply H. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. destruct i. exfalso. inversion H0. pose proof (Pos2Nat.is_pos n). @@ -758,8 +753,8 @@ Proof. apply (CRmult_eq_reg_l (CR_of_Q R 2)). right. exact H1. rewrite CRinv_r. rewrite <- CR_of_Q_mult. setoid_replace (2 * (1 # 2))%Q with 1%Q. - apply CR_of_Q_one. reflexivity. - apply CRlt_asym, pow_lt. rewrite <- CR_of_Q_zero. + reflexivity. reflexivity. + apply CRlt_asym, pow_lt. apply CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc. rewrite CRplus_opp_l, CRplus_0_l. reflexivity. @@ -929,5 +924,5 @@ Proof. intros n. exists (Pos.to_nat n). intros. unfold CRminus. simpl. rewrite CRopp_involutive, CRplus_opp_l. rewrite CRabs_right. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. apply CRle_refl. + apply CR_of_Q_le. discriminate. apply CRle_refl. Qed. diff --git a/theories/Reals/Abstract/ConstructiveReals.v b/theories/Reals/Abstract/ConstructiveReals.v index d91fd1183a..019428a5b0 100644 --- a/theories/Reals/Abstract/ConstructiveReals.v +++ b/theories/Reals/Abstract/ConstructiveReals.v @@ -101,9 +101,15 @@ Structure ConstructiveReals : Type := CRltDisjunctEpsilon : forall a b c d : CRcarrier, (CRltProp a b \/ CRltProp c d) -> CRlt a b + CRlt c d; - (* Constants *) - CRzero : CRcarrier; - CRone : CRcarrier; + (* The initial field morphism (in characteristic zero). + The abstract definition by iteration of addition is + probably the slowest. Let each instance implement + a faster (and often simpler) version. *) + CR_of_Q : Q -> CRcarrier; + CR_of_Q_lt : forall q r : Q, + Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); + lt_CR_of_Q : forall q r : Q, + CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; (* Addition and multiplication *) CRplus : CRcarrier -> CRcarrier -> CRcarrier; @@ -111,19 +117,22 @@ Structure ConstructiveReals : Type := stronger than Prop-existence of opposite *) CRmult : CRcarrier -> CRcarrier -> CRcarrier; - CRisRing : ring_theory CRzero CRone CRplus CRmult + CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) + (CRplus (CR_of_Q q) (CR_of_Q r)); + CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) + (CRmult (CR_of_Q q) (CR_of_Q r)); + CRisRing : ring_theory (CR_of_Q 0) (CR_of_Q 1) CRplus CRmult (fun x y => CRplus x (CRopp y)) CRopp CReq; CRisRingExt : ring_eq_ext CRplus CRmult CRopp CReq; (* Compatibility with order *) - CRzero_lt_one : CRlt CRzero CRone; (* 0 # 1 would only allow 0 < 1 because - of Fmult_lt_0_compat so request 0 < 1 directly. *) + CRzero_lt_one : CRlt (CR_of_Q 0) (CR_of_Q 1); CRplus_lt_compat_l : forall r r1 r2 : CRcarrier, CRlt r1 r2 -> CRlt (CRplus r r1) (CRplus r r2); CRplus_lt_reg_l : forall r r1 r2 : CRcarrier, CRlt (CRplus r r1) (CRplus r r2) -> CRlt r1 r2; CRmult_lt_0_compat : forall x y : CRcarrier, - CRlt CRzero x -> CRlt CRzero y -> CRlt CRzero (CRmult x y); + CRlt (CR_of_Q 0) x -> CRlt (CR_of_Q 0) y -> CRlt (CR_of_Q 0) (CRmult x y); (* A constructive total inverse function on F would need to be continuous, which is impossible because we cannot connect plus and minus infinities. @@ -132,26 +141,11 @@ Structure ConstructiveReals : Type := To implement Finv by Cauchy sequences we need orderAppart, ~orderEq is not enough. *) - CRinv : forall x : CRcarrier, CRapart x CRzero -> CRcarrier; - CRinv_l : forall (r:CRcarrier) (rnz : CRapart r CRzero), - CReq (CRmult (CRinv r rnz) r) CRone; - CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r CRzero), - CRlt CRzero r -> CRlt CRzero (CRinv r rnz); - - (* The initial field morphism (in characteristic zero). - The abstract definition by iteration of addition is - probably the slowest. Let each instance implement - a faster (and often simpler) version. *) - CR_of_Q : Q -> CRcarrier; - CR_of_Q_plus : forall q r : Q, CReq (CR_of_Q (q+r)) - (CRplus (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_mult : forall q r : Q, CReq (CR_of_Q (q*r)) - (CRmult (CR_of_Q q) (CR_of_Q r)); - CR_of_Q_one : CReq (CR_of_Q 1) CRone; - CR_of_Q_lt : forall q r : Q, - Qlt q r -> CRlt (CR_of_Q q) (CR_of_Q r); - lt_CR_of_Q : forall q r : Q, - CRlt (CR_of_Q q) (CR_of_Q r) -> Qlt q r; + CRinv : forall x : CRcarrier, CRapart x (CR_of_Q 0) -> CRcarrier; + CRinv_l : forall (r:CRcarrier) (rnz : CRapart r (CR_of_Q 0)), + CReq (CRmult (CRinv r rnz) r) (CR_of_Q 1); + CRinv_0_lt_compat : forall (r : CRcarrier) (rnz : CRapart r (CR_of_Q 0)), + CRlt (CR_of_Q 0) r -> CRlt (CR_of_Q 0) (CRinv r rnz); (* This function is very fast in both the Cauchy and Dedekind instances, because this rational number q is almost what @@ -213,8 +207,17 @@ Notation "x <= y <= z" := (CRle _ x y /\ CRle _ y z) : ConstructiveReals. Notation "x < y < z" := (prod (CRlt _ x y) (CRlt _ y z)) : ConstructiveReals. Notation "x == y" := (CReq _ x y) : ConstructiveReals. Notation "x ≶ y" := (CRapart _ x y) (at level 70, no associativity) : ConstructiveReals. -Notation "0" := (CRzero _) : ConstructiveReals. -Notation "1" := (CRone _) : ConstructiveReals. +Notation "0" := (CR_of_Q _ 0) : ConstructiveReals. +Notation "1" := (CR_of_Q _ 1) : ConstructiveReals. +Notation "2" := (CR_of_Q _ 2) : ConstructiveReals. +Notation "3" := (CR_of_Q _ 3) : ConstructiveReals. +Notation "4" := (CR_of_Q _ 4) : ConstructiveReals. +Notation "5" := (CR_of_Q _ 5) : ConstructiveReals. +Notation "6" := (CR_of_Q _ 6) : ConstructiveReals. +Notation "7" := (CR_of_Q _ 7) : ConstructiveReals. +Notation "8" := (CR_of_Q _ 8) : ConstructiveReals. +Notation "9" := (CR_of_Q _ 9) : ConstructiveReals. +Notation "10" := (CR_of_Q _ 10) : ConstructiveReals. Notation "x + y" := (CRplus _ x y) : ConstructiveReals. Notation "- x" := (CRopp _ x) : ConstructiveReals. Notation "x - y" := (CRminus _ x y) : ConstructiveReals. @@ -567,7 +570,7 @@ Lemma CRopp_involutive : forall {R : ConstructiveReals} (r : CRcarrier R), - - r == r. Proof. intros. apply (CRplus_eq_reg_l (CRopp R r)). - transitivity (CRzero R). apply CRisRing. + transitivity (CR_of_Q R 0). apply CRisRing. apply CReq_sym. transitivity (r + - r). apply CRisRing. apply CRisRing. Qed. @@ -578,7 +581,7 @@ Lemma CRopp_gt_lt_contravar Proof. intros. apply (CRplus_lt_reg_l R r1). destruct (CRisRing R). - apply (CRle_lt_trans _ (CRzero R)). apply Ropp_def. + apply (CRle_lt_trans _ 0). apply Ropp_def. apply (CRplus_lt_compat_l R (CRopp R r2)) in H. apply (CRle_lt_trans _ (CRplus R (CRopp R r2) r2)). apply (CRle_trans _ (CRplus R r2 (CRopp R r2))). @@ -611,13 +614,13 @@ Lemma CRopp_plus_distr : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), Proof. intros. destruct (CRisRing R), (CRisRingExt R). apply (CRplus_eq_reg_l (CRplus R r1 r2)). - transitivity (CRzero R). apply Ropp_def. + transitivity (CR_of_Q R 0). apply Ropp_def. transitivity (r2 + r1 + (-r1 + -r2)). transitivity (r2 + (r1 + (-r1 + -r2))). transitivity (r2 + - r2). apply CReq_sym. apply Ropp_def. apply Radd_ext. apply CReq_refl. - transitivity (CRzero R + - r2). + transitivity (0 + - r2). apply CReq_sym, Radd_0_l. transitivity (r1 + - r1 + - r2). apply Radd_ext. 2: apply CReq_refl. apply CReq_sym, Ropp_def. @@ -701,7 +704,7 @@ Lemma CRopp_mult_distr_r : forall {R : ConstructiveReals} (r1 r2 : CRcarrier R), - (r1 * r2) == r1 * (- r2). Proof. intros. apply (CRplus_eq_reg_l (CRmult R r1 r2)). - destruct (CRisRing R). transitivity (CRzero R). apply Ropp_def. + destruct (CRisRing R). transitivity (CR_of_Q R 0). apply Ropp_def. transitivity (r1 * (r2 + - r2)). 2: apply CRmult_plus_distr_l. transitivity (r1 * 0). @@ -725,7 +728,7 @@ Lemma CRmult_lt_compat_r : forall {R : ConstructiveReals} (r r1 r2 : CRcarrier R 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. intros. apply (CRplus_lt_reg_r (CRopp R (CRmult R r1 r))). - apply (CRle_lt_trans _ (CRzero R)). + apply (CRle_lt_trans _ 0). apply (Ropp_def (CRisRing R)). apply (CRlt_le_trans _ (CRplus R (CRmult R r2 r) (CRmult R (CRopp R r1) r))). apply (CRlt_le_trans _ (CRmult R (CRplus R r2 (CRopp R r1)) r)). @@ -734,7 +737,7 @@ Proof. apply (CRle_lt_trans _ r1). apply (Radd_0_l (CRisRing R)). apply (CRlt_le_trans _ r2 _ H0). apply (CRle_trans _ (CRplus R r2 (CRplus R (CRopp R r1) r1))). - apply (CRle_trans _ (CRplus R r2 (CRzero R))). + apply (CRle_trans _ (CRplus R r2 0)). destruct (CRplus_0_r r2). exact H1. apply CRplus_le_compat_l. destruct (CRplus_opp_l r1). exact H1. destruct (Radd_assoc (CRisRing R) r2 (CRopp R r1) r1). exact H2. @@ -752,7 +755,7 @@ Proof. Qed. Lemma CRinv_r : forall {R : ConstructiveReals} (r:CRcarrier R) - (rnz : r ≶ (CRzero R)), + (rnz : r ≶ 0), r * (/ r) rnz == 1. Proof. intros. transitivity ((/ r) rnz * r). @@ -765,7 +768,7 @@ Proof. intros. apply (CRmult_lt_compat_r ((/ r) (inr H))) in H0. 2: apply CRinv_0_lt_compat, H. apply (CRle_lt_trans _ ((r1 * r) * ((/ r) (inr H)))). - - clear H0. apply (CRle_trans _ (CRmult R r1 (CRone R))). + - clear H0. apply (CRle_trans _ (CRmult R r1 1)). destruct (CRmult_1_r r1). exact H0. apply (CRle_trans _ (CRmult R r1 (CRmult R r ((/ r) (inr H))))). destruct (Rmul_ext (CRisRingExt R) r1 r1 (CReq_refl r1) @@ -779,7 +782,7 @@ Proof. apply (CRle_trans _ (r2 * (r * ((/ r) (inr H))))). destruct (Rmul_assoc (CRisRing R) r2 r ((/ r) (inr H))). exact H0. destruct (Rmul_ext (CRisRingExt R) r2 r2 (CReq_refl r2) - (r * ((/ r) (inr H))) (CRone R)). + (r * ((/ r) (inr H))) 1). apply CRinv_r. exact H1. Qed. @@ -829,7 +832,7 @@ Proof. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans _ (CRzero R) _ c). + apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. + intro abs. apply H0. apply CRopp_lt_cancel. apply (CRle_lt_trans _ (CRmult R r2 (CRopp R r))). @@ -839,7 +842,7 @@ Proof. apply CRmult_lt_compat_r. 2: exact abs. apply (CRplus_lt_reg_r r). apply (CRle_lt_trans _ r). apply (Radd_0_l (CRisRing R)). - apply (CRlt_le_trans _ (CRzero R) _ c). + apply (CRlt_le_trans _ 0 _ c). apply CRplus_opp_l. Qed. @@ -920,31 +923,21 @@ Proof. intros R x y H. apply CR_of_Q_morph; assumption. Qed. -Lemma CR_of_Q_zero : forall {R : ConstructiveReals}, - CR_of_Q R 0 == 0. -Proof. - intros. apply CRzero_double. - transitivity (CR_of_Q R (0+0)). apply CR_of_Q_morph. - reflexivity. apply CR_of_Q_plus. -Qed. - Lemma CR_of_Q_opp : forall {R : ConstructiveReals} (q : Q), CR_of_Q R (-q) == - CR_of_Q R q. Proof. intros. apply (CRplus_eq_reg_l (CR_of_Q R q)). - transitivity (CRzero R). + transitivity (CR_of_Q R 0). transitivity (CR_of_Q R (q-q)). apply CReq_sym, CR_of_Q_plus. - transitivity (CR_of_Q R 0). - apply CR_of_Q_morph. ring. apply CR_of_Q_zero. + apply CR_of_Q_morph. ring. apply CReq_sym. apply (CRisRing R). Qed. Lemma CR_of_Q_pos : forall {R : ConstructiveReals} (q:Q), Qlt 0 q -> 0 < CR_of_Q R q. Proof. - intros. apply (CRle_lt_trans _ (CR_of_Q R 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. exact H. + intros. apply CR_of_Q_lt. exact H. Qed. Lemma CR_of_Q_inv : forall {R : ConstructiveReals} (q : Q) (qPos : Qlt 0 q), @@ -954,7 +947,7 @@ Proof. intros. apply (CRmult_eq_reg_l (CR_of_Q R q)). right. apply CR_of_Q_pos, qPos. - rewrite CRinv_r, <- CR_of_Q_mult, <- CR_of_Q_one. + rewrite CRinv_r, <- CR_of_Q_mult. apply CR_of_Q_morph. field. intro abs. rewrite abs in qPos. exact (Qlt_irrefl 0 qPos). Qed. @@ -969,7 +962,7 @@ Proof. destruct (CR_archimedean R (b * ((/ -(a*b)) (inr epsPos)))) as [n maj]. assert (0 < CR_of_Q R (Z.pos n #1)) as nPos. - { rewrite <- CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. } + { apply CR_of_Q_lt. reflexivity. } assert (b * (/ CR_of_Q R (Z.pos n #1)) (inr nPos) < -(a*b)). { apply (CRmult_lt_reg_r (CR_of_Q R (Z.pos n #1))). apply nPos. rewrite <- (Rmul_assoc (CRisRing R)), CRinv_l, CRmult_1_r. @@ -1082,7 +1075,7 @@ Definition CRfloor {R : ConstructiveReals} (a : CRcarrier R) Proof. destruct (CR_Q_dense R (a - CR_of_Q R (1#2)) a) as [q qmaj]. - apply (CRlt_le_trans _ (a-0)). apply CRplus_lt_compat_l. - apply CRopp_gt_lt_contravar. rewrite <- CR_of_Q_zero. + apply CRopp_gt_lt_contravar. apply CR_of_Q_lt. reflexivity. unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. - exists (Qfloor q). destruct qmaj. split. diff --git a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v index bc44668e2f..cf302dc847 100644 --- a/theories/Reals/Abstract/ConstructiveRealsMorphisms.v +++ b/theories/Reals/Abstract/ConstructiveRealsMorphisms.v @@ -163,9 +163,8 @@ Lemma CRmorph_zero : forall {R1 R2 : ConstructiveReals} CRmorph f 0 == 0. Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 0))). - apply CRmorph_proper. apply CReq_sym, CR_of_Q_zero. - apply (CReq_trans _ (CR_of_Q R2 0)). - apply CRmorph_rat. apply CR_of_Q_zero. + apply CRmorph_proper. reflexivity. + apply CRmorph_rat. Qed. Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} @@ -173,9 +172,8 @@ Lemma CRmorph_one : forall {R1 R2 : ConstructiveReals} CRmorph f 1 == 1. Proof. intros. apply (CReq_trans _ (CRmorph f (CR_of_Q R1 1))). - apply CRmorph_proper. apply CReq_sym, CR_of_Q_one. - apply (CReq_trans _ (CR_of_Q R2 1)). - apply CRmorph_rat. apply CR_of_Q_one. + apply CRmorph_proper. reflexivity. + apply CRmorph_rat. Qed. Lemma CRmorph_opp : forall {R1 R2 : ConstructiveReals} @@ -228,9 +226,9 @@ Lemma CRplus_pos_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Qlt 0 q -> CRlt R x (CRplus R x (CR_of_Q R q)). Proof. intros. - apply (CRle_lt_trans _ (CRplus R x (CRzero R))). apply CRplus_0_r. + apply (CRle_lt_trans _ (CRplus R x 0)). apply CRplus_0_r. apply CRplus_lt_compat_l. - apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R 0)). apply CRle_refl. apply CR_of_Q_lt. exact H. Defined. @@ -238,10 +236,10 @@ Lemma CRplus_neg_rat_lt : forall {R : ConstructiveReals} (x : CRcarrier R) (q : Qlt q 0 -> CRlt R (CRplus R x (CR_of_Q R q)) x. Proof. intros. - apply (CRlt_le_trans _ (CRplus R x (CRzero R))). 2: apply CRplus_0_r. + apply (CRlt_le_trans _ (CRplus R x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRlt_le_trans _ (CR_of_Q R 0)). - apply CR_of_Q_lt. exact H. apply CR_of_Q_zero. + apply CR_of_Q_lt. exact H. apply CRle_refl. Qed. Lemma CRmorph_plus_rat : forall {R1 R2 : ConstructiveReals} @@ -276,7 +274,7 @@ Proof. destruct (CRisRing R1). apply (CRle_trans _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). - apply (CRle_trans _ (CRplus R1 x (CRzero R1))). + apply (CRle_trans _ (CRplus R1 x 0)). destruct (CRplus_0_r x). exact H. apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H. destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). @@ -294,7 +292,7 @@ Proof. _ (CRplus R1 x (CRplus R1 (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))))). destruct (Radd_assoc x (CR_of_Q R1 q) (CRopp R1 (CR_of_Q R1 q))). exact H0. - apply (CRle_trans _ (CRplus R1 x (CRzero R1))). + apply (CRle_trans _ (CRplus R1 x 0)). apply CRplus_le_compat_l. destruct (Ropp_def (CR_of_Q R1 q)). exact H1. destruct (CRplus_0_r x). exact H1. apply (CRlt_le_trans _ (CR_of_Q R1 (r-q))). @@ -379,12 +377,12 @@ Proof. apply CRmorph_proper. destruct (CRisRing R1). apply (CReq_trans _ (CRplus R1 x (CRplus R1 y (CRopp R1 y)))). apply CReq_sym, Radd_assoc. - apply (CReq_trans _ (CRplus R1 x (CRzero R1))). 2: apply CRplus_0_r. + apply (CReq_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. destruct (CRisRingExt R1). apply Radd_ext. apply CReq_refl. apply Ropp_def. apply (CRplus_lt_reg_r (CRmorph f y)). apply (CRlt_le_trans _ _ _ abs). clear abs. - apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRzero R2))). + apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) 0)). destruct (CRplus_0_r (CRmorph f (CRplus R1 x y))). exact H. apply (CRle_trans _ (CRplus R2 (CRmorph f (CRplus R1 x y)) (CRplus R2 (CRmorph f (CRopp R1 y)) (CRmorph f y)))). @@ -407,29 +405,26 @@ Lemma CRmorph_mult_pos : forall {R1 R2 : ConstructiveReals} Proof. induction n. - simpl. destruct (CRisRingExt R1). - apply (CReq_trans _ (CRzero R2)). - + apply (CReq_trans _ (CRmorph f (CRzero R1))). + apply (CReq_trans _ 0). + + apply (CReq_trans _ (CRmorph f 0)). 2: apply CRmorph_zero. apply CRmorph_proper. - apply (CReq_trans _ (CRmult R1 x (CRzero R1))). - 2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. apply CR_of_Q_zero. - + apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRzero R2))). + apply (CReq_trans _ (CRmult R1 x 0)). + 2: apply CRmult_0_r. apply Rmul_ext. apply CReq_refl. reflexivity. + + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 0)). apply CReq_sym, CRmult_0_r. destruct (CRisRingExt R2). - apply Rmul_ext0. apply CReq_refl. apply CReq_sym, CR_of_Q_zero. + apply Rmul_ext0. apply CReq_refl. reflexivity. - destruct (CRisRingExt R1), (CRisRingExt R2). - apply (CReq_trans - _ (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). + transitivity (CRmorph f (CRplus R1 x (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). apply CRmorph_proper. - apply (CReq_trans - _ (CRmult R1 x (CRplus R1 (CRone R1) (CR_of_Q R1 (Z.of_nat n # 1))))). - apply Rmul_ext. apply CReq_refl. - apply (CReq_trans _ (CR_of_Q R1 (1 + (Z.of_nat n # 1)))). + transitivity (CRmult R1 x (CRplus R1 1 (CR_of_Q R1 (Z.of_nat n # 1)))). + apply Rmul_ext. reflexivity. + transitivity (CR_of_Q R1 (1 + (Z.of_nat n # 1))). apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. - apply (CReq_trans _ (CRplus R1 (CR_of_Q R1 1) (CR_of_Q R1 (Z.of_nat n # 1)))). - apply CR_of_Q_plus. apply Radd_ext. apply CR_of_Q_one. apply CReq_refl. - apply (CReq_trans _ (CRplus R1 (CRmult R1 x (CRone R1)) - (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1))))). - apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. apply CReq_refl. + rewrite CR_of_Q_plus. reflexivity. + transitivity (CRplus R1 (CRmult R1 x 1) + (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))). + apply CRmult_plus_distr_l. apply Radd_ext. apply CRmult_1_r. reflexivity. apply (CReq_trans _ (CRplus R2 (CRmorph f x) (CRmorph f (CRmult R1 x (CR_of_Q R1 (Z.of_nat n # 1)))))). @@ -439,16 +434,16 @@ Proof. (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). apply Radd_ext0. apply CReq_refl. exact IHn. apply (CReq_trans - _ (CRmult R2 (CRmorph f x) (CRplus R2 (CRone R2) (CR_of_Q R2 (Z.of_nat n # 1))))). + _ (CRmult R2 (CRmorph f x) (CRplus R2 1 (CR_of_Q R2 (Z.of_nat n # 1))))). apply (CReq_trans - _ (CRplus R2 (CRmult R2 (CRmorph f x) (CRone R2)) + _ (CRplus R2 (CRmult R2 (CRmorph f x) 1) (CRmult R2 (CRmorph f x) (CR_of_Q R2 (Z.of_nat n # 1))))). apply Radd_ext0. 2: apply CReq_refl. apply CReq_sym, CRmult_1_r. apply CReq_sym, CRmult_plus_distr_l. apply Rmul_ext0. apply CReq_refl. apply (CReq_trans _ (CR_of_Q R2 (1 + (Z.of_nat n # 1)))). apply (CReq_trans _ (CRplus R2 (CR_of_Q R2 1) (CR_of_Q R2 (Z.of_nat n # 1)))). - apply Radd_ext0. apply CReq_sym, CR_of_Q_one. apply CReq_refl. + apply Radd_ext0. reflexivity. reflexivity. apply CReq_sym, CR_of_Q_plus. apply CR_of_Q_morph. rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Z.add_comm. rewrite Qinv_plus_distr. reflexivity. @@ -501,7 +496,7 @@ Lemma CRmorph_mult_inv : forall {R1 R2 : ConstructiveReals} Proof. intros. apply (CRmult_eq_reg_r (CR_of_Q R2 (Z.pos p # 1))). left. apply (CRle_lt_trans _ (CR_of_Q R2 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. reflexivity. + apply CRle_refl. apply CR_of_Q_lt. reflexivity. apply (CReq_trans _ (CRmorph f x)). - apply (CReq_trans _ (CRmorph f (CRmult R1 (CRmult R1 x (CR_of_Q R1 (1 # p))) @@ -511,22 +506,22 @@ Proof. _ (CRmult R1 x (CRmult R1 (CR_of_Q R1 (1 # p)) (CR_of_Q R1 (Z.pos p # 1))))). destruct (CRisRing R1). apply CReq_sym, Rmul_assoc. - apply (CReq_trans _ (CRmult R1 x (CRone R1))). + apply (CReq_trans _ (CRmult R1 x 1)). apply (Rmul_ext (CRisRingExt R1)). apply CReq_refl. apply (CReq_trans _ (CR_of_Q R1 ((1#p) * (Z.pos p # 1)))). apply CReq_sym, CR_of_Q_mult. apply (CReq_trans _ (CR_of_Q R1 1)). - apply CR_of_Q_morph. reflexivity. apply CR_of_Q_one. + apply CR_of_Q_morph. reflexivity. reflexivity. apply CRmult_1_r. - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRmult R2 (CR_of_Q R2 (1 # p)) (CR_of_Q R2 (Z.pos p # 1))))). 2: apply (Rmul_assoc (CRisRing R2)). - apply (CReq_trans _ (CRmult R2 (CRmorph f x) (CRone R2))). + apply (CReq_trans _ (CRmult R2 (CRmorph f x) 1)). apply CReq_sym, CRmult_1_r. apply (Rmul_ext (CRisRingExt R2)). apply CReq_refl. apply (CReq_trans _ (CR_of_Q R2 1)). - apply CReq_sym, CR_of_Q_one. + reflexivity. apply (CReq_trans _ (CR_of_Q R2 ((1#p)*(Z.pos p # 1)))). apply CR_of_Q_morph. reflexivity. apply CR_of_Q_mult. Qed. @@ -571,7 +566,7 @@ Qed. Lemma CRmorph_mult_pos_pos_le : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), - CRlt R1 (CRzero R1) y + CRlt R1 0 y -> CRmult R2 (CRmorph f x) (CRmorph f y) <= CRmorph f (CRmult R1 x y). Proof. @@ -590,20 +585,20 @@ Proof. apply Qlt_minus_iff in H1. rewrite H4 in H1. inversion H1. } destruct (CR_Q_dense R1 (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A)))) x) as [s [H4 H5]]. - - apply (CRlt_le_trans _ (CRplus R1 x (CRzero R1))). + - apply (CRlt_le_trans _ (CRplus R1 x 0)). 2: apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRplus_lt_reg_l R1 (CR_of_Q R1 ((r-q) * (1#A)))). - apply (CRle_lt_trans _ (CRzero R1)). + apply (CRle_lt_trans _ 0). apply (CRle_trans _ (CR_of_Q R1 ((r-q)*(1#A) + (q-r)*(1#A)))). destruct (CR_of_Q_plus R1 ((r-q)*(1#A)) ((q-r)*(1#A))). exact H0. apply (CRle_trans _ (CR_of_Q R1 0)). - 2: destruct (@CR_of_Q_zero R1); exact H4. + 2: apply CRle_refl. intro H4. apply lt_CR_of_Q in H4. ring_simplify in H4. inversion H4. apply (CRlt_le_trans _ (CR_of_Q R1 ((r - q) * (1 # A)))). 2: apply CRplus_0_r. apply (CRle_lt_trans _ (CR_of_Q R1 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. + apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. apply Qlt_minus_iff in H1. exact H1. reflexivity. - apply (CRmorph_increasing f) in H4. @@ -637,7 +632,7 @@ Proof. apply (CRlt_le_trans _ (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). apply (CRmult_lt_reg_l (CR_of_Q R2 (/((r-q)*(1#A))))). - apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl. apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (r-q)). apply Qmult_lt_l. apply Qlt_minus_iff in H1. exact H1. reflexivity. @@ -655,24 +650,24 @@ Proof. apply (CRlt_le_trans _ (CRmorph f (CR_of_Q R1 (Z.pos A # 1)))). apply CRmorph_increasing. exact Amaj. destruct (CRmorph_rat f (Z.pos A # 1)). exact H4. - apply (CRle_trans _ (CRmult R2 (CRopp R2 (CRone R2)) (CRmorph f y))). - apply (CRle_trans _ (CRopp R2 (CRmult R2 (CRone R2) (CRmorph f y)))). + apply (CRle_trans _ (CRmult R2 (CRopp R2 1) (CRmorph f y))). + apply (CRle_trans _ (CRopp R2 (CRmult R2 1 (CRmorph f y)))). destruct (Ropp_ext (CRisRingExt R2) (CRmorph f y) - (CRmult R2 (CRone R2) (CRmorph f y))). + (CRmult R2 1 (CRmorph f y))). apply CReq_sym, (Rmul_1_l (CRisRing R2)). exact H4. - destruct (CRopp_mult_distr_l (CRone R2) (CRmorph f y)). exact H4. + destruct (CRopp_mult_distr_l 1 (CRmorph f y)). exact H4. apply (CRle_trans _ (CRmult R2 (CRmult R2 (CR_of_Q R2 (/ ((r - q) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A)))) (CRmorph f y))). apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. apply (CRle_trans _ (CR_of_Q R2 ((/ ((r - q) * (1 # A))) * ((q - r) * (1 # A))))). apply (CRle_trans _ (CR_of_Q R2 (-1))). apply (CRle_trans _ (CRopp R2 (CR_of_Q R2 1))). - destruct (Ropp_ext (CRisRingExt R2) (CRone R2) (CR_of_Q R2 1)). - apply CReq_sym, CR_of_Q_one. exact H4. + destruct (Ropp_ext (CRisRingExt R2) 1 (CR_of_Q R2 1)). + reflexivity. exact H4. destruct (@CR_of_Q_opp R2 1). exact H0. destruct (CR_of_Q_morph R2 (-1) (/ ((r - q) * (1 # A)) * ((q - r) * (1 # A)))). field. split. @@ -685,7 +680,7 @@ Proof. (CRmorph f y)). exact H0. apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H0. + apply (CRle_trans _ (CRmorph f (CRmult R1 y (CR_of_Q R1 s)))). @@ -696,14 +691,14 @@ Proof. destruct (CRmorph_proper f (CRmult R1 y (CR_of_Q R1 s)) (CRmult R1 (CR_of_Q R1 s) y)). apply (Rmul_comm (CRisRing R1)). exact H4. - + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. Qed. Lemma CRmorph_mult_pos_pos : forall {R1 R2 : ConstructiveReals} (f : @ConstructiveRealsMorphism R1 R2) (x y : CRcarrier R1), - CRlt R1 (CRzero R1) y + CRlt R1 0 y -> CRmorph f (CRmult R1 x y) == CRmult R2 (CRmorph f x) (CRmorph f y). Proof. @@ -718,10 +713,10 @@ Proof. destruct (CR_archimedean R1 y) as [A Amaj]. destruct (CR_Q_dense R1 x (CRplus R1 x (CR_of_Q R1 ((q-r) * (1#A))))) as [s [H4 H5]]. - - apply (CRle_lt_trans _ (CRplus R1 x (CRzero R1))). + - apply (CRle_lt_trans _ (CRplus R1 x 0)). apply CRplus_0_r. apply CRplus_lt_compat_l. apply (CRle_lt_trans _ (CR_of_Q R1 0)). - apply CR_of_Q_zero. apply CR_of_Q_lt. + apply CRle_refl. apply CR_of_Q_lt. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. apply Qlt_minus_iff in H3. exact H3. reflexivity. - apply (CRmorph_increasing f) in H5. @@ -763,14 +758,14 @@ Proof. (CRmult R2 (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y)))). apply CRplus_le_compat_l, CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. destruct (CRmorph_rat f ((q - r) * (1 # A))). exact H2. apply (CRlt_le_trans _ (CRplus R2 (CR_of_Q R2 r) (CR_of_Q R2 ((q - r))))). apply CRplus_lt_compat_l. * apply (CRmult_lt_reg_l (CR_of_Q R2 (/((q - r) * (1 # A))))). - apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CR_of_Q_zero. + apply (CRle_lt_trans _ (CR_of_Q R2 0)). apply CRle_refl. apply CR_of_Q_lt, Qinv_lt_0_compat. rewrite <- (Qmult_0_r (q-r)). apply Qmult_lt_l. apply Qlt_minus_iff in H3. exact H3. reflexivity. @@ -781,9 +776,9 @@ Proof. exact (proj2 (Rmul_assoc (CRisRing R2) (CR_of_Q R2 (/ ((q - r) * (1 # A)))) (CR_of_Q R2 ((q - r) * (1 # A))) (CRmorph f y))). - apply (CRle_trans _ (CRmult R2 (CRone R2) (CRmorph f y))). + apply (CRle_trans _ (CRmult R2 1 (CRmorph f y))). apply CRmult_le_compat_r_half. - apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. apply (CRle_trans _ (CR_of_Q R2 ((/ ((q - r) * (1 # A))) * ((q - r) * (1 # A))))). @@ -793,7 +788,7 @@ Proof. field_simplify. reflexivity. split. intro H5. inversion H5. intro H5. apply Qlt_minus_iff in H3. rewrite H5 in H3. inversion H3. exact H2. - destruct (CR_of_Q_one R2). exact H2. + apply CRle_refl. destruct (Rmul_1_l (CRisRing R2) (CRmorph f y)). intro H5. contradiction. apply (CRlt_le_trans _ (CR_of_Q R2 (Z.pos A # 1))). @@ -809,7 +804,7 @@ Proof. * apply (CRle_trans _ (CR_of_Q R2 (r + (q-r)))). exact (proj1 (CR_of_Q_plus R2 r (q-r))). destruct (CR_of_Q_morph R2 (r + (q-r)) q). ring. exact H2. - + apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + + apply (CRle_lt_trans _ (CRmorph f 0)). apply CRmorph_zero. apply CRmorph_increasing. exact H. Qed. @@ -867,10 +862,10 @@ Lemma CRmorph_appart_zero : forall {R1 R2 : ConstructiveReals} CRmorph f x ≶ 0. Proof. intros. destruct app. - - left. apply (CRlt_le_trans _ (CRmorph f (CRzero R1))). + - left. apply (CRlt_le_trans _ (CRmorph f 0)). apply CRmorph_increasing. exact c. exact (proj2 (CRmorph_zero f)). - - right. apply (CRle_lt_trans _ (CRmorph f (CRzero R1))). + - right. apply (CRle_lt_trans _ (CRmorph f 0)). exact (proj1 (CRmorph_zero f)). apply CRmorph_increasing. exact c. Defined. @@ -885,7 +880,7 @@ Lemma CRmorph_inv : forall {R1 R2 : ConstructiveReals} Proof. intros. apply (CRmult_eq_reg_r (CRmorph f x)). destruct fxnz. right. exact c. left. exact c. - apply (CReq_trans _ (CRone R2)). + apply (CReq_trans _ 1). 2: apply CReq_sym, CRinv_l. apply (CReq_trans _ (CRmorph f (CRmult R1 ((/ x) xnz) x))). apply CReq_sym, CRmorph_mult. @@ -915,11 +910,11 @@ Proof. - simpl. unfold INR. rewrite (CRmorph_proper f _ (1 + CR_of_Q R1 (Z.of_nat n # 1))). rewrite CRmorph_plus. unfold INR in IHn. - rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_one, <- CR_of_Q_plus. + rewrite IHn. rewrite CRmorph_one, <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. - rewrite <- CR_of_Q_one, <- CR_of_Q_plus. + rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. rewrite Nat2Z.inj_succ. rewrite <- Z.add_1_l. reflexivity. @@ -1047,7 +1042,7 @@ Proof. apply Pos2Z.pos_le_pos, Pos2Nat.inj_le. rewrite Nat2Pos.id. exact H0. destruct i. inversion H0. pose proof (Pos2Nat.is_pos p). rewrite H2 in H1. inversion H1. discriminate. - rewrite <- CR_of_Q_zero. apply CR_of_Q_le. discriminate. + apply CR_of_Q_le. discriminate. rewrite CRplus_0_r. reflexivity. } pose proof (CR_cv_open_above _ _ _ H0 H) as [n nmaj]. apply (CRle_lt_trans _ (CR_of_Q R2 (let (q0, _) := CR_Q_limit x n in diff --git a/theories/Reals/Abstract/ConstructiveSum.v b/theories/Reals/Abstract/ConstructiveSum.v index 11c8e5d8a2..3be03bf615 100644 --- a/theories/Reals/Abstract/ConstructiveSum.v +++ b/theories/Reals/Abstract/ConstructiveSum.v @@ -60,11 +60,11 @@ Lemma sum_const : forall {R : ConstructiveReals} (a : CRcarrier R) (n : nat), CRsum (fun _ => a) n == a * INR (S n). Proof. induction n. - - unfold INR. simpl. rewrite CR_of_Q_one, CRmult_1_r. reflexivity. + - unfold INR. simpl. rewrite CRmult_1_r. reflexivity. - simpl. rewrite IHn. unfold INR. replace (Z.of_nat (S (S n))) with (Z.of_nat (S n) + 1)%Z. rewrite <- Qinv_plus_distr, CR_of_Q_plus, CRmult_plus_distr_l. - apply CRplus_morph. reflexivity. rewrite CR_of_Q_one, CRmult_1_r. reflexivity. + apply CRplus_morph. reflexivity. rewrite CRmult_1_r. reflexivity. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add. apply f_equal. rewrite Nat.add_comm. reflexivity. reflexivity. Qed. diff --git a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v index 5fc3a0e653..f4daedcb97 100644 --- a/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v +++ b/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v @@ -189,49 +189,63 @@ Proof. intros. rewrite CReal_mult_comm. apply CReal_mult_0_r. Qed. -Lemma CReal_mult_lt_0_compat : forall x y : CReal, - inject_Q 0 < x - -> inject_Q 0 < y - -> inject_Q 0 < x * y. +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. + +(* 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 limx) as majx. - pose proof (QCauchySeq_bounded_prop yn 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) @@ -777,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), @@ -904,98 +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.max n k)). -Proof. - intros x k n p q H0 H1. - destruct x as [xn cau]; unfold proj1_sig. - apply cau. exact (Pos.le_trans _ _ _ H0 (Pos.le_max_l _ _)). - exact (Pos.le_trans _ _ _ H1 (Pos.le_max_l _ _)). -Qed. - -Lemma CRealShiftEqual : forall (x : CReal) (k : positive), - x == exist _ (fun n => proj1_sig x (Pos.max n k)) (CRealShiftReal x k). -Proof. - intros. split. - - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (Pos.max n k) n (Pos.le_max_l _ _ ) (Pos.le_refl _)). - apply (Qlt_not_le _ _ maj). clear maj. - apply (Qle_trans _ (Qabs (xn (Pos.max n k) - xn n))). - apply Qle_Qabs. apply Qlt_le_weak. apply (Qlt_trans _ _ _ cau). - unfold Qlt, Qnum, Qden. - apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity. - - intros [n maj]. destruct x as [xn cau]; simpl in maj. - specialize (cau n (Pos.max n k) n (Pos.le_max_l _ _ ) (Pos.le_refl _)). - apply (Qlt_not_le _ _ maj). clear maj. - rewrite Qabs_Qminus in cau. - apply (Qle_trans _ (Qabs (xn n - xn (Pos.max n k)))). - apply Qle_Qabs. apply Qlt_le_weak. apply (Qlt_trans _ _ _ cau). - unfold Qlt, Qnum, Qden. - apply Z.mul_lt_mono_pos_r. reflexivity. reflexivity. -Qed. - -(* Find a positive negative real number, which rational sequence - stays above 0, so that it can be inversed. *) -Definition CRealPosShift (x : CReal) (xPos : 0 < x) : positive - := let (n,maj) := xPos in - let (a,_) := Qarchimedean (/ (proj1_sig x n - 0 - (2 # n))) in - Pos.max n (2*a). - +(* 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), - Qlt (1 # CRealPosShift x xPos) (proj1_sig x (Pos.max n (CRealPosShift x xPos))). -Proof. - intros x xPos p. unfold CRealPosShift. - pose proof (CRealLt_aboveSig 0 x) as H. - destruct xPos as [n maj], x as [xn cau]; simpl in maj. - unfold inject_Q, proj1_sig in H. specialize (H n maj). - simpl. - destruct (Qarchimedean (/ (xn n - 0 - (2 # n)))) as [a _]. - apply (Qlt_trans _ (2 # (Pos.max n (2*a)))). - apply Z.mul_lt_mono_pos_r; reflexivity. - specialize (H (Pos.max p (Pos.max n (2*a))) (Pos.le_max_r _ _)). - apply (Qlt_le_trans _ _ _ H). ring_simplify. apply Qle_refl. + 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_pos_cauchy : forall (x : CReal) (xPos : 0 < x), - QCauchySeq (fun n : positive - => / proj1_sig x (Pos.max ((CRealPosShift x xPos) ^ 2 * n) - (CRealPosShift x xPos))). +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. - remember (CRealPosShift x xPos) as k. - pose (fun n : positive => proj1_sig x (Pos.max n k)) as yn. - pose proof (CRealShiftReal x k) as cau. - pose proof (CRealPosShift_correct x xPos) as maj. + intros [xn xcau] xPos k maj. unfold proj1_sig. intros n p q H0 H1. - setoid_replace - (/ proj1_sig x (Pos.max (k ^ 2 * p) k) - / proj1_sig x (Pos.max (k ^ 2 * q) k))%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) + 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)))). - rewrite <- Heqk in maj. 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 * 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. @@ -1004,37 +980,40 @@ 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. apply Pos.mul_le_mono_l. exact H0. rewrite factorDenom. apply Qle_refl. - + unfold yn. field. split. intro abs. + + field. split. intro abs. specialize (maj (k ^ 2 * p)%positive). - rewrite <- Heqk in maj. - 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 <- Heqk in maj. - 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_pos (x : CReal) (xPos : 0 < x) : CReal - := exist _ (fun n : positive - => / proj1_sig x (Pos.max ((CRealPosShift x xPos) ^ 2 * n) - (CRealPosShift x xPos))) - (CReal_inv_pos_cauchy x xPos). + := 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)). -Lemma CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. +Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x. Proof. - intros. apply (CReal_plus_lt_reg_l x). - rewrite (CReal_plus_opp_r x), CReal_plus_0_r. exact H. -Qed. + 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 @@ -1051,35 +1030,30 @@ Proof. intros. unfold CReal_inv. simpl. destruct rnz. - exfalso. apply CRealLt_asym in H. contradiction. - - remember (CRealPosShift r c) as k. - unfold CReal_inv_pos. - pose (CRealPosShift_correct r c) as maj. - rewrite <- Heqk in maj. - pose (fun n => proj1_sig r (Pos.max n (CRealPosShift r c))) as rn. + - 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. - simpl in rn. rewrite <- Heqk. - rewrite <- (Qmult_1_l (/ xn (Pos.max (k ^ 2 * (2 * (A + 1))) k))). - 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 <- (Qplus_lt_l _ _ (- rn 1%positive)). - apply (Qle_lt_trans _ (Qabs (rn (k ^ 2 * (2 * (A + 1)))%positive + - rn 1%positive))). - unfold rn. rewrite <- Heqk. + 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. - rewrite <- Heqk. - destruct (Pos.max (k ^ 2 * (2 * (A + 1))) k)%positive; discriminate. - apply Pos.le_max_l. + 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). @@ -1111,34 +1085,33 @@ Lemma CReal_inv_l_pos : forall (r:CReal) (rnz : 0 < r), (CReal_inv_pos r rnz) * r == 1. Proof. intros r c. - remember (CRealPosShift r c) as k. unfold CReal_inv_pos. pose proof (CRealPosShift_correct r c) as maj. - rewrite <- Heqk in maj. - pose (exist (fun x => QCauchySeq x) - (fun n => proj1_sig r (Pos.max n k)) (CRealShiftReal r k)) - as rshift. rewrite (CReal_mult_proper_l - _ r (exist _ (fun n => proj1_sig rshift (k ^ 2 * n)%positive) - (CReal_linear_shift rshift _))). - 2: rewrite <- CReal_linear_shift_eq; apply CRealShiftEqual. - 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. } + _ 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, rshift, inject_Q, proj1_sig. - rewrite <- Heqk, Qmult_comm, Qmult_inv_r. + 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. intro abs. + discriminate. apply Qle_refl. unfold proj1_sig in maj. - remember (QCauchySeq_bound - (fun n0 : positive => / rn (Pos.max (k ^ 2 * n0) k)) - id)%Q as x. - remember (QCauchySeq_bound - (fun n0 : positive => rn (Pos.max (k ^ 2 * n0) k)%positive) - id) as x0. - specialize (maj ((k * (k * 1) * (Pos.max x x0 * n)~0)%positive)). - simpl in maj. rewrite abs in maj. inversion 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), diff --git a/theories/Reals/Cauchy/ConstructiveRcomplete.v b/theories/Reals/Cauchy/ConstructiveRcomplete.v index be844c413a..754f9be5fe 100644 --- a/theories/Reals/Cauchy/ConstructiveRcomplete.v +++ b/theories/Reals/Cauchy/ConstructiveRcomplete.v @@ -309,12 +309,11 @@ Definition CRealConstructive : ConstructiveReals := Build_ConstructiveReals CReal CRealLt CRealLtIsLinear CRealLtProp CRealLtEpsilon CRealLtForget CRealLtDisjunctEpsilon - (inject_Q 0) (inject_Q 1) + inject_Q inject_Q_lt lt_inject_Q CReal_plus CReal_opp CReal_mult + inject_Q_plus inject_Q_mult CReal_isRing CReal_isRingExt CRealLt_0_1 CReal_plus_lt_compat_l CReal_plus_lt_reg_l CReal_mult_lt_0_compat CReal_inv CReal_inv_l CReal_inv_0_lt_compat - inject_Q inject_Q_plus inject_Q_mult - inject_Q_one inject_Q_lt lt_inject_Q CRealQ_dense Rup_pos CReal_abs CRealAbsLUB CRealComplete. 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 |