diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-12 17:49:21 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-12 17:49:21 +0000 |
| commit | cb1ae314411d78952062e5092804b85d981ad6e1 (patch) | |
| tree | 52b9a4058c89b5849d875a4c1129951f35e9c1b1 /theories | |
| parent | 7cb6a61133b6e3c2cd5601282a1f472ff0104c1f (diff) | |
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
83 files changed, 343 insertions, 202 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 112edaa56..5711a81a7 100755 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -10,6 +10,7 @@ Require Le. Require Lt. +Import nat_scope. Section Between. Variables P,Q : nat -> Prop. diff --git a/theories/Arith/Bool_nat.v b/theories/Arith/Bool_nat.v index 872c314f1..bbe1475f5 100644 --- a/theories/Arith/Bool_nat.v +++ b/theories/Arith/Bool_nat.v @@ -11,6 +11,7 @@ Require Export Compare_dec. Require Export Peano_dec. Require Sumbool. +Import nat_scope. (** The decidability of equality and order relations over type [nat] give some boolean functions with the adequate specification. *) diff --git a/theories/Arith/Compare.v b/theories/Arith/Compare.v index f98115e6b..5b12033dc 100755 --- a/theories/Arith/Compare.v +++ b/theories/Arith/Compare.v @@ -9,6 +9,7 @@ (*i $Id$ i*) (** Equality is decidable on [nat] *) +Import nat_scope. Lemma not_eq_sym : (A:Set)(p,q:A)(~p=q) -> ~(q=p). Proof sym_not_eq. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 67218de83..735d267d6 100755 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -12,6 +12,7 @@ Require Le. Require Lt. Require Gt. Require Decidable. +Import nat_scope. Definition zerop : (n:nat){n=O}+{lt O n}. NewDestruct n; Auto with arith. diff --git a/theories/Arith/Div.v b/theories/Arith/Div.v index 2b7cfac14..e4b0300dd 100755 --- a/theories/Arith/Div.v +++ b/theories/Arith/Div.v @@ -9,6 +9,7 @@ (*i $Id$ i*) (** Euclidean division *) +Import nat_scope. Require Le. Require Euclid_def. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index f039aa7a0..dd0cc8458 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -12,6 +12,7 @@ Require Lt. Require Plus. Require Compare_dec. Require Even. +Import nat_scope. (** Here we define [n/2] and prove some of its properties *) diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index b4a232e20..88cca274b 100755 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -9,6 +9,7 @@ (*i $Id$ i*) (** Equality on natural numbers *) +Import nat_scope. Fixpoint eq_nat [n:nat] : nat -> Prop := [m:nat]Cases n m of diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index 5a2dd1a84..173a90638 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -11,6 +11,7 @@ Require Mult. Require Compare_dec. Require Wf_nat. +Import nat_scope. Inductive diveucl [a,b:nat] : Set diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 074e0a03d..034a60088 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -11,6 +11,7 @@ (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) +Import nat_scope. Inductive even : nat->Prop := even_O : (even O) diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index f31154018..6b55c5bd3 100755 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -11,6 +11,7 @@ Require Le. Require Lt. Require Plus. +Import nat_scope. Theorem gt_Sn_O : (n:nat)(gt (S n) O). Proof. diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 9bdb7dc23..7765187cf 100755 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -9,6 +9,8 @@ (*i $Id$ i*) (** Order on natural numbers *) +Import nat_scope. +Open Scope nat_scope. Theorem le_n_S : (n,m:nat)(le n m)->(le (S n) (S m)). Proof. diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 711e065da..96541cb9f 100755 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Le. +Import nat_scope. Theorem lt_n_Sn : (n:nat)(lt n (S n)). Proof. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 43c683a90..8a599ed7e 100755 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Arith. +Import nat_scope. (** maximum of two natural numbers *) diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index 8a5de8703..650b95380 100755 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Arith. +Import nat_scope. (** minimum of two natural numbers *) diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 0f435a560..42f44083a 100755 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -12,6 +12,7 @@ Require Lt. Require Le. +Import nat_scope. Fixpoint minus [n:nat] : nat -> nat := [m:nat]Cases n m of diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index ac16d4cb9..1daf8567c 100755 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -11,6 +11,7 @@ Require Export Plus. Require Export Minus. Require Export Lt. +Import nat_scope. (** Multiplication *) diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 694351b67..e998e0b7c 100755 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -9,6 +9,7 @@ (*i $Id$ i*) Require Decidable. +Import nat_scope. Theorem O_or_S : (n:nat)({m:nat|(S m)=n})+{O=n}. Proof. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 581b45851..b0c715c8b 100755 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -12,6 +12,8 @@ Require Lt. +Import nat_scope. + Chapter Well_founded_Nat. Variable A : Set. diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v index 06f28b503..0ba1a5884 100644 --- a/theories/Init/DatatypesSyntax.v +++ b/theories/Init/DatatypesSyntax.v @@ -15,10 +15,12 @@ Require Export Datatypes. Arguments Scope sum [type_scope type_scope]. Arguments Scope prod [type_scope type_scope]. -Infix "+" sum (at level 4, left associativity) : type_scope. -Infix "*" prod (at level 3, right associativity) : type_scope. +Infix LEFTA 4 "+" sum : type_scope. +Notation "x * y" := (prod x y) (at level 3, right associativity) : type_scope + V8only (at level 30, left associativity). -Notation "( x , y )" := (pair ? ? x y) (at level 0). +Notation "( x , y )" := (pair ? ? x y) (at level 0) + V8only "x , y" (at level 150, left associativity). Notation Fst := (fst ? ?). Notation Snd := (snd ? ?). @@ -26,7 +28,8 @@ Arguments Scope option [ type_scope ]. (** Parsing only of things in [Datatypes.v] *) +V7only[ Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot). Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot). Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot). - +]. diff --git a/theories/Init/LogicSyntax.v b/theories/Init/LogicSyntax.v index 2ad45477f..c652a7028 100644 --- a/theories/Init/LogicSyntax.v +++ b/theories/Init/LogicSyntax.v @@ -11,36 +11,49 @@ Require Export Logic. (** Symbolic notations for things in [Logic.v] *) - +V7only[ Notation "< P , Q > { p , q }" := (conj P Q p q) (P annot, at level 1). +]. -Notation "~ x" := (not x) (at level 5, right associativity). -Notation "x = y" := (eq ? x y) (at level 5, no associativity). +Notation "~ x" := (not x) (at level 5, right associativity) + V8only (at level 55, right associativity). +Notation "x = y" := (eq ? x y) (at level 5, no associativity) + V8only (at level 50, no associativity). Infix RIGHTA 6 "/\\" and. Infix RIGHTA 7 "\\/" or. Infix RIGHTA 8 "<->" iff. Notation "'IF' c1 'then' c2 'else' c3" := (IF c1 c2 c3) - (at level 1, c1, c2, c3 at level 8). + (at level 1, c1, c2, c3 at level 8) + V8only (at level 200). (* Order is important to give printing priority to fully typed ALL and EX *) +Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8) + V8only (at level 200). +Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8) + V8only (at level 200, p at level 200). Notation All := (all ?). -Notation "'ALL' x | p" := (all ? [x]p) (at level 10, p at level 8). -Notation "'ALL' x : t | p" := (all t [x:t]p) (at level 10, p at level 8). +Notation "'EX' x : t | p" := (ex t [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). +Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). Notation Ex := (ex ?). -Notation "'EX' x | p" := (ex ? [x]p) (at level 10, p at level 8). -Notation "'EX' x : t | p" := (ex t [x:t]p) (at level 10, p at level 8). -Notation Ex2 := (ex2 ?). -Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) - (at level 10, p, q at level 8). Notation "'EX' x : t | p & q" := (ex2 t [x:t]p [x:t]q) - (at level 10, p, q at level 8). + (at level 10, p, q at level 8) + V8only "'EX2' x : t | p & q" (at level 200, x at level 80). +Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) + (at level 10, p, q at level 8) + V8only "'EX2' x | p & q" (at level 200, x at level 80). +Notation Ex2 := (ex2 ?). (** Parsing only of things in [Logic.v] *) +V7only[ Notation "< A > 'All' ( P )" := (all A P) (A annot, at level 1, only parsing). -Notation "< A > x = y" := (eq A x y) (A annot, at level 1, x at level 0, only parsing). +Notation "< A > x = y" := (eq A x y) + (A annot, at level 1, x at level 0, only parsing). +]. diff --git a/theories/Init/Logic_TypeSyntax.v b/theories/Init/Logic_TypeSyntax.v index ed915d119..08d4f47c5 100644 --- a/theories/Init/Logic_TypeSyntax.v +++ b/theories/Init/Logic_TypeSyntax.v @@ -12,29 +12,39 @@ Require Logic_Type. (** Symbolic notations for things in [Logic_type.v] *) -Notation "x == y" := (eqT ? x y) (at level 5, no associativity). -Notation "x === y" := (identityT ? x y) (at level 5, no associativity). +Notation "x == y" := (eqT ? x y) (at level 5, no associativity) + V8only (at level 50, no associativity). +Notation "x === y" := (identityT ? x y) (at level 5, no associativity) + V8only (at level 50, no associativity). (* Order is important to give printing priority to fully typed ALL and EX *) +Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). +Notation "'ALLT' x | p" := (allT ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). Notation AllT := (allT ?). -Notation "'ALLT' x : t | p" := (allT t [x:t]p) (at level 10, p at level 8). -Notation "'ALLT' x | p" := (allT ? [x]p) (at level 10, p at level 8). +Notation "'EXT' x : t | p" := (exT t [x:t]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). +Notation "'EXT' x | p" := (exT ? [x]p) (at level 10, p at level 8) + V8only (at level 200, x at level 80). Notation ExT := (exT ?). -Notation "'EXT' x : t | p" := (exT t [x:t]p) (at level 10, p at level 8). -Notation "'EXT' x | p" := (exT ? [x]p) (at level 10, p at level 8). -Notation ExT2 := (exT2 ?). Notation "'EXT' x : t | p & q" := (exT2 t [x:t]p [x:t]q) - (at level 10, p, q at level 8). + (at level 10, p, q at level 8) + V8only "'EXT2' x : t | p & q" (at level 200, x at level 80). Notation "'EXT' x | p & q" := (exT2 ? [x]p [x]q) - (at level 10, p, q at level 8). + (at level 10, p, q at level 8) + V8only "'EXT2' x | p & q" (at level 200, x at level 80). +Notation ExT2 := (exT2 ?). (** Parsing only of things in [Logic_type.v] *) +V7only[ Notation "< A > x == y" := (eqT A x y) (A annot, at level 1, x at level 0, only parsing). Notation "< A > x === y" := (identityT A x y) (A annot, at level 1, x at level 0, only parsing). +]. diff --git a/theories/Init/PeanoSyntax.v b/theories/Init/PeanoSyntax.v index e76dbe665..2f53ca9b2 100644 --- a/theories/Init/PeanoSyntax.v +++ b/theories/Init/PeanoSyntax.v @@ -10,32 +10,26 @@ Require Datatypes. Require Peano. +V7only[ Syntax constr level 0: S [ (S $p) ] -> [$p:"nat_printer":9] | O [ O ] -> ["(0)"]. - +]. (* Outside the module to be able to parse the grammar for 0,1,2... !! *) Delimits Scope nat_scope with N. (* For parsing/printing based on scopes *) Module nat_scope. -Infix "+" plus (at level 4) : nat_scope. -Infix "*" mult (at level 3): nat_scope. -Infix "<=" le (at level 5, no associativity) : nat_scope. -Infix "<" lt (at level 5, no associativity) : nat_scope. -Infix ">=" ge (at level 5, no associativity) : nat_scope. -Infix ">" gt (at level 5, no associativity) : nat_scope. - (* Warning: this hides sum and prod and breaks sumor symbolic notation *) Open Scope nat_scope. -(* -Syntax constr - level 0: - S' [ (S $p) ] -> [$p:"nat_printer_S":9] -| O' [ O ] -> [ _:"nat_printer_O" ] -. -*) +Infix 4 "+" plus : nat_scope V8only 40. +Infix 3 "*" mult : nat_scope V8only 30. +Infix NONA 5 "<=" le : nat_scope V8only 50. +Infix NONA 5 "<" lt : nat_scope V8only 50. +Infix NONA 5 ">=" ge : nat_scope V8only 50. +Infix NONA 5 ">" gt : nat_scope V8only 50. + End nat_scope. diff --git a/theories/Init/SpecifSyntax.v b/theories/Init/SpecifSyntax.v index 9d868cb54..b8bb1dec6 100644 --- a/theories/Init/SpecifSyntax.v +++ b/theories/Init/SpecifSyntax.v @@ -11,12 +11,34 @@ Require DatatypesSyntax. Require Specif. +(** Extra factorization of parsing rules *) + +(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) + +Notation "B + { x : A | P }" := B + (sig A [x:A]P) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + +Notation "B + { x : A | P & Q }" := B + (sig2 A [x:A]P [x:A]Q) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + +Notation "B + { x : A & P }" := B + (sigS A [x:A]P) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + +Notation "B + { x : A & P & Q }" := B + (sigS2 A [x:A]P [x:A]Q) + (at level 4, left associativity, only parsing) + V8only (at level 40, x at level 80, left associativity, only parsing). + (** Symbolic notations for things in [Specif.v] *) (* At level 1 to factor with {x:A|P} etc *) -Notation "{ A } + { B }" := (sumbool A B) (at level 1). +Notation "{ A } + { B }" := (sumbool A B) (at level 1) + V8only (at level 10, A at level 80). -Notation "A + { B }" := (sumor A B) (at level 4, left associativity). +Notation "A + { B }" := (sumor A B) (at level 4, left associativity) + V8only (at level 40, B at level 80, left associativity). Notation ProjS1 := (projS1 ? ?). Notation ProjS2 := (projS2 ? ?). @@ -27,28 +49,15 @@ Notation Value := (value ?). Arguments Scope sig [type_scope type_scope]. Arguments Scope sig2 [type_scope type_scope type_scope]. -Notation "{ x : A | P }" := (sig A [x:A]P) (at level 1). -Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) (at level 1). +Notation "{ x : A | P }" := (sig A [x:A]P) (at level 1) + V8only (at level 10, x at level 80). +Notation "{ x : A | P & Q }" := (sig2 A [x:A]P [x:A]Q) (at level 1) + V8only (at level 10, x at level 80). Arguments Scope sigS [type_scope type_scope]. Arguments Scope sigS2 [type_scope type_scope type_scope]. -Notation "{ x : A & P }" := (sigS A [x:A]P) (at level 1). -Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1). - -(** Extra factorization of parsing rules *) - -(* Factorizing "sumor" at level 4 to parse B+{x:A|P} without parentheses *) - -Notation "B + { x : A | P }" := B + ({x:A | P}) - (at level 4, left associativity, only parsing). - -Notation "B + { x : A | P & Q }" := B + ({x:A | P & Q}) - (at level 4, left associativity, only parsing). - -Notation "B + { x : A & P }" := B + ({x:A & P}) - (at level 4, left associativity, only parsing). - -Notation "B + { x : A & P & Q }" := B + ({x:A & P & Q}) - (at level 4, left associativity, only parsing). - +Notation "{ x : A & P }" := (sigS A [x:A]P) (at level 1) + V8only (at level 10, x at level 80). +Notation "{ x : A & P & Q }" := (sigS2 A [x:A]P [x:A]Q) (at level 1) + V8only (at level 10, x at level 80). diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 745af5ef6..4fb640827 100755 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -107,7 +107,7 @@ Apply F_ext; Auto. Qed. -Lemma fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). +Lemma Fix_eq : (x:A)(fix x)=(F x [y:A][p:(R y x)](fix y)). Intro; Unfold fix. Case (Fix_F_eq x). Apply F_ext; Intros. diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index cd56ba1de..5baa76891 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -38,7 +38,8 @@ Fixpoint app [l:list] : list -> list | (cons a l1) => (cons a (app l1 m)) end. -Infix RIGHTA 7 "^" app. +Infix RIGHTA 7 "^" app + V8only 30. Lemma app_nil_end : (l:list)l=(l^nil). Proof. diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v index dd7aba8c9..b74da123f 100644 --- a/theories/Lists/PolyListSyntax.v +++ b/theories/Lists/PolyListSyntax.v @@ -12,4 +12,5 @@ Require PolyList. -Infix RIGHTA 7 "^" app. +Infix RIGHTA 7 "^" app + V8only 30. diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index c87053772..e86a4d003 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -14,6 +14,7 @@ Require Rseries. Require SeqProp. Require PartSum. Require Max. +Import R_scope. (***************************************************) (* Various versions of the criterion of D'Alembert *) @@ -544,4 +545,4 @@ Unfold Rdiv; Apply Rmult_lt_pos. Assumption. Apply Rlt_Rinv; Apply Rabsolu_pos_lt. Red; Intro H7; Rewrite H7 in r; Elim (Rlt_antirefl ? r). -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v index d9477c50d..5c7f02d4d 100644 --- a/theories/Reals/AltSeries.v +++ b/theories/Reals/AltSeries.v @@ -14,6 +14,7 @@ Require Rseries. Require SeqProp. Require PartSum. Require Max. +Import R_scope. (**********) Definition tg_alt [Un:nat->R] : nat->R := [i:nat]``(pow (-1) i)*(Un i)``. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 3436a2558..18e833e69 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -12,6 +12,7 @@ Require Rbase. Require Rbasic_fun. Require Even. Require Div2. +Import R_scope. Lemma minus_neq_O : (n,i:nat) (lt i n) -> ~(minus n i)=O. Intros; Red; Intro. @@ -128,4 +129,4 @@ Replace (plus (S n) O) with (S n); [Apply le_n_Sn | Ring]. Replace (plus (S n) (S i)) with (S (plus (S n) i)). Apply le_S; Assumption. Apply INR_eq; Rewrite S_INR; Do 2 Rewrite plus_INR; Do 2 Rewrite S_INR; Ring. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Binomial.v b/theories/Reals/Binomial.v index 2654a5f60..c97f98474 100644 --- a/theories/Reals/Binomial.v +++ b/theories/Reals/Binomial.v @@ -11,6 +11,7 @@ Require Rbase. Require Rfunctions. Require PartSum. +Import R_scope. Definition C [n,p:nat] : R := ``(INR (fact n))/((INR (fact p))*(INR (fact (minus n p))))``. diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v index cf962a0e2..c6926ec18 100644 --- a/theories/Reals/Cauchy_prod.v +++ b/theories/Reals/Cauchy_prod.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. +Import R_scope. (**********) Lemma sum_N_predN : (An:nat->R;N:nat) (lt O N) -> (sum_f_R0 An N)==``(sum_f_R0 An (pred N)) + (An N)``. @@ -342,4 +343,4 @@ Simpl; Symmetry; Apply S_pred with O; Assumption. Inversion H. Left; Reflexivity. Right; Apply lt_le_trans with (1); [Apply lt_n_Sn | Exact H1]. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v index 9a4e04283..e366adb38 100644 --- a/theories/Reals/Cos_plus.v +++ b/theories/Reals/Cos_plus.v @@ -14,6 +14,8 @@ Require SeqSeries. Require Rtrigo_def. Require Cos_rel. Require Max. +Import nat_scope. +Import R_scope. Definition Majxy [x,y:R] : nat->R := [n:nat](Rdiv (pow (Rmax R1 (Rmax (Rabsolu x) (Rabsolu y))) (mult (4) (S n))) (INR (fact n))). diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index f1275c3db..fb41d9927 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. +Import R_scope. Definition A1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``(pow (-1) k)/(INR (fact (mult (S (S O)) k)))*(pow x (mult (S (S O)) k))`` N). diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 94307dc85..791954d06 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -10,6 +10,7 @@ Require RIneq. Require Omega. +Import R_scope. Lemma Rlt_R0_R2 : ``0<2``. Replace ``2`` with (INR (2)); [Apply lt_INR_0; Apply lt_O_Sn | Reflexivity]. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index 61df2b49f..8a16bfdf1 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -17,6 +17,7 @@ Require PSeries_reg. Require Div2. Require Even. Require Max. +Import R_scope. Definition E1 [x:R] : nat->R := [N:nat](sum_f_R0 [k:nat]``/(INR (fact k))*(pow x k)`` N). diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index b271d408b..520ccc788 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. Require Rtopology. +Import R_scope. (* The Mean Value Theorem *) Theorem MVT : (f,g:R->R;a,b:R;pr1:(c:R)``a<c<b``->(derivable_pt f c);pr2:(c:R)``a<c<b``->(derivable_pt g c)) ``a<b`` -> ((c:R)``a<=c<=b``->(continuity_pt f c)) -> ((c:R)``a<=c<=b``->(continuity_pt g c)) -> (EXT c : R | (EXT P : ``a<c<b`` | ``((g b)-(g a))*(derive_pt f c (pr1 c P))==((f b)-(f a))*(derive_pt g c (pr2 c P))``)). diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index 4010f1d44..b0d0d5949 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -13,6 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo. Require Ranalysis. +Import R_scope. (*******************************************) (* Newton's Integral *) diff --git a/theories/Reals/PSeries_reg.v b/theories/Reals/PSeries_reg.v index 974160de1..92549a55e 100644 --- a/theories/Reals/PSeries_reg.v +++ b/theories/Reals/PSeries_reg.v @@ -14,6 +14,7 @@ Require SeqSeries. Require Ranalysis1. Require Max. Require Even. +Import R_scope. Definition Boule [x:R;r:posreal] : R -> Prop := [y:R]``(Rabsolu (y-x))<r``. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 737520552..0b3da1ea7 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -13,6 +13,7 @@ Require Rfunctions. Require Rseries. Require Rcomplete. Require Max. +Import R_scope. Lemma tech1 : (An:nat->R;N:nat) ((n:nat)``(le n N)``->``0<(An n)``) -> ``0 < (sum_f_R0 An N)``. Intros; Induction N. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 361bf9b22..c07302f3f 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -16,6 +16,9 @@ Require Export Raxioms. Require Export ZArithRing. Require Omega. Require Export Field. +Import nat_scope. +Import Z_scope. +Import R_scope. (***************************************************************************) (** Instantiating Ring tactic on reals *) @@ -397,6 +400,8 @@ Qed. (***********) Definition Rsqr:R->R:=[r:R]``r*r``. +Notation "x ²" := (Rsqr x) (at level 2,left associativity) + V8only (at level 20, left associativity). (***********) Lemma Rsqr_O:(Rsqr ``0``)==``0``. diff --git a/theories/Reals/RList.v b/theories/Reals/RList.v index 82c920621..ce022d7c1 100644 --- a/theories/Reals/RList.v +++ b/theories/Reals/RList.v @@ -10,6 +10,7 @@ Require Rbase. Require Rfunctions. +Import R_scope. Inductive Rlist : Type := | nil : Rlist diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index 933149427..9e8b81d3e 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -10,6 +10,7 @@ Require Rbase. Require Rbasic_fun. +Import R_scope. (****************************************************) (* Rsqr : some results *) diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 35890cde8..01f0662a9 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -11,6 +11,7 @@ Require Rbase. Require Rfunctions. Require Rsqrt_def. +Import R_scope. (* Here is a continuous extension of Rsqrt on R *) Definition sqrt : R->R := [x:R](Cases (case_Rabsolu x) of diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index 2575b8508..40d484dcd 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -28,6 +28,7 @@ Require Export RList. Require Export Sqrt_reg. Require Export Ranalysis4. Require Export Rpower. +Import R_scope. Axiom AppVar : R. @@ -473,4 +474,4 @@ Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (continuity_pt aux ?2); | [|-(eqT ? (derive_pt ?1 ?2 ?3) ?4)] -> Let trm = Eval Cbv Beta in (?1 AppVar) In Let aux = (RewTerm trm) In -IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt.
\ No newline at end of file +IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 0c1515d9f..b4c2c8cce 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require Export Rlimit. Require Export Rderiv. +Import R_scope. (****************************************************) (** Basic operations on functions *) @@ -1020,4 +1021,4 @@ Unfold Rdiv; Rewrite <- Ropp_mul1; Apply Rmult_lt_pos. Apply Rlt_anti_compatibility with l. Unfold Rminus; Rewrite Rplus_Ropp_r; Rewrite Rplus_Or; Assumption. Apply Rlt_Rinv; Sup0. -Qed.
\ No newline at end of file +Qed. diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 83f9409cd..e2bc87ffe 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -11,6 +11,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. +Import R_scope. (**********) Lemma formule : (x,h,l1,l2:R;f1,f2:R->R) ``h<>0`` -> ``(f2 x)<>0`` -> ``(f2 (x+h))<>0`` -> ``((f1 (x+h))/(f2 (x+h))-(f1 x)/(f2 x))/h-(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))`` == ``/(f2 (x+h))*(((f1 (x+h))-(f1 x))/h-l1) + l1/((f2 x)*(f2 (x+h)))*((f2 x)-(f2 (x+h))) - (f1 x)/((f2 x)*(f2 (x+h)))*(((f2 (x+h))-(f2 x))/h-l2) + (l2*(f1 x))/((Rsqr (f2 x))*(f2 (x+h)))*((f2 (x+h))-(f2 x))``. diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v index 9cc34059b..0ccda909d 100644 --- a/theories/Reals/Ranalysis3.v +++ b/theories/Reals/Ranalysis3.v @@ -12,7 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. Require Ranalysis2. - +Import R_scope. (* Division *) Theorem derivable_pt_lim_div : (f1,f2:R->R;x,l1,l2:R) (derivable_pt_lim f1 x l1) -> (derivable_pt_lim f2 x l2) -> ~``(f2 x)==0``-> (derivable_pt_lim (div_fct f1 f2) x ``(l1*(f2 x)-l2*(f1 x))/(Rsqr (f2 x))``). diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 5c81a076e..5dc3991e2 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -15,6 +15,7 @@ Require Rtrigo. Require Ranalysis1. Require Ranalysis3. Require Exp_prop. +Import R_scope. (**********) Lemma derivable_pt_inv : (f:R->R;x:R) ``(f x)<>0`` -> (derivable_pt f x) -> (derivable_pt (inv_fct f) x). diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index cda4273a5..455511633 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -15,6 +15,7 @@ Require Export ZArith_base. Require Export Rsyntax. Require Export TypeSyntax. +Import R_scope. (*********************************************************) (* Field axioms *) @@ -111,6 +112,8 @@ Fixpoint INR [n:nat]:R:=(Cases n of |(S O) => ``1`` |(S n) => ``(INR n)+1`` end). +Arguments Scope INR [nat_scope]. + (**********************************************************) (** Injection from [Z] to [R] *) @@ -122,6 +125,7 @@ Definition IZR:Z->R:=[z:Z](Cases z of |(POS n) => (INR (convert n)) |(NEG n) => ``-(INR (convert n))`` end). +Arguments Scope IZR [Z_scope]. (**********************************************************) (** [R] Archimedian *) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 0fb879095..5de4bd1fd 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -16,6 +16,7 @@ Require Rbase. Require R_Ifp. Require Fourier. +Import R_scope. (*******************************) (** Rmin *) diff --git a/theories/Reals/Rcomplete.v b/theories/Reals/Rcomplete.v index 0fff7c42a..151f2b263 100644 --- a/theories/Reals/Rcomplete.v +++ b/theories/Reals/Rcomplete.v @@ -13,6 +13,7 @@ Require Rfunctions. Require Rseries. Require SeqProp. Require Max. +Import R_scope. (****************************************************) (* R is complete : *) diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index 234fb3760..b5c0c6b1c 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -20,6 +20,7 @@ Require Fourier. Require Classical_Prop. Require Classical_Pred_Type. Require Omega. +Import R_scope. (*********) Definition D_x:(R->Prop)->R->R->Prop:=[D:R->Prop][y:R][x:R] diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 64d5a613b..e4cfa330a 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -25,7 +25,7 @@ Require Export SplitRmult. Require Export ArithProp. Require Omega. Require Zpower. - +Import R_scope. (*******************************) (** Factorial *) diff --git a/theories/Reals/Rgeom.v b/theories/Reals/Rgeom.v index 9588df9d3..b36b9ad35 100644 --- a/theories/Reals/Rgeom.v +++ b/theories/Reals/Rgeom.v @@ -13,7 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo. Require R_sqrt. - +Import R_scope. Definition dist_euc [x0,y0,x1,y1:R] : R := ``(sqrt ((Rsqr (x0-x1))+(Rsqr (y0-y1))))``. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index aa43801a9..b10b1407e 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -16,6 +16,7 @@ Require RiemannInt_SF. Require Classical_Prop. Require Classical_Pred_Type. Require Max. +Import R_scope. Implicit Arguments On. @@ -27,7 +28,7 @@ Definition Riemann_integrable [f:R->R;a,b:R] : Type := (eps:posreal) (SigT ? [ph Definition phi_sequence [un:nat->posreal;f:R->R;a,b:R;pr:(Riemann_integrable f a b)] := [n:nat](projT1 ? ? (pr (un n))). -Lemma phi_sequence_prop : (un:nat->posreal;f:R->R;a,b:R;pr:(Riemann_integrable f a b);N:nat) (SigT ? [psi:(StepFun a b)]((t:R)``(Rmin a b)<=t<=(Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence un f a b pr N) t)))<=(psi t)``)/\``(Rabsolu (RiemannInt_SF psi))<(un N)``). +Lemma phi_sequence_prop : (un:nat->posreal;f:R->R;a,b:R;pr:(Riemann_integrable f a b);N:nat) (SigT ? [psi:(StepFun a b)]((t:R)``(Rmin a b)<=t<=(Rmax a b)``->``(Rabsolu ((f t)-[(phi_sequence un pr N t)]))<=(psi t)``)/\``(Rabsolu (RiemannInt_SF psi))<(un N)``). Intros; Apply (projT2 ? ? (pr (un N))). Qed. @@ -94,17 +95,17 @@ Qed. Lemma RiemannInt_P4 : (f:R->R;a,b,l:R;pr1,pr2:(Riemann_integrable f a b);un,vn:nat->posreal) (Un_cv un R0) -> (Un_cv vn R0) -> (Un_cv [N:nat](RiemannInt_SF (phi_sequence un pr1 N)) l) -> (Un_cv [N:nat](RiemannInt_SF (phi_sequence vn pr2 N)) l). Unfold Un_cv; Unfold R_dist; Intros; Assert H3 : ``0<eps/3``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. -Elim (H ? H3); Clear H; Intros N0 H; Elim (H0 ? H3); Clear H0; Intros N1 H0; Elim (H1 ? H3); Clear H1; Intros N2 H1; Pose N := (max (max N0 N1) N2); Exists N; Intros; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF (phi_sequence vn f a b pr2 n))-(RiemannInt_SF (phi_sequence un f a b pr1 n))))+(Rabsolu ((RiemannInt_SF (phi_sequence un f a b pr1 n))-l))``. -Replace ``(RiemannInt_SF (phi_sequence vn f a b pr2 n))-l`` with ``((RiemannInt_SF (phi_sequence vn f a b pr2 n))-(RiemannInt_SF (phi_sequence un f a b pr1 n)))+((RiemannInt_SF (phi_sequence un f a b pr1 n))-l)``; [Apply Rabsolu_triang | Ring]. +Elim (H ? H3); Clear H; Intros N0 H; Elim (H0 ? H3); Clear H0; Intros N1 H0; Elim (H1 ? H3); Clear H1; Intros N2 H1; Pose N := (max (max N0 N1) N2); Exists N; Intros; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence vn pr2 n)])-(RiemannInt_SF [(phi_sequence un pr1 n)])))+(Rabsolu ((RiemannInt_SF [(phi_sequence un pr1 n)])-l))``. +Replace ``(RiemannInt_SF [(phi_sequence vn pr2 n)])-l`` with ``((RiemannInt_SF [(phi_sequence vn pr2 n)])-(RiemannInt_SF [(phi_sequence un pr1 n)]))+((RiemannInt_SF [(phi_sequence un pr1 n)])-l)``; [Apply Rabsolu_triang | Ring]. Replace ``eps`` with ``2*eps/3+eps/3``. Apply Rplus_lt. -Elim (phi_sequence_prop vn pr2 n); Intros psi_vn H5; Elim (phi_sequence_prop un pr1 n); Intros psi_un H6; Replace ``(RiemannInt_SF (phi_sequence vn f a b pr2 n))-(RiemannInt_SF (phi_sequence un f a b pr1 n))`` with ``(RiemannInt_SF (phi_sequence vn f a b pr2 n))+(-1)*(RiemannInt_SF (phi_sequence un f a b pr1 n))``; [Idtac | Ring]; Rewrite <- StepFun_P30. +Elim (phi_sequence_prop vn pr2 n); Intros psi_vn H5; Elim (phi_sequence_prop un pr1 n); Intros psi_un H6; Replace ``(RiemannInt_SF [(phi_sequence vn pr2 n)])-(RiemannInt_SF [(phi_sequence un pr1 n)])`` with ``(RiemannInt_SF [(phi_sequence vn pr2 n)])+(-1)*(RiemannInt_SF [(phi_sequence un pr1 n)])``; [Idtac | Ring]; Rewrite <- StepFun_P30. Case (total_order_Rle a b); Intro. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 ``-1`` (phi_sequence vn pr2 n) (phi_sequence un pr1 n)))))). Apply StepFun_P34; Assumption. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 R1 psi_un psi_vn))). -Apply StepFun_P37; Try Assumption; Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ((phi_sequence vn f a b pr2 n x)-(f x)))+(Rabsolu ((f x)-(phi_sequence un f a b pr1 n x)))``. -Replace ``(phi_sequence vn f a b pr2 n x)+-1*(phi_sequence un f a b pr1 n x)`` with ``((phi_sequence vn f a b pr2 n x)-(f x))+((f x)-(phi_sequence un f a b pr1 n x))``; [Apply Rabsolu_triang | Ring]. +Apply StepFun_P37; Try Assumption; Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ([(phi_sequence vn pr2 n x)]-(f x)))+(Rabsolu ((f x)-[(phi_sequence un pr1 n x)]))``. +Replace ``[(phi_sequence vn pr2 n x)]+-1*[(phi_sequence un pr1 n x)]`` with ``([(phi_sequence vn pr2 n x)]-(f x))+((f x)-[(phi_sequence un pr1 n x)])``; [Apply Rabsolu_triang | Ring]. Assert H10 : (Rmin a b)==a. Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n0; Assumption]. Assert H11 : (Rmax a b)==b. @@ -130,8 +131,8 @@ Apply StepFun_P34; Try Auto with real. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P6 (pre (mkStepFun (StepFun_P28 R1 psi_vn psi_un)))))). Apply StepFun_P37. Auto with real. -Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ((phi_sequence vn f a b pr2 n x)-(f x)))+(Rabsolu ((f x)-(phi_sequence un f a b pr1 n x)))``. -Replace ``(phi_sequence vn f a b pr2 n x)+-1*(phi_sequence un f a b pr1 n x)`` with ``((phi_sequence vn f a b pr2 n x)-(f x))+((f x)-(phi_sequence un f a b pr1 n x))``; [Apply Rabsolu_triang | Ring]. +Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ([(phi_sequence vn pr2 n x)]-(f x)))+(Rabsolu ((f x)-[(phi_sequence un pr1 n x)]))``. +Replace ``[(phi_sequence vn pr2 n x)]+-1*[(phi_sequence un pr1 n x)]`` with ``([(phi_sequence vn pr2 n x)]-(f x))+((f x)-[(phi_sequence un pr1 n x)])``; [Apply Rabsolu_triang | Ring]. Assert H10 : (Rmin a b)==b. Unfold Rmin; Case (total_order_Rle a b); Intro; [Elim n0; Assumption | Reflexivity]. Assert H11 : (Rmax a b)==a. @@ -397,24 +398,24 @@ Qed. Lemma RiemannInt_P8 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable f b a)) ``(RiemannInt pr1)==-(RiemannInt pr2)``. Intros; EApply UL_sequence. Unfold RiemannInt; Case (RiemannInt_exists pr1 5!RinvN RinvN_cv); Intros; Apply u. -Unfold RiemannInt; Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Intros; Cut (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f a b pr1 n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). -Cut (EXT psi2:nat->(StepFun b a) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f b a pr2 n) t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). +Unfold RiemannInt; Case (RiemannInt_exists pr2 5!RinvN RinvN_cv); Intros; Cut (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr1 n)] t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). +Cut (EXT psi2:nat->(StepFun b a) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr2 n)] t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). Intros; Elim H; Clear H; Intros psi2 H; Elim H0; Clear H0; Intros psi1 H0; Assert H1 := RinvN_cv; Unfold Un_cv; Intros; Assert H3 : ``0<eps/3``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. Unfold Un_cv in H1; Elim (H1 ? H3); Clear H1; Intros N0 H1; Unfold R_dist in H1; Simpl in H1; Assert H4 : (n:nat)(ge n N0)->``(RinvN n)<eps/3``. Intros; Assert H5 := (H1 ? H4); Replace (pos (RinvN n)) with ``(Rabsolu (/((INR n)+1)-0))``; [Assumption | Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Apply Rabsolu_right; Left; Apply (cond_pos (RinvN n))]. -Clear H1; Unfold Un_cv in u; Elim (u ? H3); Clear u; Intros N1 H1; Exists (max N0 N1); Intros; Unfold R_dist; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b a pr2 n))))+(Rabsolu ((RiemannInt_SF (phi_sequence RinvN f b a pr2 n))-x))``. -Rewrite <- (Rabsolu_Ropp ``(RiemannInt_SF (phi_sequence RinvN f b a pr2 n))-x``); Replace ``(RiemannInt_SF (phi_sequence RinvN f a b pr1 n))- -x`` with ``((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b a pr2 n)))+ -((RiemannInt_SF (phi_sequence RinvN f b a pr2 n))-x)``; [Apply Rabsolu_triang | Ring]. +Clear H1; Unfold Un_cv in u; Elim (u ? H3); Clear u; Intros N1 H1; Exists (max N0 N1); Intros; Unfold R_dist; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)])))+(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x))``. +Rewrite <- (Rabsolu_Ropp ``(RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x``); Replace ``(RiemannInt_SF [(phi_sequence RinvN pr1 n)])- -x`` with ``((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))+ -((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x)``; [Apply Rabsolu_triang | Ring]. Replace eps with ``2*eps/3+eps/3``. Apply Rplus_lt. -Rewrite (StepFun_P39 (phi_sequence RinvN pr2 n)); Replace ``(RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+ -(RiemannInt_SF (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN f b a pr2 n)))))`` with ``(RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(-1)*(RiemannInt_SF (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN f b a pr2 n)))))``; [Idtac | Ring]; Rewrite <- StepFun_P30. +Rewrite (StepFun_P39 (phi_sequence RinvN pr2 n)); Replace ``(RiemannInt_SF [(phi_sequence RinvN pr1 n)])+ -(RiemannInt_SF (mkStepFun (StepFun_P6 (pre [(phi_sequence RinvN pr2 n)]))))`` with ``(RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(-1)*(RiemannInt_SF (mkStepFun (StepFun_P6 (pre [(phi_sequence RinvN pr2 n)]))))``; [Idtac | Ring]; Rewrite <- StepFun_P30. Case (total_order_Rle a b); Intro. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P32 (mkStepFun (StepFun_P28 ``-1`` (phi_sequence RinvN pr1 n) (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN pr2 n))))))))). Apply StepFun_P34; Assumption. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 ``1`` (psi1 n) (mkStepFun (StepFun_P6 (pre (psi2 n))))))). Apply StepFun_P37; Try Assumption. -Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu (((phi_sequence RinvN f a b pr1 n) x0)-(f x0)))+(Rabsolu ((f x0)-((phi_sequence RinvN f b a pr2 n) x0)))``. -Replace ``((phi_sequence RinvN f a b pr1 n) x0)+ -1*((phi_sequence RinvN f b a pr2 n) x0)`` with ``(((phi_sequence RinvN f a b pr1 n) x0)-(f x0))+((f x0)-((phi_sequence RinvN f b a pr2 n) x0))``; [Apply Rabsolu_triang | Ring]. +Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu (([(phi_sequence RinvN pr1 n)] x0)-(f x0)))+(Rabsolu ((f x0)-([(phi_sequence RinvN pr2 n)] x0)))``. +Replace ``([(phi_sequence RinvN pr1 n)] x0)+ -1*([(phi_sequence RinvN pr2 n)] x0)`` with ``(([(phi_sequence RinvN pr1 n)] x0)-(f x0))+((f x0)-([(phi_sequence RinvN pr2 n)] x0))``; [Apply Rabsolu_triang | Ring]. Assert H7 : (Rmin a b)==a. Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n0; Assumption]. Assert H8 : (Rmax a b)==b. @@ -433,8 +434,8 @@ Rewrite StepFun_P39; Rewrite Rabsolu_Ropp; Apply Rle_lt_trans with (RiemannInt_S Apply StepFun_P34; Assumption. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 ``1`` (mkStepFun (StepFun_P6 (pre (psi1 n)))) (psi2 n)))). Apply StepFun_P37; Try Assumption. -Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu (((phi_sequence RinvN f a b pr1 n) x0)-(f x0)))+(Rabsolu ((f x0)-((phi_sequence RinvN f b a pr2 n) x0)))``. -Replace ``((phi_sequence RinvN f a b pr1 n) x0)+ -1*((phi_sequence RinvN f b a pr2 n) x0)`` with ``(((phi_sequence RinvN f a b pr1 n) x0)-(f x0))+((f x0)-((phi_sequence RinvN f b a pr2 n) x0))``; [Apply Rabsolu_triang | Ring]. +Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu (([(phi_sequence RinvN pr1 n)] x0)-(f x0)))+(Rabsolu ((f x0)-([(phi_sequence RinvN pr2 n)] x0)))``. +Replace ``([(phi_sequence RinvN pr1 n)] x0)+ -1*([(phi_sequence RinvN pr2 n)] x0)`` with ``(([(phi_sequence RinvN pr1 n)] x0)-(f x0))+((f x0)-([(phi_sequence RinvN pr2 n)] x0))``; [Apply Rabsolu_triang | Ring]. Assert H7 : (Rmin a b)==b. Unfold Rmin; Case (total_order_Rle a b); Intro; [Elim n0; Assumption | Reflexivity]. Assert H8 : (Rmax a b)==a. @@ -608,19 +609,19 @@ Intros; Replace (pos (RinvN n)) with ``(Rabsolu ((RinvN n)-0))``; [Unfold RinvN; Clear H4; Assert H4 := H7; Clear H7; Assert H7 : (n:nat) (ge n N3)->``(RinvN n)< eps/(5*(Rabsolu l))``. Intros; Replace (pos (RinvN n)) with ``(Rabsolu ((RinvN n)-0))``; [Unfold RinvN; Apply H5; Assumption | Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Apply Rabsolu_right; Left; Apply (cond_pos (RinvN n))]. Clear H5; Assert H5 := H7; Clear H7; Exists N; Intros; Unfold R_dist. -Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF (phi_sequence RinvN ? ? ? pr3 n))-((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))+l*(RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n)))))+(Rabsolu ((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))-x0))+(Rabsolu l)*(Rabsolu ((RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n))-x))``. -Apply Rle_trans with ``(Rabsolu ((RiemannInt_SF (phi_sequence RinvN ? ? ? pr3 n))-((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))+l*(RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n)))))+(Rabsolu (((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))-x0)+l*((RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n))-x)))``. -Replace ``(RiemannInt_SF (phi_sequence RinvN ? ? ? pr3 n))-(x0+l*x)`` with ``(((RiemannInt_SF (phi_sequence RinvN ? ? ? pr3 n))-((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))+l*(RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n)))))+(((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))-x0)+l*((RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n))-x))``; [Apply Rabsolu_triang | Ring]. -Rewrite Rplus_assoc; Apply Rle_compatibility; Rewrite <- Rabsolu_mult; Replace ``(RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))-x0+l*((RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n))-x)`` with ``((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))-x0)+(l*((RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n))-x))``; [Apply Rabsolu_triang | Ring]. +Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+l*(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))))+(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x0))+(Rabsolu l)*(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x))``. +Apply Rle_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+l*(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))))+(Rabsolu (((RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x0)+l*((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x)))``. +Replace ``(RiemannInt_SF [(phi_sequence RinvN pr3 n)])-(x0+l*x)`` with ``(((RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+l*(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))))+(((RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x0)+l*((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x))``; [Apply Rabsolu_triang | Ring]. +Rewrite Rplus_assoc; Apply Rle_compatibility; Rewrite <- Rabsolu_mult; Replace ``(RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x0+l*((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x)`` with ``((RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x0)+(l*((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x))``; [Apply Rabsolu_triang | Ring]. Replace eps with ``3*eps/5+eps/5+eps/5``. Repeat Apply Rplus_lt. -Assert H7 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN ? ? ? pr1 n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). +Assert H7 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr1 n)] t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n0)). -Assert H8 : (EXT psi2:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((g t)-((phi_sequence RinvN ? ? ? pr2 n) t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). +Assert H8 : (EXT psi2:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((g t)-([(phi_sequence RinvN pr2 n)] t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr2 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr2 n0)). -Assert H9 : (EXT psi3:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu (((f t)+l*(g t))-((phi_sequence RinvN ? ? ? pr3 n) t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``). +Assert H9 : (EXT psi3:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu (((f t)+l*(g t))-([(phi_sequence RinvN pr3 n)] t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr3 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr3 n0)). -Elim H7; Clear H7; Intros psi1 H7; Elim H8; Clear H8; Intros psi2 H8; Elim H9; Clear H9; Intros psi3 H9; Replace ``(RiemannInt_SF (phi_sequence RinvN ? ? ? pr3 n))-((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))+l*(RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n)))`` with ``(RiemannInt_SF (phi_sequence RinvN ? ? ? pr3 n))+(-1)*((RiemannInt_SF (phi_sequence RinvN ? ? ? pr1 n))+l*(RiemannInt_SF (phi_sequence RinvN ? ? ? pr2 n)))``; [Idtac | Ring]; Do 2 Rewrite <- StepFun_P30; Assert H10 : (Rmin a b)==a. +Elim H7; Clear H7; Intros psi1 H7; Elim H8; Clear H8; Intros psi2 H8; Elim H9; Clear H9; Intros psi3 H9; Replace ``(RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+l*(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))`` with ``(RiemannInt_SF [(phi_sequence RinvN pr3 n)])+(-1)*((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+l*(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))``; [Idtac | Ring]; Do 2 Rewrite <- StepFun_P30; Assert H10 : (Rmin a b)==a. Unfold Rmin; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n0; Assumption]. Assert H11 : (Rmax a b)==b. Unfold Rmax; Case (total_order_Rle a b); Intro; [Reflexivity | Elim n0; Assumption]. @@ -629,13 +630,13 @@ Apply StepFun_P34; Assumption. Apply Rle_lt_trans with (RiemannInt_SF (mkStepFun (StepFun_P28 R1 (psi3 n) (mkStepFun (StepFun_P28 (Rabsolu l) (psi1 n) (psi2 n)))))). Apply StepFun_P37; Try Assumption. Intros; Simpl; Rewrite Rmult_1l. -Apply Rle_trans with ``(Rabsolu (((phi_sequence RinvN ? ? ? pr3 n) x1)-((f x1)+l*(g x1))))+(Rabsolu (((f x1)+l*(g x1))+ -1*(((phi_sequence RinvN ? ? ? pr1 n) x1)+l*((phi_sequence RinvN ? ? ? pr2 n) x1))))``. -Replace ``((phi_sequence RinvN ? ? ? pr3 n) x1)+ -1*(((phi_sequence RinvN ? ? ? pr1 n) x1)+l*((phi_sequence RinvN ? ? ? pr2 n) x1))`` with ``(((phi_sequence RinvN ? ? ? pr3 n) x1)-((f x1)+l*(g x1)))+(((f x1)+l*(g x1))+ -1*(((phi_sequence RinvN ? ? ? pr1 n) x1)+l*((phi_sequence RinvN ? ? ? pr2 n) x1)))``; [Apply Rabsolu_triang | Ring]. +Apply Rle_trans with ``(Rabsolu (([(phi_sequence RinvN pr3 n)] x1)-((f x1)+l*(g x1))))+(Rabsolu (((f x1)+l*(g x1))+ -1*(([(phi_sequence RinvN pr1 n)] x1)+l*([(phi_sequence RinvN pr2 n)] x1))))``. +Replace ``([(phi_sequence RinvN pr3 n)] x1)+ -1*(([(phi_sequence RinvN pr1 n)] x1)+l*([(phi_sequence RinvN pr2 n)] x1))`` with ``(([(phi_sequence RinvN pr3 n)] x1)-((f x1)+l*(g x1)))+(((f x1)+l*(g x1))+ -1*(([(phi_sequence RinvN pr1 n)] x1)+l*([(phi_sequence RinvN pr2 n)] x1)))``; [Apply Rabsolu_triang | Ring]. Rewrite Rplus_assoc; Apply Rplus_le. Elim (H9 n); Intros; Rewrite <- Rabsolu_Ropp; Rewrite Ropp_distr2; Apply H13. Elim H12; Intros; Split; Left; Assumption. -Apply Rle_trans with ``(Rabsolu ((f x1)-((phi_sequence RinvN ? ? ? pr1 n) x1)))+(Rabsolu l)*(Rabsolu ((g x1)-((phi_sequence RinvN ? ? ? pr2 n) x1)))``. -Rewrite <- Rabsolu_mult; Replace ``((f x1)+(l*(g x1)+ -1*(((phi_sequence RinvN ? ? ? pr1 n) x1)+l*((phi_sequence RinvN ? ? ? pr2 n) x1))))`` with ``((f x1)-((phi_sequence RinvN ? ? ? pr1 n) x1))+l*((g x1)-((phi_sequence RinvN ? ? ? pr2 n) x1))``; [Apply Rabsolu_triang | Ring]. +Apply Rle_trans with ``(Rabsolu ((f x1)-([(phi_sequence RinvN pr1 n)] x1)))+(Rabsolu l)*(Rabsolu ((g x1)-([(phi_sequence RinvN pr2 n)] x1)))``. +Rewrite <- Rabsolu_mult; Replace ``((f x1)+(l*(g x1)+ -1*(([(phi_sequence RinvN pr1 n)] x1)+l*([(phi_sequence RinvN pr2 n)] x1))))`` with ``((f x1)-([(phi_sequence RinvN pr1 n)] x1))+l*((g x1)-([(phi_sequence RinvN pr2 n)] x1))``; [Apply Rabsolu_triang | Ring]. Apply Rplus_le. Elim (H7 n); Intros; Apply H13. Elim H12; Intros; Split; Left; Assumption. @@ -672,7 +673,7 @@ Qed. Lemma RiemannInt_P15 : (a,b,c:R;pr:(Riemann_integrable (fct_cte c) a b)) ``(RiemannInt pr)==c*(b-a)``. Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!(fct_cte c) 2!a 3!b pr 5!RinvN RinvN_cv); Intros; EApply UL_sequence. Apply u. -Pose phi1 := [N:nat](phi_sequence RinvN 2!(fct_cte c) 3!a 4!b pr N); Change (Un_cv [N:nat](RiemannInt_SF (phi1 N)) ``c*(b-a)``); Pose f := (fct_cte c); Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f a b pr n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). +Pose phi1 := [N:nat](phi_sequence RinvN 2!(fct_cte c) 3!a 4!b pr N); Change (Un_cv [N:nat](RiemannInt_SF (phi1 N)) ``c*(b-a)``); Pose f := (fct_cte c); Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr n)] t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr n)). Elim H1; Clear H1; Intros psi1 H1; Pose phi2 := [n:nat](mkStepFun (StepFun_P4 a b c)); Pose psi2 := [n:nat](mkStepFun (StepFun_P4 a b R0)); Apply RiemannInt_P11 with f RinvN phi2 psi2 psi1; Try Assumption. Apply RinvN_cv. @@ -1113,27 +1114,27 @@ Intros f a b c pr1 pr2 pr3 Hyp1 Hyp2; Unfold RiemannInt; Case (RiemannInt_exists Apply u. Unfold Un_cv; Intros; Assert H0 : ``0<eps/3``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. -Elim (u1 ? H0); Clear u1; Intros N1 H1; Elim (u0 ? H0); Clear u0; Intros N2 H2; Cut (Un_cv [n:nat]``(RiemannInt_SF (phi_sequence RinvN f a c pr3 n))-((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b c pr2 n)))`` R0). -Intro; Elim (H3 ? H0); Clear H3; Intros N3 H3; Pose N0 := (max (max N1 N2) N3); Exists N0; Intros; Unfold R_dist; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF (phi_sequence RinvN f a c pr3 n))-((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b c pr2 n)))))+(Rabsolu (((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b c pr2 n)))-(x1+x0)))``. -Replace ``(RiemannInt_SF (phi_sequence RinvN f a c pr3 n))-(x1+x0)`` with ``((RiemannInt_SF (phi_sequence RinvN f a c pr3 n))-((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b c pr2 n))))+(((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b c pr2 n)))-(x1+x0))``; [Apply Rabsolu_triang | Ring]. +Elim (u1 ? H0); Clear u1; Intros N1 H1; Elim (u0 ? H0); Clear u0; Intros N2 H2; Cut (Un_cv [n:nat]``(RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))`` R0). +Intro; Elim (H3 ? H0); Clear H3; Intros N3 H3; Pose N0 := (max (max N1 N2) N3); Exists N0; Intros; Unfold R_dist; Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))))+(Rabsolu (((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))-(x1+x0)))``. +Replace ``(RiemannInt_SF [(phi_sequence RinvN pr3 n)])-(x1+x0)`` with ``((RiemannInt_SF [(phi_sequence RinvN pr3 n)])-((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)])))+(((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))-(x1+x0))``; [Apply Rabsolu_triang | Ring]. Replace eps with ``eps/3+eps/3+eps/3``. Rewrite Rplus_assoc; Apply Rplus_lt. Unfold R_dist in H3; Cut (ge n N3). Intro; Assert H6 := (H3 ? H5); Unfold Rminus in H6; Rewrite Ropp_O in H6; Rewrite Rplus_Or in H6; Apply H6. Unfold ge; Apply le_trans with N0; [Unfold N0; Apply le_max_r | Assumption]. -Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))-x1))+(Rabsolu ((RiemannInt_SF (phi_sequence RinvN f b c pr2 n))-x0))``. -Replace ``((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))+(RiemannInt_SF (phi_sequence RinvN f b c pr2 n)))-(x1+x0)`` with ``((RiemannInt_SF (phi_sequence RinvN f a b pr1 n))-x1)+((RiemannInt_SF (phi_sequence RinvN f b c pr2 n))-x0)``; [Apply Rabsolu_triang | Ring]. +Apply Rle_lt_trans with ``(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x1))+(Rabsolu ((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x0))``. +Replace ``((RiemannInt_SF [(phi_sequence RinvN pr1 n)])+(RiemannInt_SF [(phi_sequence RinvN pr2 n)]))-(x1+x0)`` with ``((RiemannInt_SF [(phi_sequence RinvN pr1 n)])-x1)+((RiemannInt_SF [(phi_sequence RinvN pr2 n)])-x0)``; [Apply Rabsolu_triang | Ring]. Apply Rplus_lt. Unfold R_dist in H1; Apply H1. Unfold ge; Apply le_trans with N0; [Apply le_trans with (max N1 N2); [Apply le_max_l | Unfold N0; Apply le_max_l] | Assumption]. Unfold R_dist in H2; Apply H2. Unfold ge; Apply le_trans with N0; [Apply le_trans with (max N1 N2); [Apply le_max_r | Unfold N0; Apply le_max_l] | Assumption]. Apply r_Rmult_mult with ``3``; [Unfold Rdiv; Repeat Rewrite Rmult_Rplus_distr; Do 2 Rewrite (Rmult_sym ``3``); Repeat Rewrite Rmult_assoc; Rewrite <- Rinv_l_sym; [Ring | DiscrR] | DiscrR]. -Clear x u x0 x1 eps H H0 N1 H1 N2 H2; Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-((phi_sequence RinvN f a b pr1 n) t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). +Clear x u x0 x1 eps H H0 N1 H1 N2 H2; Assert H1 : (EXT psi1:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr1 n)] t)))<= (psi1 n t)``)/\``(Rabsolu (RiemannInt_SF (psi1 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr1 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr1 n)). -Assert H2 : (EXT psi2:nat->(StepFun b c) | (n:nat) ((t:R)``(Rmin b c) <= t``/\``t <= (Rmax b c)``->``(Rabsolu ((f t)-((phi_sequence RinvN f b c pr2 n) t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). +Assert H2 : (EXT psi2:nat->(StepFun b c) | (n:nat) ((t:R)``(Rmin b c) <= t``/\``t <= (Rmax b c)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr2 n)] t)))<= (psi2 n t)``)/\``(Rabsolu (RiemannInt_SF (psi2 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr2 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr2 n)). -Assert H3 : (EXT psi3:nat->(StepFun a c) | (n:nat) ((t:R)``(Rmin a c) <= t``/\``t <= (Rmax a c)``->``(Rabsolu ((f t)-((phi_sequence RinvN f a c pr3 n) t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``). +Assert H3 : (EXT psi3:nat->(StepFun a c) | (n:nat) ((t:R)``(Rmin a c) <= t``/\``t <= (Rmax a c)``->``(Rabsolu ((f t)-([(phi_sequence RinvN pr3 n)] t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr3 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr3 n)). Elim H1; Clear H1; Intros psi1 H1; Elim H2; Clear H2; Intros psi2 H2; Elim H3; Clear H3; Intros psi3 H3; Assert H := RinvN_cv; Unfold Un_cv; Intros; Assert H4 : ``0<eps/3``. Unfold Rdiv; Apply Rmult_lt_pos; [Assumption | Apply Rlt_Rinv; Sup0]. @@ -1395,7 +1396,7 @@ Intros; Elim h; Intro. Elim H; Clear H; Intros; Elim H; Intro. Elim H1; Intro. Apply RiemannInt_P27; Split; Assumption. -Pose f_b := [x:R]``(f b)*(x-b)+(RiemannInt (FTC_P1 h C0 b h (FTC_P2 b)))``; Rewrite H3. +Pose f_b := [x:R]``(f b)*(x-b)+(RiemannInt [(FTC_P1 h C0 h (FTC_P2 b))])``; Rewrite H3. Assert H4 : (derivable_pt_lim f_b b (f b)). Unfold f_b; Pattern 2 (f b); Replace (f b) with ``(f b)+0``. Change (derivable_pt_lim (plus_fct (mult_fct (fct_cte (f b)) (minus_fct id (fct_cte b))) (fct_cte (RiemannInt (FTC_P1 h C0 h (FTC_P2 b))))) b ``(f b)+0``). @@ -1434,8 +1435,8 @@ Apply Rle_trans with (Rabsolu h0). Rewrite <- Rabsolu_Ropp; Apply Rle_Rabsolu. Left; Assumption. Unfold del; Apply Rle_trans with (Rmin x1 ``b-a``); Apply Rmin_r. -Replace ``(primitive h (FTC_P1 h C0) (b+h0))-(primitive h (FTC_P1 h C0) b)`` with ``-(RiemannInt H13)``. -Replace (f b) with ``-(RiemannInt (RiemannInt_P14 (b+h0) b (f b)))/h0``. +Replace ``[(primitive h (FTC_P1 h C0) (b+h0))]-[(primitive h (FTC_P1 h C0) b)]`` with ``-(RiemannInt H13)``. +Replace (f b) with ``-[(RiemannInt (RiemannInt_P14 (b+h0) b (f b)))]/h0``. Rewrite <- Rabsolu_Ropp; Unfold Rminus; Unfold Rdiv; Rewrite Ropp_mul1; Rewrite Ropp_distr1; Repeat Rewrite Ropp_Ropp; Replace ``(RiemannInt H13)*/h0+ -(RiemannInt (RiemannInt_P14 (b+h0) b (f b)))*/h0`` with ``((RiemannInt H13)-(RiemannInt (RiemannInt_P14 (b+h0) b (f b))))/h0``. Replace ``(RiemannInt H13)-(RiemannInt (RiemannInt_P14 (b+h0) b (f b)))`` with (RiemannInt (RiemannInt_P10 ``-1`` H13 (RiemannInt_P14 ``b+h0`` b (f b)))). Unfold Rdiv; Rewrite Rabsolu_mult; Apply Rle_lt_trans with ``(RiemannInt (RiemannInt_P16 (RiemannInt_P10 (-1) H13 (RiemannInt_P14 (b+h0) b (f b)))))*(Rabsolu (/h0))``. diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index ab0283899..3681dd393 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis. Require Classical_Prop. +Import R_scope. Implicit Arguments On. diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index ffad4fd8d..c9ad0032d 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -17,6 +17,7 @@ Require Rbase. Require Rfunctions. Require Classical_Prop. Require Fourier. +Import R_scope. (*******************************) (* Calculus *) diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a700d0848..096ab1eaa 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -23,6 +23,7 @@ Require Rsqrt_def. Require R_sqrt. Require MVT. Require Ranalysis4. +Import R_scope. Lemma P_Rmin: (P : R -> Prop) (x, y : R) (P x) -> (P y) -> (P (Rmin x y)). Intros P x y H1 H2; Unfold Rmin; Case (total_order_Rle x y); Intro; Assumption. diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v index 198309911..7089ac26c 100644 --- a/theories/Reals/Rprod.v +++ b/theories/Reals/Rprod.v @@ -14,6 +14,7 @@ Require Rfunctions. Require Rseries. Require PartSum. Require Binomial. +Import R_scope. (* TT Ak; 1<=k<=N *) Fixpoint prod_f_SO [An:nat->R;N:nat] : R := Cases N of diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index 4a5e35fbf..21cf09264 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require Rseries. Require PartSum. +Import R_scope. Set Implicit Arguments. diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 8c63c9eb5..6496c9982 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -13,6 +13,7 @@ Require Rbase. Require Rfunctions. Require SeqSeries. Require Ranalysis1. +Import R_scope. Fixpoint Dichotomy_lb [x,y:R;P:R->bool;N:nat] : R := Cases N of diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v index 44c2638e8..5d2ec7aa7 100644 --- a/theories/Reals/Rsyntax.v +++ b/theories/Reals/Rsyntax.v @@ -12,6 +12,7 @@ Require Export Rdefinitions. Axiom NRplus : R->R. Axiom NRmult : R->R. +V7only[ Grammar rnatural ident := nat_id [ prim:var($id) ] -> [$id] @@ -194,43 +195,51 @@ Syntax constr | Rodd_inside [<<(REXPR <<(Rplus R1 $r)>>)>>] -> [ $r:"r_printer_odd" ] | Reven_inside [<<(REXPR <<(Rmult (Rplus R1 R1) $r)>>)>>] -> [ $r:"r_printer_even" ] . - +]. (* For parsing/printing based on scopes *) Module R_scope. Delimits Scope R_scope with R. -Infix "<=" Rle (at level 5, no associativity) : R_scope. -Infix "<" Rlt (at level 5, no associativity) : R_scope. -Infix ">=" Rge (at level 5, no associativity) : R_scope. -Infix ">" Rgt (at level 5, no associativity) : R_scope. -Infix "+" Rplus (at level 4) : R_scope. -Infix "-" Rminus (at level 4) : R_scope. -Infix "*" Rmult (at level 3) : R_scope. -Infix "/" Rdiv (at level 3) : R_scope. -Distfix 0 "- _" Ropp : R_scope. + +(* Warning: this hides sum and prod and breaks sumor symbolic notation *) +Open Scope R_scope. + +Infix "<=" Rle (at level 5, no associativity) : R_scope + V8only (at level 50, no associativity). +Infix "<" Rlt (at level 5, no associativity) : R_scope + V8only (at level 50, no associativity). +Infix ">=" Rge (at level 5, no associativity) : R_scope + V8only (at level 50, no associativity). +Infix ">" Rgt (at level 5, no associativity) : R_scope + V8only (at level 50, no associativity). +Infix "+" Rplus (at level 4) : R_scope + V8only (at level 40, left associativity). +Infix "-" Rminus (at level 4) : R_scope + V8only (at level 40, left associativity). +Infix "*" Rmult (at level 3) : R_scope + V8only (at level 30, left associativity). +Infix "/" Rdiv (at level 3) : R_scope + V8only (at level 30, left associativity). +Notation "- x" := (Ropp x) (at level 0) : R_scope + V8only (at level 40, left associativity). Notation "x == y == z" := (eqT R x y)/\(eqT R y z) - (at level 5, y at level 4): R_scope. + (at level 5, y at level 4, no associtivity): R_scope + V8only (at level 50, y at level 49, no associativity). Notation "x <= y <= z" := (Rle x y)/\(Rle y z) - (at level 5, y at level 4) : R_scope. + (at level 5, y at level 4) : R_scope + V8only (at level 50, y at level 49, no associativity). Notation "x <= y < z" := (Rle x y)/\(Rlt y z) - (at level 5, y at level 4) : R_scope. + (at level 5, y at level 4) : R_scope + V8only (at level 50, y at level 49, no associativity). Notation "x < y < z" := (Rlt x y)/\(Rlt y z) - (at level 5, y at level 4) : R_scope. + (at level 5, y at level 4) : R_scope + V8only (at level 50, y at level 49, no associativity). Notation "x < y <= z" := (Rlt x y)/\(Rle y z) - (at level 5, y at level 4) : R_scope. -Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope. -Distfix 0 "/ _" Rinv : R_scope. - -(* Warning: this hides sum and prod and breaks sumor symbolic notation *) -Open Scope R_scope. - -(* -Syntax constr - level 0: - Rzero' [ R0 ] -> [ _:"r_printer_R0" ] - | Rone' [ R1 ] -> [ _:"r_printer_R1" ] - | Rconst' [(Rplus R1 $r)] -> [$r:"r_printer_Rplus1"] - | Ropp' [(Ropp $n)] -> [ $n:"r_printer_Ropp" ] -*) + (at level 5, y at level 4) : R_scope + V8only (at level 50, y at level 49, no associativity). +Notation "x <> y" := ~(eqT R x y) (at level 5) : R_scope + V8only (at level 50). +Notation "/ x" := (Rinv x) (at level 0): R_scope + V8only (at level 30, left associativity). End R_scope. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index b019bff37..5a170b5e5 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -14,6 +14,7 @@ Require Ranalysis1. Require RList. Require Classical_Prop. Require Classical_Pred_Type. +Import R_scope. Definition included [D1,D2:R->Prop] : Prop := (x:R)(D1 x)->(D2 x). Definition disc [x:R;delta:posreal] : R->Prop := [y:R]``(Rabsolu (y-x))<delta``. @@ -90,7 +91,8 @@ Qed. Definition eq_Dom [D1,D2:R->Prop] : Prop := (included D1 D2)/\(included D2 D1). -Infix "=_D" eq_Dom (at level 5, no associativity). +Infix "=_D" eq_Dom (at level 5, no associativity) + V8only (at level 50, no associativity). Lemma open_set_P1 : (D:R->Prop) (open_set D) <-> D =_D (interior D). Intro; Split. diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index 8210b35f1..f265b4a77 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -19,6 +19,7 @@ Require Export Cos_plus. Require ZArith_base. Require Zcomplements. Require Classical_Prop. +Import R_scope. (** sin_PI2 is the only remaining axiom **) Axiom sin_PI2 : ``(sin (PI/2))==1``. diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index be9a6f872..d147d68ac 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require SeqSeries. Require Rtrigo_def. +Import R_scope. (*****************************************************************) (* Using series definitions of cos and sin *) diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v index 4e9244dd3..cfa65824b 100644 --- a/theories/Reals/Rtrigo_calc.v +++ b/theories/Reals/Rtrigo_calc.v @@ -13,6 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo. Require R_sqrt. +Import R_scope. Lemma tan_PI : ``(tan PI)==0``. Unfold tan; Rewrite sin_PI; Rewrite cos_PI; Unfold Rdiv; Apply Rmult_Ol. diff --git a/theories/Reals/Rtrigo_def.v b/theories/Reals/Rtrigo_def.v index 554a2059e..cf2ba3dd2 100644 --- a/theories/Reals/Rtrigo_def.v +++ b/theories/Reals/Rtrigo_def.v @@ -13,6 +13,7 @@ Require Rfunctions. Require SeqSeries. Require Rtrigo_fun. Require Max. +Import R_scope. (*****************************) (* Definition of exponential *) diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index ac5c9ed20..aa1c2b9d7 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -14,6 +14,7 @@ Require SeqSeries. Require Rtrigo. Require Ranalysis1. Require PSeries_reg. +Import R_scope. Lemma CVN_R_cos : (fn:nat->R->R) (fn == [N:nat][x:R]``(pow (-1) N)/(INR (fact (mult (S (S O)) N)))*(pow x (mult (S (S O)) N))``) -> (CVN_R fn). Unfold CVN_R; Intros. diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 6f489f37f..e64d9cc4f 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -13,6 +13,7 @@ Require Rfunctions. Require Rseries. Require Classical. Require Max. +Import R_scope. Definition Un_decreasing [Un:nat->R] : Prop := (n:nat) (Rle (Un (S n)) (Un n)). Definition opp_seq [Un:nat->R] : nat->R := [n:nat]``-(Un n)``. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 0d4bfbfad..14d438077 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -21,6 +21,7 @@ Require Export Rsigma. Require Export Rprod. Require Export Cauchy_prod. Require Export Alembert. +Import R_scope. (**********) Lemma sum_maj1 : (fn:nat->R->R;An:nat->R;x,l1,l2:R;N:nat) (Un_cv [n:nat](SP fn n x) l1) -> (Un_cv [n:nat](sum_f_R0 An n) l2) -> ((n:nat)``(Rabsolu (fn n x))<=(An n)``) -> ``(Rabsolu (l1-(SP fn N x)))<=l2-(sum_f_R0 An N)``. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 9cf2ac003..ccda09a0b 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -12,6 +12,7 @@ Require Rbase. Require Rfunctions. Require Ranalysis1. Require R_sqrt. +Import R_scope. (**********) Lemma sqrt_var_maj : (h:R) ``(Rabsolu h) <= 1`` -> ``(Rabsolu ((sqrt (1+h))-1))<=(Rabsolu h)``. diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 5c73cdae0..8efa124c3 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -32,7 +32,10 @@ Notation List := (list A). Notation Nil := (nil A). (* useless but symmetric *) Notation Cons := (cons 1!A). +Notation "<< x , y >>" := (exist List Descl x y) (at level 0) + V8only (at level 0, x,y at level 100). +V7only[ Syntax constr level 1: List [ (list A) ] -> ["List"] @@ -42,12 +45,11 @@ Syntax constr level 10: Cons2 [ (cons A $e $l) ] -> ["Cons " $e:L " " $l:L ]. -Hints Resolve d_one d_nil t_step. - Syntax constr level 1: pair_sig [ (exist (list A) Desc $e $d) ] -> ["<<" $e:L "," $d:L ">>"]. - +]. +Hints Resolve d_one d_nil t_step. Lemma left_prefix : (x,y,z:List)(ltl x^y z)-> (ltl x z). Proof. diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index be8820481..cd74d0bad 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -12,6 +12,7 @@ Require fast_integer. Require zarith_aux. Require auxiliary. Require Zsyntax. +Import Z_scope. (** Our purpose is to write an induction shema for {0,1,2,...} similar to the [nat] schema (Theorem [Natlike_rec]). For that the diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v index 7fbc56ee8..7037a5cac 100644 --- a/theories/ZArith/ZArith_dec.v +++ b/theories/ZArith/ZArith_dec.v @@ -14,6 +14,8 @@ Require fast_integer. Require zarith_aux. Require auxiliary. Require Zsyntax. +Import Z_scope. + Lemma Dcompare_inf : (r:relation) {r=EGAL} + {r=INFERIEUR} + {r=SUPERIEUR}. Proof. diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index 78f537098..ccbad9de2 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -12,6 +12,7 @@ Require ZArith_base. Require ZArithRing. Require Omega. Require Wf_nat. +Import Z_scope. (** Multiplication by a number >0 preserves [Zcompare]. It also perserves [Zle], [Zlt], [Zge], [Zgt] *) diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index c3ebf133d..aa0991583 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -23,6 +23,7 @@ Require Export ZArith_base. Require Omega. Require ZArithRing. Require Zcomplements. +Import Z_scope. (** @@ -267,6 +268,7 @@ Save. (** Syntax *) +V7only[ Grammar znatural expr2 : constr := expr_div [ expr2($p) "/" expr2($c) ] -> [ (Zdiv $p $c) ] | expr_mod [ expr2($p) "%" expr2($c) ] -> [ (Zmod $p $c) ] @@ -283,8 +285,13 @@ Syntax constr -> [ (ZEXPR $n1):E "/" [0 0] (ZEXPR $n2):L ] | Zmod_inside [ << (ZEXPR <<(Zmod $n1 $n2)>>) >> ] - -> [ (ZEXPR $n1):E "%" [0 0] (ZEXPR $n2):L ] + -> [ (ZEXPR $n1):E " %" [1 0] (ZEXPR $n2):L ] . +]. +Infix 3 "/" Zdiv : Z_scope + V8only 30. +Infix 3 "mod" Zmod : Z_scope + V8only 30. (** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) @@ -302,7 +309,7 @@ Absurd `b-a >= 1`. Omega. Rewrite -> H0. Rewrite -> H2. -Assert `c*(b/c)+b%c-(c*(a/c)+a%c) = c*(b/c - a/c) + b%c - a%c`. +Assert `c*(b/c)+b % c-(c*(a/c)+a % c) = c*(b/c - a/c) + b % c - a % c`. Ring. Rewrite H3. Assert `c*(b/c-a/c) >= c*1`. @@ -314,7 +321,7 @@ Ring. Omega. Save. -Lemma Z_mod_plus : (a,b,c:Z)`c > 0`->`(a+b*c)%c = a%c`. +Lemma Z_mod_plus : (a,b,c:Z)`c > 0`->`(a+b*c) % c = a % c`. Proof. Intros a b c cPos. Generalize (Z_div_mod_eq a c cPos). @@ -323,9 +330,9 @@ Generalize (Z_div_mod_eq `a+b*c` c cPos). Generalize (Z_mod_lt `a+b*c` c cPos). Intros. -Assert `(a+b*c)%c - a%c = c*(b+a/c - (a+b*c)/c)`. -Replace `(a+b*c)%c` with `a+b*c - c*((a+b*c)/c)`. -Replace `a%c` with `a - c*(a/c)`. +Assert `(a+b*c) % c - a % c = c*(b+a/c - (a+b*c)/c)`. +Replace `(a+b*c) % c` with `a+b*c - c*((a+b*c)/c)`. +Replace `a % c` with `a - c*(a/c)`. Ring. Omega. Omega. @@ -358,7 +365,7 @@ Generalize (Z_div_mod_eq `a+b*c` c cPos). Generalize (Z_mod_lt `a+b*c` c cPos). Intros. Apply Zmult_reg_left with c. Omega. -Replace `c*((a+b*c)/c)` with `a+b*c-(a+b*c)%c`. +Replace `c*((a+b*c)/c)` with `a+b*c-(a+b*c) % c`. Rewrite (Z_mod_plus a b c cPos). Pattern 1 a; Rewrite H2. Ring. @@ -375,7 +382,7 @@ Pattern 2 a; Rewrite H. Omega. Save. -Lemma Z_mod_same : (a:Z)`a>0`->`a%a=0`. +Lemma Z_mod_same : (a:Z)`a>0`->`a % a=0`. Proof. Intros a aPos. Generalize (Z_mod_plus `0` `1` a aPos). diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index 660a58ed6..52e2f552e 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -23,6 +23,7 @@ Require ZArith_base. Require Omega. Require Zcomplements. Require Zpower. +Import Z_scope. Section Log_pos. (* Log of positive integers *) diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v index ad5db4b53..2ed638696 100644 --- a/theories/ZArith/Zmisc.v +++ b/theories/ZArith/Zmisc.v @@ -13,6 +13,7 @@ Require zarith_aux. Require auxiliary. Require Zsyntax. Require Bool. +Import Z_scope. (** Overview of the sections of this file: - logic: Logic complements. @@ -37,8 +38,10 @@ End logic. Section numbers. -Definition entier_of_Z := [z:Z]Case z of Nul Pos Pos end. -Definition Z_of_entier := [x:entier]Case x of ZERO POS end. +Definition entier_of_Z := + [z:Z]Cases z of ZERO => Nul | (POS p) => (Pos p) | (NEG p) => (Pos p) end. +Definition Z_of_entier := + [x:entier]Cases x of Nul => ZERO | (Pos p) => (POS p) end. (* Coercion Z_of_entier : entier >-> Z. *) @@ -370,7 +373,7 @@ Qed. Theorem Zcompare_elim : (c1,c2,c3:Prop)(x,y:Z) ((x=y) -> c1) ->(`x < y` -> c2) ->(`x > y`-> c3) - -> Case `x ?= y`of c1 c2 c3 end. + -> Cases `x ?= y`of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. Intros. Apply rename with x:=`x ?= y`; Intro r; Elim r; @@ -380,7 +383,7 @@ Apply rename with x:=`x ?= y`; Intro r; Elim r; Qed. Lemma Zcompare_x_x : (x:Z) `x ?= x` = EGAL. -Intro; Apply Case (Zcompare_EGAL x x) of [h1,h2: ?]h2 end. +Intro; Apply let (h1,h2) = (Zcompare_EGAL x x) in h2. Apply refl_equal. Qed. @@ -397,7 +400,8 @@ Discriminate H. Qed. Lemma Zcompare_eq_case : - (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> (Case `x ?= y` of c1 c2 c3 end). + (c1,c2,c3:Prop)(x,y:Z) c1 -> x=y -> + Cases `x ?= y` of EGAL => c1 | INFERIEUR => c2 | SUPERIEUR => c3 end. Intros. Rewrite -> (Case (Zcompare_EGAL x y) of [h1,h2: ?]h2 end H0). Assumption. @@ -405,22 +409,26 @@ Qed. (** Four very basic lemmas about [Zle], [Zlt], [Zge], [Zgt] *) Lemma Zle_Zcompare : - (x,y:Z)`x <= y` -> Case `x ?= y` of True True False end. + (x,y:Z)`x <= y` -> + Cases `x ?= y` of EGAL => True | INFERIEUR => True | SUPERIEUR => False end. Intros x y; Unfold Zle; Elim `x ?=y`; Auto with arith. Qed. Lemma Zlt_Zcompare : - (x,y:Z)`x < y` -> Case `x ?= y` of False True False end. + (x,y:Z)`x < y` -> + Cases `x ?= y` of EGAL => False | INFERIEUR => True | SUPERIEUR => False end. Intros x y; Unfold Zlt; Elim `x ?=y`; Intros; Discriminate Orelse Trivial with arith. Qed. Lemma Zge_Zcompare : - (x,y:Z)` x >= y`-> Case `x ?= y` of True False True end. + (x,y:Z)` x >= y`-> + Cases `x ?= y` of EGAL => True | INFERIEUR => False | SUPERIEUR => True end. Intros x y; Unfold Zge; Elim `x ?=y`; Auto with arith. Qed. Lemma Zgt_Zcompare : - (x,y:Z)`x > y` -> Case `x ?= y` of False False True end. + (x,y:Z)`x > y` -> + Cases `x ?= y` of EGAL => False | INFERIEUR => False | SUPERIEUR => True end. Intros x y; Unfold Zgt; Elim `x ?= y`; Intros; Discriminate Orelse Trivial with arith. Qed. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 11ec071c1..8b68b223d 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -11,6 +11,7 @@ Require ZArith_base. Require Omega. Require Zcomplements. +Import Z_scope. Section section1. @@ -312,7 +313,7 @@ Elim (convert p); Simpl; [ Trivial with zarith | Intro n; Rewrite (two_power_nat_S n); Unfold 2 Zdiv_rest_aux; - Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)); + Elim (iter_nat n 'T:(Z*Z)*Z ' Zdiv_rest_aux ((x,`0`),`1`)); NewDestruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. Qed. @@ -374,7 +375,7 @@ Lemma Zdiv_rest_correct : (x:Z)(p:positive)(Zdiv_rest_proofs x p). Intros x p. Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p). -Elim (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)). +Elim (iter_pos p 'T:(Z*Z)*Z ' Zdiv_rest_aux ((x,`0`),`1`)). Induction a. Intros. Elim H; Intros H1 H2; Clear H. diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v index f9f8288d0..a5ddfff4f 100644 --- a/theories/ZArith/Zsqrt.v +++ b/theories/ZArith/Zsqrt.v @@ -11,6 +11,7 @@ Require Export ZArith_base. Require Export ZArithRing. Require Export Omega. +Import Z_scope. (** The following tactic replaces all instances of (POS (xI ...)) by `2*(POS ...)+1` , but only when ... is not made only with xO, XI, or xH. *) diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v index 9ac3d03d3..3f1abc8d7 100644 --- a/theories/ZArith/Zsyntax.v +++ b/theories/ZArith/Zsyntax.v @@ -11,6 +11,7 @@ Require Export fast_integer. Require Export zarith_aux. +V7only[ Grammar znatural ident := nat_id [ prim:var($id) ] -> [$id] @@ -114,9 +115,9 @@ Syntax constr | Zlt_Zlt [ (Zlt $n1 $n2)/\(Zlt $n2 $n3) ] -> [[<hov 0> "`" (ZEXPR $n1) [1 0] "< " (ZEXPR $n2) [1 0] "< " (ZEXPR $n3) "`"]] - | ZZero [ ZERO ] -> [ "`0`" ] - | ZPos [ (POS $r) ] -> [$r:"positive_printer":9] - | ZNeg [ (NEG $r) ] -> [$r:"negative_printer":9] + | ZZero_v7 [ ZERO ] -> [ "`0`" ] + | ZPos_v7 [ (POS $r) ] -> [$r:"positive_printer":9] + | ZNeg_v7 [ (NEG $r) ] -> [$r:"negative_printer":9] ; level 7: @@ -217,6 +218,7 @@ Syntax constr | ZNeg_inside [ << (ZEXPR <<(NEG $p)>>) >>] -> [$p:"negative_printer_inside":9] . +]. (* For parsing/printing based on scopes *) Module Z_scope. @@ -226,44 +228,46 @@ Module Z_scope. Delimits Scope positive_scope with P. Delimits Scope Z_scope with Z. -Infix "+" Zplus (at level 4) : Z_scope. -Infix "-" Zminus (at level 4) : Z_scope. -Infix "*" Zmult (at level 3) : Z_scope. -Distfix 0 "- _" Zopp : Z_scope. -Infix "<=" Zle (at level 5, no associativity) : Z_scope. -Infix "<" Zlt (at level 5, no associativity) : Z_scope. -Infix ">=" Zge (at level 5, no associativity) : Z_scope. -Infix ">" Zgt (at level 5, no associativity) : Z_scope. -Infix "? =" Zcompare (at level 5, no associativity) : Z_scope. +(* Warning: this hides sum and prod and breaks sumor symbolic notation *) +Open Scope Z_scope. + +Arguments Scope POS [positive_scope]. +Arguments Scope NEG [positive_scope]. + +Infix LEFTA 4 "+" Zplus : Z_scope. +Infix LEFTA 4 "-" Zminus : Z_scope. +Infix LEFTA 3 "*" Zmult : Z_scope. +Notation "- x" := (Zopp x) (at level 0) : Z_scope + V8only (at level 40). +Infix NONA 5 "<=" Zle : Z_scope. +Infix NONA 5 "<" Zlt : Z_scope. +Infix NONA 5 ">=" Zge : Z_scope. +Infix NONA 5 ">" Zgt : Z_scope. +Infix NONA 5 "?=" Zcompare : Z_scope. Notation "x <= y <= z" := (Zle x y)/\(Zle y z) - (at level 5, y at level 4):Z_scope. + (at level 5, y at level 4):Z_scope + V8only (at level 50, y at level 49). Notation "x <= y < z" := (Zle x y)/\(Zlt y z) - (at level 5, y at level 4):Z_scope. + (at level 5, y at level 4):Z_scope + V8only (at level 50, y at level 49). Notation "x < y < z" := (Zlt x y)/\(Zlt y z) - (at level 5, y at level 4):Z_scope. + (at level 5, y at level 4):Z_scope + V8only (at level 50, y at level 49). Notation "x < y <= z" := (Zlt x y)/\(Zle y z) - (at level 5, y at level 4):Z_scope. + (at level 5, y at level 4):Z_scope + V8only (at level 50, y at level 49). Notation "x = y = z" := x=y/\y=z - (at level 5, y at level 4):Z_scope. + (at level 5, y at level 4) : Z_scope + V8only (at level 50, y at level 49). -Notation "x <> y" := ~(eq Z x y) (at level 5) : Z_scope. +Notation "x <> y" := ~(eq Z x y) (at level 5, no associativity) : Z_scope + V8only (at level 50, no associativity). (* Notation "| x |" (Zabs x) : Z_scope.(* "|" conflicts with THENS *)*) +V7only[ (* Overwrite the printing of "`x = y`" *) Syntax constr level 0: Zeq [ (eq Z $n1 $n2) ] -> [[<hov 0> $n1 [1 0] "= " $n2 ]]. - - -(* Warning: this hides sum and prod and breaks sumor symbolic notation *) -Open Scope Z_scope. - -(* -Syntax constr - level 0: - | ZZero' [ ZERO ] -> [dummy:"z_printer_ZERO"] - | ZPos' [ (POS $r) ] -> [$r:"z_printer_POS":9] - | ZNeg' [ (NEG $r) ] -> [$r:"z_printer_NEG":9] -. -*) +]. End Z_scope. diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 56baf1782..d93a6ea44 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -11,6 +11,7 @@ Require ZArith_base. Require Export Wf_nat. Require Omega. +Import Z_scope. (** Well-founded relations on Z. *) diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v index fe16e8dff..8b73960be 100644 --- a/theories/ZArith/fast_integer.v +++ b/theories/ZArith/fast_integer.v @@ -75,7 +75,7 @@ with add_carry [x,y:positive]:positive := end end. -Infix "+" add (at level 4, left associativity) : positive_scope. +Infix LEFTA 4 "+" add : positive_scope. Open Scope positive_scope. @@ -1020,7 +1020,8 @@ Fixpoint times [x:positive] : positive -> positive:= | xH => y end. -Infix "*" times (at level 3, left associativity) : positive_scope. +Infix LEFTA 3 "*" times : positive_scope + V8only 30. (** Correctness of multiplication on positive *) Theorem times_convert : @@ -1065,7 +1066,8 @@ Definition Zmult := [x,y:Z] end end. -Infix "*" Zmult (at level 3, left associativity) : Z_scope. +Infix LEFTA 3 "*" Zmult : Z_scope + V8only 30. Open Scope Z_scope. |