aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend32
-rw-r--r--CHANGES9
-rw-r--r--Makefile17
-rw-r--r--parsing/g_rsyntax.ml70
-rw-r--r--parsing/lexer.mll2
-rw-r--r--theories/Reals/Raxioms.v65
-rw-r--r--theories/Reals/Rbase.v24
-rw-r--r--theories/Reals/Rdefinitions.v36
-rw-r--r--theories/Reals/Reals.v1
-rw-r--r--theories/Reals/Rlimit.v659
-rw-r--r--theories/Reals/Rsyntax.v182
11 files changed, 495 insertions, 602 deletions
diff --git a/.depend b/.depend
index 299eb3d9d..db13f54aa 100644
--- a/.depend
+++ b/.depend
@@ -439,14 +439,6 @@ parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
parsing/pcoq.cmi lib/pp.cmi lib/util.cmi parsing/extend.cmi
parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
parsing/pcoq.cmx lib/pp.cmx lib/util.cmx parsing/extend.cmi
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
- toplevel/vernac.cmi
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
- toplevel/vernac.cmx
-parsing/g_cases.cmo: parsing/coqast.cmi parsing/pcoq.cmi
-parsing/g_cases.cmx: parsing/coqast.cmx parsing/pcoq.cmx
-parsing/g_constr.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi
-parsing/g_constr.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx
parsing/g_natsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi \
parsing/coqast.cmi parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi \
lib/pp.cmi lib/util.cmi parsing/g_natsyntax.cmi
@@ -455,18 +447,12 @@ parsing/g_natsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx \
lib/pp.cmx lib/util.cmx parsing/g_natsyntax.cmi
parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi
parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmx toplevel/vernac.cmx
-parsing/g_proofs.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
- lib/util.cmi toplevel/vernac.cmi
-parsing/g_proofs.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
- lib/util.cmx toplevel/vernac.cmx
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
- lib/pp.cmi lib/util.cmi
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmx \
- lib/pp.cmx lib/util.cmx
-parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi lib/pp.cmi \
- lib/util.cmi toplevel/vernac.cmi
-parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmx lib/pp.cmx \
- lib/util.cmx toplevel/vernac.cmx
+parsing/g_rsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
+ parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
+ lib/util.cmi
+parsing/g_rsyntax.cmx: parsing/ast.cmx parsing/astterm.cmx parsing/coqast.cmx \
+ parsing/esyntax.cmx kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx \
+ lib/util.cmx
parsing/g_zsyntax.cmo: parsing/ast.cmi parsing/astterm.cmi parsing/coqast.cmi \
parsing/esyntax.cmi kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi \
lib/util.cmi parsing/g_zsyntax.cmi
@@ -943,12 +929,6 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx \
kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
kernel/term.cmx lib/util.cmx tactics/tactics.cmi
-tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
- kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
- proofs/tacmach.cmi tactics/tacticals.cmi
-tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
- kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
- proofs/tacmach.cmx tactics/tacticals.cmx
tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi parsing/pattern.cmi \
pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi
tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx parsing/pattern.cmx \
diff --git a/CHANGES b/CHANGES
index 07417a10f..5d360e0f6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,8 +9,6 @@ Parsing
- "command" in grammars and quotations is now "constr" as in
pretty-printing rules
-
-
Syntaxe des constructions
- Consecutive as in patterns are forbidden
@@ -26,6 +24,13 @@ Syntaxe des constructions
cas de clauses par défaut redondantes auquel cas la première est prise
avec un avertissement.
+Syntaxe des theories
+
+- Ajout d'une syntaxe pour les reels: ``Rexpr``.
+ Point noir du aux constantes:
+ (Rplus (Rplus (Rplus R1 R1) (Rplus R1 R1)) R1) est toujours (2+2+1)
+ au lieu de 2+2+1
+
Vernac
- Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des
diff --git a/Makefile b/Makefile
index 0b24e6dd0..3c979eaff 100644
--- a/Makefile
+++ b/Makefile
@@ -92,9 +92,9 @@ PARSING=parsing/lexer.cmo parsing/coqast.cmo parsing/pcoq.cmo parsing/ast.cmo \
parsing/g_constr.cmo parsing/g_cases.cmo \
parsing/extend.cmo parsing/esyntax.cmo \
parsing/printer.cmo parsing/pretty.cmo parsing/egrammar.cmo \
- parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo
+ parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
-# ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo
+ARITHSYNTAX=parsing/g_natsyntax.cmo parsing/g_zsyntax.cmo parsing/g_rsyntax.cmo
PROOFS=proofs/proof_type.cmo proofs/proof_trees.cmo proofs/logic.cmo \
proofs/refiner.cmo proofs/evar_refiner.cmo proofs/tacmach.cmo \
@@ -295,11 +295,12 @@ WELLFOUNDEDVO=theories/Wellfounded/Disjoint_Union.vo \
theories/Wellfounded/Well_Ordering.vo \
theories/Wellfounded/Lexicographic_Product.vo
-REALSVO=theories/Reals/R_Ifp.vo theories/Reals/Reals.vo \
- theories/Reals/Raxioms.vo theories/Reals/Rfunctions.vo \
- theories/Reals/Rbase.vo theories/Reals/Rlimit.vo \
- theories/Reals/Rbasic_fun.vo theories/Reals/TypeSyntax.vo \
- theories/Reals/Rderiv.vo
+REALSVO=theories/Reals/TypeSyntax.vo \
+ theories/Reals/Rdefinitions.vo theories/Reals/Rsyntax.vo \
+ theories/Reals/Raxioms.vo theories/Reals/Rbase.vo \
+ theories/Reals/R_Ifp.vo theories/Reals/Rbasic_fun.vo \
+ theories/Reals/Rfunctions.vo theories/Reals/Rlimit.vo \
+ theories/Reals/Rderiv.vo theories/Reals/Reals.vo
THEORIESVO = $(LOGICVO) $(ARITHVO) $(BOOLVO) $(ZARITHVO) $(LISTSVO) \
$(SETSVO) $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO)
@@ -584,7 +585,7 @@ clean::
.el.elc:
echo "(setq load-path (cons \".\" load-path))" > $*.compile
echo "(byte-compile-file \"$<\")" >> $*.compile
- $(EMACS) -batch -l $*.compile
+ - $(EMACS) -batch -l $*.compile
rm -f $*.compile
###########################################################################
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
new file mode 100644
index 000000000..d4e56c86b
--- /dev/null
+++ b/parsing/g_rsyntax.ml
@@ -0,0 +1,70 @@
+open Coqast
+open Ast
+open Pp
+open Util
+open Names
+open Pcoq
+
+exception Non_closed_number
+
+let get_r_sign loc =
+ let ast_of_id id = Astterm.globalize_constr (Nvar(loc,id)) in
+ ((ast_of_id "R0", ast_of_id "R1", ast_of_id "Rplus",
+ ast_of_id "NRplus"))
+
+let r_of_int n dloc =
+ let (ast0,ast1,astp,_) = get_r_sign dloc in
+ let rec mk_r n =
+ if n <= 0 then
+ ast0
+ else if n = 1 then
+ ast1
+ else
+ Node(dloc,"APPLIST", [astp; mk_r (n-1); ast1])
+ in
+ mk_r n
+
+let r_of_string s dloc =
+ r_of_int (int_of_string s) dloc
+
+let rnumber =
+ match create_entry (get_univ "rnatural") "rnumber" ETast with
+ | Ast n -> n
+ | _ -> anomaly "G_rsyntax : create_entry rnumber failed"
+
+let _ =
+ Gram.extend rnumber None
+ [None, None,
+ [[Gramext.Stoken ("INT", "")],
+ Gramext.action r_of_string]]
+
+(** pp **)
+
+let rec int_of_r_rec ast1 astp p =
+ match p with
+ | Node (_,"APPLIST", [b; a; c]) when alpha_eq(b,astp) &&
+ alpha_eq(c,ast1) ->
+ (int_of_r_rec ast1 astp a)+1
+ | a when alpha_eq(a,ast1) -> 1
+ | _ -> raise Non_closed_number
+
+let int_of_r p =
+ let (_,ast1,astp,_) = get_r_sign dummy_loc in
+ try
+ Some (int_of_r_rec ast1 astp p)
+ with
+ Non_closed_number -> None
+
+let replace_plus p =
+ let (_,ast1,_,astnr) = get_r_sign dummy_loc in
+ ope ("REXPR",[ope("APPLIST", [astnr; p; ast1;])])
+
+let r_printer std_pr p =
+ let (_,ast1,astp,_) = get_r_sign dummy_loc in
+ match (int_of_r p) with
+ | Some i -> [< 'sTR (string_of_int (i+1)) >]
+ | None -> std_pr (replace_plus p)
+
+
+let _ = Esyntax.Ppprim.add ("r_printer", r_printer)
+
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index d9270647e..659723170 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -136,7 +136,7 @@ rule token = parse
if is_keyword s then ("",s) else ("IDENT",s) }
| decimal_literal | hex_literal | oct_literal | bin_literal
{ ("INT", Lexing.lexeme lexbuf) }
- | "(" | ")" | "[" | "]" | "{" | "}" | "_" | ";"| "`" | "()" | "'("
+ | "(" | ")" | "[" | "]" | "{" | "}" | "." | "_" | ";"| "`" | "``" | "()" | "'("
| "->" | "\\/" | "/\\" | "|-" | ":=" | "<->" | extrachar
{ ("", Lexing.lexeme lexbuf) }
| "." blank
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 2297e7d7b..21ab28be8 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -7,31 +7,9 @@
(*********************************************************)
Require Export ZArith.
+Require Export Rsyntax.
Require Export TypeSyntax.
-Parameter R:Type.
-Parameter R0:R.
-Parameter R1:R.
-Parameter Rplus:R->R->R.
-Parameter Rmult:R->R->R.
-Parameter Ropp:R->R.
-Parameter Rinv:R->R.
-Parameter Rlt:R->R->Prop.
-Parameter up:R->Z.
-(*********************************************************)
-
-(**********)
-Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
-
-(**********)
-Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
-
-(**********)
-Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
-
-(**********)
-Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
-
(*********************************************************)
(* Field axioms *)
(*********************************************************)
@@ -40,18 +18,17 @@ Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
(*********************************************************)
(**********)
-Axiom Rplus_sym:(r1,r2:R)((Rplus r1 r2)==(Rplus r2 r1)).
+Axiom Rplus_sym:(r1,r2:R)``r1+r2==r2+r1``.
(**********)
-Axiom Rplus_assoc:(r1,r2,r3:R)
- ((Rplus (Rplus r1 r2) r3)==(Rplus r1 (Rplus r2 r3))).
+Axiom Rplus_assoc:(r1,r2,r3:R)``(r1+r2)+r3==r1+(r2+r3)``.
(**********)
-Axiom Rplus_Ropp_r:(r:R)((Rplus r (Ropp r))==R0).
+Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``.
Hints Resolve Rplus_Ropp_r : real v62.
(**********)
-Axiom Rplus_ne:(r:R)(((Rplus r R0)==r)/\((Rplus R0 r)==r)).
+Axiom Rplus_ne:(r:R)``r+0==r``/\``0+r==r``.
Hints Resolve Rplus_ne : real v62.
(***********************************************************)
@@ -59,19 +36,18 @@ Hints Resolve Rplus_ne : real v62.
(***********************************************************)
(**********)
-Axiom Rmult_sym:(r1,r2:R)((Rmult r1 r2)==(Rmult r2 r1)).
+Axiom Rmult_sym:(r1,r2:R)``r1*r2==r2*r1``.
Hints Resolve Rmult_sym : real v62.
(**********)
-Axiom Rmult_assoc:(r1,r2,r3:R)
- ((Rmult (Rmult r1 r2) r3)==(Rmult r1 (Rmult r2 r3))).
+Axiom Rmult_assoc:(r1,r2,r3:R)``(r1*r2)*r3==r1*(r2*r3)``.
Hints Resolve Rmult_assoc : real v62.
(**********)
-Axiom Rinv_l:(r:R)(~(r==R0))->((Rmult (Rinv r) r)==R1).
+Axiom Rinv_l:(r:R)``r<>0``->``(1/r)*r==1``.
(**********)
-Axiom Rmult_ne:(r:R)(((Rmult r R1)==r)/\((Rmult R1 r)==r)).
+Axiom Rmult_ne:(r:R)``r*1==r``/\``1*r==r``.
Hints Resolve Rmult_ne : real v62.
(**********)
@@ -82,8 +58,7 @@ Axiom R1_neq_R0:(~R1==R0).
(*********************************************************)
(**********)
-Axiom Rmult_Rplus_distr:(r1,r2,r3:R)
- ((Rmult r1 (Rplus r2 r3))==(Rplus (Rmult r1 r2) (Rmult r1 r3))).
+Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``.
Hints Resolve Rmult_Rplus_distr : real v62.
(*********************************************************)
@@ -94,27 +69,24 @@ Hints Resolve Rmult_Rplus_distr : real v62.
(*********************************************************)
(**********)
-Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT (Rlt r1 r2) (r1==r2))
- (Rgt r1 r2)).
+Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``).
(*********************************************************)
(* Lower *)
(*********************************************************)
(**********)
-Axiom Rlt_antisym:(r1,r2:R)(Rlt r1 r2) -> ~(Rlt r2 r1).
+Axiom Rlt_antisym:(r1,r2:R)``r1<r2`` -> ~ ``r2<r1``.
(**********)
Axiom Rlt_trans:(r1,r2,r3:R)
- (Rlt r1 r2)->(Rlt r2 r3)->(Rlt r1 r3).
+ ``r1<r2``->``r2<r3``->``r1<r3``.
(**********)
-Axiom Rlt_compatibility:(r,r1,r2:R)(Rlt r1 r2)->
- (Rlt (Rplus r r1) (Rplus r r2)).
+Axiom Rlt_compatibility:(r,r1,r2:R)``r1<r2``->``r+r1<r+r2``.
(**********)
-Axiom Rlt_monotony:(r,r1,r2:R)(Rlt R0 r)->(Rlt r1 r2)->
- (Rlt (Rmult r r1) (Rmult r r2)).
+Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``.
(**********************************************************)
(* Injection from N to R *)
@@ -143,22 +115,21 @@ Definition IZR:Z->R:=[z:Z](Cases z of
(**********************************************************)
(**********)
-Axiom archimed:(r:R)(Rgt (IZR (up r)) r)/\
- (Rle (Rminus (IZR (up r)) r) R1).
+Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``.
(**********************************************************)
(* R Complete *)
(**********************************************************)
(**********)
-Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->(Rle x m).
+Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->``x <= m``.
(**********)
Definition bound:=[E:R->Prop](ExT [m:R](is_upper_bound E m)).
(**********)
Definition is_lub:=[E:R->Prop][m:R]
- (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->(Rle m b).
+ (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->``m <= b``.
(**********)
Axiom complet:(E:R->Prop)(bound E)->
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index b459a3d85..970b18ee4 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -45,7 +45,7 @@ Save.
Hints Resolve Req_EM : real v62.
(**********)
-Lemma total_order:(r1,r2:R)((Rlt r1 r2)\/(r1==r2)\/(Rgt r1 r2)).
+Lemma total_order:(r1,r2:R)``r1<r2``\/(r1==r2)\/``r1>r2``.
Intros;Elim (total_order_T r1 r2);Intro;Auto.
Elim y;Intro;Auto.
Save.
@@ -606,6 +606,15 @@ Intros; Generalize (Rlt_compatibility r3 r1 r2 H);
Save.
(*********)
+Lemma Rplus_lt_le_lt:(r1,r2,r3,r4:R)(Rlt r1 r2)->(Rle r3 r4)->
+ (Rlt (Rplus r1 r3) (Rplus r2 r4)).
+Intros;Unfold Rle in H0; Elim H0.
+Exact (Rplus_lt r1 r2 r3 r4 H).
+Intro;Rewrite H1;Rewrite (Rplus_sym r1 r4);Rewrite (Rplus_sym r2 r4);
+ Exact (Rlt_compatibility r4 r1 r2 H).
+Save.
+
+(*********)
Lemma Rmult_lt:(r1,r2,r3,r4:R)(Rgt r3 R0)->(Rgt r2 R0)->
(Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)).
Intros;Unfold Rgt in H H0;Generalize (Rlt_monotony r3 r1 r2 H H1);Intro;
@@ -951,6 +960,19 @@ Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro;
Save.
(*********)
+Lemma Rmult_lt_0:(r1,r2,r3,r4:R)(Rge r3 R0)->(Rgt r2 R0)->
+ (Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)).
+Intros;Elim H.
+Intro;Exact (Rmult_lt r1 r2 r3 r4 H3 H0 H1 H2).
+Intro;Rewrite H3;Rewrite (Rmult_Or r1);
+ Cut (Rgt r4 R0).
+Intro;Exact (Rmult_gt r2 r4 H0 H4).
+Cut (Rle R0 r3).
+Intro;Exact (Rle_lt_trans R0 r3 r4 H4 H2).
+Exact (Rle_sym2 R0 r3 H).
+Save.
+
+(*********)
Lemma Rmult_lt_pos:(x,y:R)(Rlt R0 x)->(Rlt R0 y)->(Rlt R0 (Rmult x y)).
Generalize Rmult_gt;Unfold Rgt;Auto.
Save.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
new file mode 100644
index 000000000..ecaa7b4ca
--- /dev/null
+++ b/theories/Reals/Rdefinitions.v
@@ -0,0 +1,36 @@
+(* $Id$ *)
+
+
+(*********************************************************)
+(* Definitions for the axiomatization *)
+(* *)
+(*********************************************************)
+
+Require Export ZArith.
+Require Export TypeSyntax.
+
+Parameter R:Type.
+Parameter R0:R.
+Parameter R1:R.
+Parameter Rplus:R->R->R.
+Parameter Rmult:R->R->R.
+Parameter Ropp:R->R.
+Parameter Rinv:R->R.
+Parameter Rlt:R->R->Prop.
+Parameter up:R->Z.
+(*********************************************************)
+
+(**********)
+Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
+
+(**********)
+Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
+
+(**********)
+Definition Rdiv:R->R->R:=[r1,r2:R](Rmult r1 (Rinv r2)).
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index c9ee14137..3af2faa4c 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -1,6 +1,7 @@
(* $Id$ *)
+Require Export Rdefinitions.
Require Export TypeSyntax.
Require Export Raxioms.
Require Export Rbase.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 56a7c709d..465dfd7a4 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -134,6 +134,53 @@ Clear H0;Generalize (H r H1); Intro;Generalize (Rlt_antirefl r);
Intro;ElimType False; Auto.
Save.
+(*********)
+Definition mul_factor := [l,l':R](Rinv (Rplus R1 (Rplus (Rabsolu l)
+ (Rabsolu l')))).
+
+(*********)
+Lemma mul_factor_wd : (l,l':R)
+ ~(Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))==R0.
+Intros;Rewrite (Rplus_sym R1 (Rplus (Rabsolu l) (Rabsolu l')));
+ Apply tech_Rplus.
+Cut (Rle (Rabsolu (Rplus l l')) (Rplus (Rabsolu l) (Rabsolu l'))).
+Cut (Rle R0 (Rabsolu (Rplus l l'))).
+Exact (Rle_trans ? ? ?).
+Exact (Rabsolu_pos (Rplus l l')).
+Exact (Rabsolu_triang ? ?).
+Exact Rlt_R0_R1.
+Save.
+
+(*********)
+Lemma mul_factor_gt:(eps:R)(l,l':R)(Rgt eps R0)->
+ (Rgt (Rmult eps (mul_factor l l')) R0).
+Intros;Unfold Rgt;Rewrite <- (Rmult_Or eps);Apply Rlt_monotony.
+Assumption.
+Unfold mul_factor;Apply Rlt_Rinv;
+ Cut (Rle R1 (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))).
+Cut (Rlt R0 R1).
+Exact (Rlt_le_trans ? ? ?).
+Exact Rlt_R0_R1.
+Replace (Rle R1 (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l'))))
+ with (Rle (Rplus R1 R0) (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))).
+Apply Rle_compatibility.
+Cut (Rle (Rabsolu (Rplus l l')) (Rplus (Rabsolu l) (Rabsolu l'))).
+Cut (Rle R0 (Rabsolu (Rplus l l'))).
+Exact (Rle_trans ? ? ?).
+Exact (Rabsolu_pos ?).
+Exact (Rabsolu_triang ? ?).
+Rewrite (proj1 ? ? (Rplus_ne R1));Trivial.
+Save.
+
+(*********)
+Lemma mul_factor_gt_f:(eps:R)(l,l':R)(Rgt eps R0)->
+ (Rgt (Rmin R1 (Rmult eps (mul_factor l l'))) R0).
+Intros;Apply Rmin_Rgt_r;Split.
+Exact Rlt_R0_R1.
+Exact (mul_factor_gt eps l l' H).
+Save.
+
+
(*******************************)
(* Metric space *)
(*******************************)
@@ -329,6 +376,16 @@ Unfold 2 3 Rminus;
Apply (eq_Rle (Rminus x y) (Rminus x y) (refl_eqT R (Rminus x y))).
Save.
+(*********)
+Lemma R_dist_plus: (a,b,c,d:R)(Rle (R_dist (Rplus a c) (Rplus b d))
+ (Rplus (R_dist a b) (R_dist c d))).
+Intros;Unfold R_dist;
+ Replace (Rminus (Rplus a c) (Rplus b d))
+ with (Rplus (Rminus a b) (Rminus c d)).
+Exact (Rabsolu_triang (Rminus a b) (Rminus c d)).
+Ring.
+Save.
+
(*******************************)
(* R is a metric space *)
(*******************************)
@@ -378,36 +435,27 @@ Save.
Lemma limit_plus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
(limit1_in f D l x0)->(limit1_in g D l' x0)->
(limit1_in [x:R](Rplus (f x) (g x)) D (Rplus l l') x0).
-Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+Intros;Unfold limit1_in; Unfold limit_in; Simpl; Intros;
Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
- Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
- Clear H H0;Intros;Elim H;Elim H0;Clear H H0;Intros;
- Split with (Rmin x1 x);Split.
-Elim (Rmin_Rgt x1 x R0);Intros a b;
- Apply (b (conj (Rgt x1 R0) (Rgt x R0) H H2));Clear a b.
-Intros;Elim H4;Clear H4;Intros;Elim (Rmin_Rgt x1 x (R_dist x2 x0));
- Intros a b;Clear b;Unfold Rgt in a;Elim (a H5);Clear H5 a;Intros;
- Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5));
- Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));
- Clear H0 H3 H5 H6;Intros;
- Generalize (Rplus_lt (R_dist (f x2) l)
- (Rmult eps (Rinv (Rplus R1 R1)))
- (R_dist (g x2) l')
- (Rmult eps (Rinv (Rplus R1 R1))) H3 H0);
- Clear H0 H3 H4;Intro;Rewrite (eps2 eps) in H0;Unfold R_dist;
- Unfold Rminus;Rewrite (Rplus_sym l l');Rewrite (Ropp_distr1 l' l);
- Rewrite <-(Rplus_assoc (Rplus (f x2) (g x2)) (Ropp l') (Ropp l));
- Rewrite (Rplus_assoc (f x2) (g x2) (Ropp l'));
- Rewrite (Rplus_sym (Rplus (f x2) (Rplus (g x2) (Ropp l')))
- (Ropp l));
- Rewrite <-(Rplus_assoc (Ropp l) (f x2) (Rplus (g x2) (Ropp l')));
- Rewrite (Rplus_sym (Ropp l) (f x2));
- Fold (Rminus (f x2) l);Fold (Rminus (g x2) l');Unfold R_dist in H0;
- Apply (Rle_lt_trans
- (Rabsolu (Rplus (Rminus (f x2) l) (Rminus (g x2) l')))
- (Rplus (Rabsolu (Rminus (f x2) l)) (Rabsolu (Rminus (g x2) l')))
- eps
- (Rabsolu_triang (Rminus (f x2) l) (Rminus (g x2) l')) H0).
+ Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
+ Simpl;Clear H H0; Intros; Elim H; Elim H0; Clear H H0; Intros;
+ Split with (Rmin x1 x); Split.
+Exact (Rmin_Rgt_r x1 x R0 (conj ? ? H H2)).
+Intros;Elim H4; Clear H4; Intros;
+ Cut (Rlt (Rplus (R_dist (f x2) l) (R_dist (g x2) l')) eps).
+ Cut (Rle (R_dist (Rplus (f x2) (g x2)) (Rplus l l'))
+ (Rplus (R_dist (f x2) l) (R_dist (g x2) l'))).
+Exact (Rle_lt_trans ? ? ?).
+Exact (R_dist_plus ? ? ? ?).
+Elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); Clear H5; Intros.
+Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));
+ Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5));
+ Intros;
+ Replace eps
+ with (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
+ (Rmult eps (Rinv (Rplus R1 R1)))).
+Exact (Rplus_lt ? ? ? ? H7 H8).
+Exact (eps2 eps).
Save.
(*********)
@@ -441,494 +489,71 @@ Save.
Lemma limit_mul:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
(limit1_in f D l x0)->(limit1_in g D l' x0)->
(limit1_in [x:R](Rmult (f x) (g x)) D (Rmult l l') x0).
-Unfold limit1_in;Unfold limit_in;Simpl;Intros;
- Elim (Req_EM l R0);Elim (Req_EM l' R0);Intros.
-(**)
-Rewrite H2;Rewrite H3;Rewrite H2 in H0;Rewrite H3 in H;
- Rewrite (Rmult_Or R0);Unfold R_dist;Unfold R_dist in H H0;
- Elim (H eps H1);Clear H;Unfold 1 Rgt in H0;Elim (H0 R1 Rlt_R0_R1);
- Clear H0;Intros;Elim H;Elim H0;Clear H H0;Intros;
- Split with (Rmin x1 x);Split.
-Elim (Rmin_Rgt x1 x R0);Intros a b;
- Apply (b (conj (Rgt x1 R0) (Rgt x R0) H H4));Clear a b.
-Intros;Elim H6;Clear H6;Intros;Elim (Rmin_Rgt x1 x (R_dist x2 x0));
- Intros a b;Clear b;Unfold Rgt in a;Elim (a H7);Clear H7 a;Intros;
- Unfold R_dist in H7 H8;
- Generalize (H0 x2 (conj (D x2)
- (Rlt (Rabsolu (Rminus x2 x0)) x1) H6 H7));
- Generalize (H5 x2 (conj (D x2)
- (Rlt (Rabsolu (Rminus x2 x0)) x) H6 H8));Intros;
- Clear H0 H5 H7 H8;Rewrite (minus_R0 (g x2)) in H9;
- Rewrite (minus_R0 (f x2)) in H10;
- Rewrite (minus_R0 (Rmult (f x2) (g x2)));
- Generalize Rlt_R0_R1;Intro;Fold (Rgt R1 R0) in H0;
- Rewrite (Rabsolu_mult (f x2) (g x2));
- Rewrite <-(let (H1,H2)=(Rmult_ne eps) in H1);
- Generalize (Rabsolu_pos (g x2));Unfold Rle;Intro;Elim H5;Clear H5;
- Intro.
-Apply (Rmult_lt (Rabsolu (f x2)) eps (Rabsolu (g x2)) R1 H5 H1 H10 H9).
-Rewrite <-H5;Rewrite (Rmult_Or (Rabsolu (f x2)));
- Rewrite (let (H1,H2)=(Rmult_ne eps) in H1);Unfold Rgt in H1;Assumption.
-(**)
-Rewrite H3;Rewrite H3 in H;Rewrite (Rmult_Ol l');
- Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));Intros;
- Elim H4;Clear H4;Intros;
- Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H R1 H6);Intros;
- Elim H7;Clear H7;Intros;
- Cut (Rgt (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))) R0).
-Intro;Elim (H (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))) H9);
- Intros;Elim H10;Clear H10;Intros;Split with (Rmin (Rmin x x1) x2);
- Split.
-Elim (Rmin_Rgt (Rmin x x1) x2 R0);Intros;Elim (Rmin_Rgt x x1 R0);Intros;
- Generalize (H15 (conj (Rgt x R0) (Rgt x1 R0) H4 H7));Clear H14 H15;
- Intro;Clear H12;
- Apply (H13 (conj (Rgt (Rmin x x1) R0) (Rgt x2 R0) H14 H10)).
-Intros;Elim H12;Clear H12;Intros;
- Elim (Rmin_Rgt (Rmin x x1) x2 (R_dist x3 x0));Intros;Clear H15;
- Unfold 1 Rgt in H14;Elim (H14 H13);Clear H14;Intros;Unfold Rgt in H15;
- Clear H13;Elim (Rmin_Rgt x x1 (R_dist x3 x0));Intros;
- Elim (H13 H14);Clear H14 H13 H16;Intros;Unfold Rgt in H13 H14;
- Generalize (H5 x3 (conj (D x3) (Rlt (R_dist x3 x0) x) H12 H13));
- Generalize (H8 x3 (conj (D x3) (Rlt (R_dist x3 x0) x1) H12 H14));
- Generalize (H11 x3 (conj (D x3) (Rlt (R_dist x3 x0) x2) H12 H15));
- Clear H5 H8 H11 H15 H13 H14 H12;Intros;Unfold R_dist in H5 H8 H11;
- Unfold R_dist;Rewrite (minus_R0 (Rmult (f x3) (g x3)));
- Rewrite (minus_R0 (f x3)) in H5;Rewrite (minus_R0 (f x3)) in H8;
- Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x3) (g x3))) in H1);
- Rewrite <-(Rplus_Ropp_l (Rmult (f x3) l'));Rewrite (Rmult_sym (f x3) l');
- Rewrite <-(Ropp_mul1 l' (f x3));
- Rewrite (Rmult_sym (Ropp l') (f x3));
- Rewrite <-(Rplus_assoc (Rmult (f x3) (g x3))
- (Rmult (f x3) (Ropp l')) (Rmult l' (f x3)));
- Rewrite <-(Rmult_Rplus_distr (f x3) (g x3) (Ropp l'));Fold (Rminus (g x3) l');
- Generalize (Rabsolu_triang (Rmult (f x3) (Rminus (g x3) l'))
- (Rmult l' (f x3)));Intro;
- Apply (Rle_lt_trans
- (Rabsolu (Rplus (Rmult (f x3) (Rminus (g x3) l')) (Rmult l' (f x3))))
- (Rplus (Rabsolu (Rmult (f x3) (Rminus (g x3) l')))
- (Rabsolu (Rmult l' (f x3)))) eps H12);Clear H12;
- Rewrite (Rabsolu_mult (f x3) (Rminus (g x3) l'));
- Rewrite (Rabsolu_mult l' (f x3));
- Elim (Req_EM (f x3) R0);Intros.
-Rewrite H12;Rewrite Rabsolu_R0;
- Rewrite (Rmult_Ol (Rabsolu (Rminus (g x3) l')));
- Rewrite (Rmult_Or (Rabsolu l'));
- Rewrite (let (H1,H2)=(Rplus_ne R0) in H1);
- Unfold Rgt in H1;Assumption.
-Generalize (Rabsolu_pos_lt (f x3) H12);Intro;
- Fold (Rgt (Rabsolu (f x3)) R0) in H13;
- Generalize (Rmult_lt (Rabsolu (Rminus (g x3) l'))
- (Rmult eps (Rinv (Rplus R1 R1)))
- (Rabsolu (f x3)) R1 H13 (eps2_Rgt_R0 eps H1)
- H11 H8);Intro;
- Generalize (Rlt_monotony (Rabsolu l') (Rabsolu (f x3))
- (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))))
- (Rabsolu_pos_lt l' H2) H5);Clear H5 H8 H11 H12 H13;Intro;
- Rewrite (Rmult_sym (Rabsolu (Rminus (g x3) l')) (Rabsolu (f x3)))
- in H14;Generalize (Rplus_lt
- (Rmult (Rabsolu (f x3)) (Rabsolu (Rminus (g x3) l')))
- (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
- (Rmult (Rabsolu l') (Rabsolu (f x3)))
- (Rmult (Rabsolu l')
- (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))))) H14 H5);
- Clear H5 H14;Intro;
- Cut eps==(Rplus (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
- (Rmult (Rabsolu l')
- (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))))).
-Intro;Rewrite <-H8 in H5;Assumption.
-Rewrite (let (H1,H2)=
- (Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H1);
- Cut ~(Rabsolu l')==R0.
-Intro;Rewrite (Rinv_Rmult (Rplus R1 R1) (Rabsolu l'));Auto.
-Rewrite (Rmult_sym (Rabsolu l')
- (Rmult eps (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l')))));
- Rewrite (Rmult_assoc eps
- (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l')))
- (Rabsolu l'));
- Rewrite (Rmult_assoc (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l'))
- (Rabsolu l'));
- Rewrite (Rinv_l (Rabsolu l') H8);
- Rewrite (let (H1,H2)=
- (Rmult_ne (Rinv (Rplus R1 R1))) in H1);
- Apply sym_eqT;Apply eps2.
-Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H12;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H11 H12).
-Generalize (Rabsolu_pos_lt l' H2);Intro;
- Apply (imp_not_Req (Rabsolu l') R0);Auto.
-Unfold Rgt;Unfold Rgt in H1;
- Rewrite <-(Rmult_Or (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))));
- Rewrite (Rmult_sym eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))));
- Apply (Rlt_monotony (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))) R0 eps);
- Auto.
-Apply (Rlt_Rinv (Rmult (Rplus R1 R1) (Rabsolu l')));
- Generalize (Rabsolu_pos_lt l' H2);
- Clear H H0 H3 H4 H5 H7 H8 f g D l x0 x x1;Intro;
- Rewrite <-(Rmult_Or (Rplus R1 R1));
- Apply (Rlt_monotony (Rplus R1 R1) R0 (Rabsolu l'));Auto.
-Unfold Rgt in H6;Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H0).
-(**)
-Rewrite H2;Rewrite H2 in H0;Rewrite (Rmult_Or l);
- Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));Intros;
- Elim H4;Clear H4;Intros;
- Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H0 R1 H6);Intros;
- Elim H7;Clear H7;Intros;
- Cut (Rgt (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))) R0).
-Intro;Elim (H0 (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))) H9);
- Intros;Elim H10;Clear H10;Intros;Split with (Rmin (Rmin x x1) x2);
- Split.
-Elim (Rmin_Rgt (Rmin x x1) x2 R0);Intros;Elim (Rmin_Rgt x x1 R0);Intros;
- Generalize (H15 (conj (Rgt x R0) (Rgt x1 R0) H4 H7));Clear H14 H15;
- Intro;Clear H12;
- Apply (H13 (conj (Rgt (Rmin x x1) R0) (Rgt x2 R0) H14 H10)).
-Intros;Elim H12;Clear H12;Intros;
- Elim (Rmin_Rgt (Rmin x x1) x2 (R_dist x3 x0));Intros;Clear H15;
- Unfold 1 Rgt in H14;Elim (H14 H13);Clear H14;Intros;Unfold Rgt in H15;
- Clear H13;Elim (Rmin_Rgt x x1 (R_dist x3 x0));Intros;
- Elim (H13 H14);Clear H14 H13 H16;Intros;Unfold Rgt in H13 H14;
- Generalize (H5 x3 (conj (D x3) (Rlt (R_dist x3 x0) x) H12 H13));
- Generalize (H8 x3 (conj (D x3) (Rlt (R_dist x3 x0) x1) H12 H14));
- Generalize (H11 x3 (conj (D x3) (Rlt (R_dist x3 x0) x2) H12 H15));
- Clear H5 H8 H11 H15 H13 H14 H12;Intros;Unfold R_dist in H5 H8 H11;
- Unfold R_dist;Rewrite (minus_R0 (Rmult (f x3) (g x3)));
- Rewrite (minus_R0 (g x3)) in H8;Rewrite (minus_R0 (g x3)) in H5;
- Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x3) (g x3))) in H1);
- Rewrite <-(Rplus_Ropp_l (Rmult (g x3) l));Rewrite (Rmult_sym (g x3) l);
- Rewrite <-(Ropp_mul1 l (g x3));
- Rewrite (Rmult_sym (Ropp l) (g x3));
- Rewrite <-(Rplus_assoc (Rmult (f x3) (g x3))
- (Rmult (g x3) (Ropp l)) (Rmult l (g x3)));
- Rewrite (Rmult_sym (f x3) (g x3));
- Rewrite <-(Rmult_Rplus_distr (g x3) (f x3) (Ropp l));Fold (Rminus (f x3) l);
- Generalize (Rabsolu_triang (Rmult (g x3) (Rminus (f x3) l))
- (Rmult l (g x3)));Intro;
- Apply (Rle_lt_trans
- (Rabsolu (Rplus (Rmult (g x3) (Rminus (f x3) l)) (Rmult l (g x3))))
- (Rplus (Rabsolu (Rmult (g x3) (Rminus (f x3) l)))
- (Rabsolu (Rmult l (g x3)))) eps H12);Clear H12;
- Rewrite (Rabsolu_mult (g x3) (Rminus (f x3) l));
- Rewrite (Rabsolu_mult l (g x3));
- Elim (Req_EM (g x3) R0);Intros.
-Rewrite H12;Rewrite Rabsolu_R0;
- Rewrite (Rmult_Ol (Rabsolu (Rminus (f x3) l)));
- Rewrite (Rmult_Or (Rabsolu l));
- Rewrite (let (H1,H2)=(Rplus_ne R0) in H1);
- Unfold Rgt in H1;Assumption.
-Generalize (Rabsolu_pos_lt (g x3) H12);Intro;
- Fold (Rgt (Rabsolu (g x3)) R0) in H13;
- Generalize (Rmult_lt (Rabsolu (Rminus (f x3) l))
- (Rmult eps (Rinv (Rplus R1 R1)))
- (Rabsolu (g x3)) R1 H13 (eps2_Rgt_R0 eps H1)
- H11 H8);Intro;
- Generalize (Rlt_monotony (Rabsolu l) (Rabsolu (g x3))
- (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))))
- (Rabsolu_pos_lt l H3) H5);Clear H5 H8 H11 H12 H13;Intro;
- Rewrite (Rmult_sym (Rabsolu (Rminus (f x3) l)) (Rabsolu (g x3)))
- in H14;Generalize (Rplus_lt
- (Rmult (Rabsolu (g x3)) (Rabsolu (Rminus (f x3) l)))
- (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
- (Rmult (Rabsolu l) (Rabsolu (g x3)))
- (Rmult (Rabsolu l)
- (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))))) H14 H5);
- Clear H5 H14;Intro;
- Cut eps==(Rplus (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
- (Rmult (Rabsolu l)
- (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))))).
-Intro;Rewrite <-H8 in H5;Assumption.
-Rewrite (let (H1,H2)=
- (Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H1);
- Cut ~(Rabsolu l)==R0.
-Intro;Rewrite (Rinv_Rmult (Rplus R1 R1) (Rabsolu l));Auto.
-Rewrite (Rmult_sym (Rabsolu l)
- (Rmult eps (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l)))));
- Rewrite (Rmult_assoc eps
- (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l)))
- (Rabsolu l));
- Rewrite (Rmult_assoc (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l))
- (Rabsolu l));
- Rewrite (Rinv_l (Rabsolu l) H8);
- Rewrite (let (H1,H2)=
- (Rmult_ne (Rinv (Rplus R1 R1))) in H1);
- Apply sym_eqT;Apply eps2.
-Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H12;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H11 H12).
-Generalize (Rabsolu_pos_lt l H3);Intro;
- Apply (imp_not_Req (Rabsolu l) R0);Auto.
-Unfold Rgt;Unfold Rgt in H1;
- Rewrite <-(Rmult_Or (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))));
- Rewrite (Rmult_sym eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))));
- Apply (Rlt_monotony (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))) R0 eps);
- Auto.
-Apply (Rlt_Rinv (Rmult (Rplus R1 R1) (Rabsolu l)));
- Generalize (Rabsolu_pos_lt l H3);
- Clear H H0 H2 H4 H5 H7 H8 f g D l' x0 x x1;Intro;
- Rewrite <-(Rmult_Or (Rplus R1 R1));
- Apply (Rlt_monotony (Rplus R1 R1) R0 (Rabsolu l));Auto.
-Unfold Rgt in H6;Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H0).
-(**)
-Cut ~(Rplus (Rplus R1 R1) (Rplus R1 R1))==R0.
-Cut ~(Rabsolu l)==R0.
-Cut ~(Rabsolu l')==R0.
-Intros tl' tl add4;
- Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
- Intros;Elim H4;Clear H4;Intros;
- Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H0 R1 H6);Intros;
- Elim H7;Clear H7;Intros;
- Cut (Rgt (Rmult eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))) R0).
-Cut (Rgt (Rmult eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))) R0).
-Intros;Elim (H0 (Rmult eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))) H10);
- Intros;Elim H11;Clear H11;Intros;
- Elim (H (Rmult eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))) H9);
- Intros;Elim H13;Clear H13;Intros;
- Split with (Rmin (Rmin x x1) (Rmin x2 x3));Split.
-Elim (Rmin_Rgt (Rmin x x1) (Rmin x2 x3) R0);Intros;
- Elim (Rmin_Rgt x x1 R0);Elim (Rmin_Rgt x2 x3 R0);Intros;
- Apply (H16 (conj (Rgt (Rmin x x1) R0) (Rgt (Rmin x2 x3) R0)
- (H20 (conj (Rgt x R0) (Rgt x1 R0) H4 H7))
- (H18 (conj (Rgt x2 R0) (Rgt x3 R0) H11 H13)))).
-Intros;Elim H15;Clear H15;Intros;
- Elim (Rmin_Rgt (Rmin x x1) (Rmin x2 x3) (R_dist x4 x0));Intros;
- Clear H18;Unfold 1 Rgt in H17;Elim (H17 H16);Clear H17 H16;Intros;
- Elim (Rmin_Rgt x x1 (R_dist x4 x0));
- Elim (Rmin_Rgt x2 x3 (R_dist x4 x0));Intros;
- Unfold 1 Rgt in H17;Unfold 1 Rgt in H20;Elim (H18 H17);Elim (H20 H16);
- Clear H16 H17 H18 H19 H20 H21;Intros;Unfold Rgt in H16 H17 H18 H19;
- Generalize (H5 x4 (conj (D x4) (Rlt (R_dist x4 x0) x) H15 H16));
- Generalize (H8 x4 (conj (D x4) (Rlt (R_dist x4 x0) x1) H15 H17));
- Generalize (H12 x4 (conj (D x4) (Rlt (R_dist x4 x0) x2) H15 H18));
- Generalize (H14 x4 (conj (D x4) (Rlt (R_dist x4 x0) x3) H15 H19));
- Clear H H0 H5 H8 H12 H14 H16 H17 H18 H19;Intros;
- Unfold R_dist in H H0 H5 H8;Unfold R_dist;
- Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x4) (g x4))) in H1);
- Rewrite <-(Rplus_Ropp_l (Rmult (g x4) l));Rewrite (Rmult_sym (g x4) l);
- Rewrite <-(Ropp_mul1 l (g x4));
- Rewrite (Rmult_sym (Ropp l) (g x4));
- Rewrite <-(Rplus_assoc (Rmult (f x4) (g x4))
- (Rmult (g x4) (Ropp l)) (Rmult l (g x4)));
- Rewrite (Rmult_sym (f x4) (g x4));
- Rewrite <-(Rmult_Rplus_distr (g x4) (f x4) (Ropp l));Fold (Rminus (f x4) l);
- Unfold 1 Rminus;Rewrite (Rmult_sym l l');Rewrite <-(Ropp_mul1 l' l);
- Rewrite (Rmult_sym (Ropp l') l);
- Rewrite (Rplus_assoc (Rmult (g x4) (Rminus (f x4) l))
- (Rmult l (g x4)) (Rmult l (Ropp l')));
- Rewrite <-(Rmult_Rplus_distr l (g x4) (Ropp l'));
- Fold (Rminus (g x4) l');
- Generalize (Rabsolu_triang (Rmult (g x4) (Rminus (f x4) l))
- (Rmult l (Rminus (g x4) l')));Intro;
- Apply (Rle_lt_trans
- (Rabsolu (Rplus (Rmult (g x4) (Rminus (f x4) l))
- (Rmult l (Rminus (g x4) l'))))
- (Rplus (Rabsolu (Rmult (g x4) (Rminus (f x4) l)))
- (Rabsolu (Rmult l (Rminus (g x4) l')))) eps H12);Clear H12;
- Generalize (Rlt_monotony (Rabsolu l) (Rabsolu (Rminus (g x4) l'))
- (Rmult eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))))
- (Rabsolu_pos_lt l H3) H0);Intro;
- Generalize (Rlt_monotony (Rabsolu l') (Rabsolu (Rminus (f x4) l))
- (Rmult eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))))
- (Rabsolu_pos_lt l' H2) H);Intro;
- Elim (Req_EM (f x4) l);Intros.
-Rewrite H16;Rewrite (eq_Rminus l l (refl_eqT R l));
- Rewrite (Rmult_Or (g x4));Rewrite Rabsolu_R0;
- Rewrite (let (H1,H2)=(Rplus_ne (Rabsolu (Rmult l (Rminus (g x4) l'))))
- in H2);Rewrite (Rabsolu_mult l (Rminus (g x4) l'));
- Apply (Rlt_trans (Rmult (Rabsolu l) (Rabsolu (Rminus (g x4) l')))
- (Rmult (Rabsolu l)
- (Rmult eps
- (Rinv
- (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
- eps H12);
- Rewrite (Rmult_sym eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))));
- Rewrite <-(Rmult_assoc (Rabsolu l)
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))) eps);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l) add4
- tl);
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l)));
- Rewrite <-(Rmult_assoc (Rabsolu l) (Rinv (Rabsolu l))
- (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
- Rewrite (Rinv_r (Rabsolu l) tl);
- Rewrite (let (H1,H2)=(Rmult_ne (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
- in H2);Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- eps);Apply (Rlt_eps4_eps eps H1).
-Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;
- Cut (Rgt (Rabsolu (Rminus (f x4) l)) R0).
-Intro;
- Generalize (Rmult_lt (Rabsolu (Rminus (g x4) l')) R1
- (Rabsolu (Rminus (f x4) l))
- (Rmult eps (Rinv (Rplus R1 R1)))
- H18 H17 H5 H8);Intro;
- Rewrite (let (H1,H2)=(Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H2)
- in H19;Generalize (Rplus_lt (Rmult (Rabsolu (Rminus (g x4) l'))
- (Rabsolu (Rminus (f x4) l)))
- (Rmult eps (Rinv (Rplus R1 R1)))
- (Rmult (Rabsolu l') (Rabsolu (Rminus (f x4) l)))
- (Rmult (Rabsolu l')
- (Rmult eps (Rinv
- (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))))
- H19 H14);Intro;
- Generalize (Rplus_lt (Rmult (Rabsolu l) (Rabsolu (Rminus (g x4) l')))
- (Rmult (Rabsolu l)
- (Rmult eps
- (Rinv
- (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
- (Rplus
- (Rmult (Rabsolu (Rminus (g x4) l'))
- (Rabsolu (Rminus (f x4) l)))
- (Rmult (Rabsolu l') (Rabsolu (Rminus (f x4) l))))
- (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
- (Rmult (Rabsolu l')
- (Rmult eps
- (Rinv
- (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))))))
- H12 H20);
- Clear H5 H8 H12 H14 H19 H20 H H0 H9 H10;Replace (Rplus
- (Rmult (Rabsolu l)
- (Rmult eps
- (Rinv
- (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
- (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
- (Rmult (Rabsolu l')
- (Rmult eps
- (Rinv
- (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
- (Rabsolu l'))))))) with eps.
-Intro;Rewrite (Rplus_sym (Rabsolu (Rmult (g x4) (Rminus (f x4) l)))
- (Rabsolu (Rmult l (Rminus (g x4) l'))));
- Pattern 2 (g x4);
- Rewrite <-(let (H1,H2)=(Rplus_ne (g x4)) in H1);
- Rewrite <-(Rplus_Ropp_r l');Rewrite <-(Rplus_assoc (g x4) l' (Ropp l'));
- Rewrite (Rmult_sym (Rplus (Rplus (g x4) l') (Ropp l'))
- (Rminus (f x4) l));
- Rewrite (Rabsolu_mult (Rminus (f x4) l)
- (Rplus (Rplus (g x4) l') (Ropp l')));
- Rewrite (Rmult_sym (Rabsolu (Rminus (g x4) l'))
- (Rabsolu (Rminus (f x4) l))) in H;
- Rewrite (Rmult_sym (Rabsolu l')
- (Rabsolu (Rminus (f x4) l))) in H;
- Rewrite <-(Rmult_Rplus_distr (Rabsolu (Rminus (f x4) l))
- (Rabsolu (Rminus (g x4) l'))
- (Rabsolu l')) in H;
- Rewrite <-(Rabsolu_mult l (Rminus (g x4) l')) in H;
- Rewrite (Rplus_assoc (g x4) l' (Ropp l'));
- Rewrite (Rplus_sym l' (Ropp l'));
- Rewrite <-(Rplus_assoc (g x4) (Ropp l') l');
- Fold (Rminus (g x4) l');
- Generalize (Rabsolu_triang (Rminus (g x4) l') l');Intro;
- Unfold Rle in H0;Elim H0;Clear H0;Intro.
-Unfold Rgt in H18.
- Generalize (Rlt_monotony (Rabsolu (Rminus (f x4) l))
- (Rabsolu (Rplus (Rminus (g x4) l') l'))
- (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l'))
- H18 H0);Intro;
- Generalize (Rlt_compatibility (Rabsolu (Rmult l (Rminus (g x4) l')))
- (Rmult (Rabsolu (Rminus (f x4) l))
- (Rabsolu (Rplus (Rminus (g x4) l') l')))
- (Rmult (Rabsolu (Rminus (f x4) l))
- (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l')))
- H5);Clear H0 H5;Intro;
- Apply (Rlt_trans (Rplus (Rabsolu (Rmult l (Rminus (g x4) l')))
- (Rmult (Rabsolu (Rminus (f x4) l))
- (Rabsolu (Rplus (Rminus (g x4) l') l'))))
- (Rplus (Rabsolu (Rmult l (Rminus (g x4) l')))
- (Rmult (Rabsolu (Rminus (f x4) l))
- (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l'))))
- eps H0 H).
-Rewrite H0;Assumption.
-Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
- (Rabsolu l) add4 tl);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
- (Rabsolu l') add4 tl');
- Rewrite (Rmult_sym eps (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l))));
- Rewrite (Rmult_sym eps (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l'))));
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l)));
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l')));
- Rewrite (Rmult_assoc (Rinv (Rabsolu l))
- (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
- Rewrite (Rmult_assoc (Rinv (Rabsolu l'))
- (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
- Rewrite <-(Rmult_assoc (Rabsolu l) (Rinv (Rabsolu l))
- (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps));
- Rewrite <-(Rmult_assoc (Rabsolu l') (Rinv (Rabsolu l'))
- (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps));
- Rewrite (Rinv_r (Rabsolu l) tl);Rewrite (Rinv_r (Rabsolu l') tl');
- Rewrite (let (H1,H2)=(Rmult_ne
- (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps)) in H2);
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
- Rewrite (Rplus_sym (Rmult eps (Rinv (Rplus R1 R1)))
- (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))));
- Rewrite <- (Rplus_assoc
- (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
- (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
- (Rmult eps (Rinv (Rplus R1 R1))));
- Rewrite eps4;Rewrite eps2;Trivial.
-Unfold Rgt;Apply (Rabsolu_pos_lt (Rminus (f x4) l));Red;Intro;Elim H16;
- Apply (Rminus_eq (f x4) l H18).
-Apply (Rmult_gt eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))) H1);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')
- add4 tl');
- Apply (Rmult_gt (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l'))).
-Unfold Rgt;Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))).
-Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H9);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H9 H10);Intro;
- Clear H9 H10;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H9;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
- H11 H9).
-Unfold Rgt;Apply (Rlt_Rinv (Rabsolu l') (Rabsolu_pos_lt l' H2)).
-Apply (Rmult_gt eps
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))) H1);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)
- add4 tl);
- Apply (Rmult_gt (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
- (Rinv (Rabsolu l))).
-Unfold Rgt;Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))).
-Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H9);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H9 H10);Intro;
- Clear H9 H10;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H9;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
- H11 H9).
-Unfold Rgt;Apply (Rlt_Rinv (Rabsolu l) (Rabsolu_pos_lt l H3)).
-Generalize (Rabsolu_pos_lt l' H2);Intro;
- Apply (imp_not_Req (Rabsolu l') R0);Auto.
-Generalize (Rabsolu_pos_lt l H3);Intro;
- Apply (imp_not_Req (Rabsolu l) R0);Auto.
-Apply (imp_not_Req (Rplus (Rplus R1 R1) (Rplus R1 R1)) R0);Right;Unfold Rgt;
- Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H4);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H5;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H4 H5);Intro;
- Clear H4 H5;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H6);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H4;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
- H6 H4).
+Intros;Unfold limit1_in; Unfold limit_in; Simpl; Intros;
+ Elim (H (Rmin R1 (Rmult eps (mul_factor l l')))
+ (mul_factor_gt_f eps l l' H1));
+ Elim (H0 (Rmult eps (mul_factor l l')) (mul_factor_gt eps l l' H1));
+ Clear H H0; Simpl; Intros; Elim H; Elim H0; Clear H H0; Intros;
+ Split with (Rmin x1 x); Split.
+Exact (Rmin_Rgt_r x1 x R0 (conj ? ? H H2)).
+Intros; Elim H4; Clear H4; Intros;Unfold R_dist;
+ Replace (Rminus (Rmult (f x2) (g x2)) (Rmult l l')) with
+ (Rplus (Rmult (f x2) (Rminus (g x2) l')) (Rmult l' (Rminus (f x2) l))).
+Cut (Rlt (Rplus (Rabsolu (Rmult (f x2) (Rminus (g x2) l'))) (Rabsolu (Rmult l'
+ (Rminus (f x2) l)))) eps).
+Cut (Rle (Rabsolu (Rplus (Rmult (f x2) (Rminus (g x2) l')) (Rmult l' (Rminus
+ (f x2) l)))) (Rplus (Rabsolu (Rmult (f x2) (Rminus (g x2) l'))) (Rabsolu
+ (Rmult l' (Rminus (f x2) l))))).
+Exact (Rle_lt_trans ? ? ?).
+Exact (Rabsolu_triang ? ?).
+Rewrite (Rabsolu_mult (f x2) (Rminus (g x2) l'));
+ Rewrite (Rabsolu_mult l' (Rminus (f x2) l));
+ Cut (Rle (Rplus (Rmult (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l')))
+ (Rmult (Rabsolu l') (Rmult eps (mul_factor l l')))) eps).
+Cut (Rlt (Rplus (Rmult (Rabsolu (f x2)) (Rabsolu (Rminus (g x2) l'))) (Rmult
+ (Rabsolu l') (Rabsolu (Rminus (f x2) l)))) (Rplus (Rmult (Rplus R1 (Rabsolu
+ l)) (Rmult eps (mul_factor l l'))) (Rmult (Rabsolu l') (Rmult eps
+ (mul_factor l l'))))).
+Exact (Rlt_le_trans ? ? ?).
+Elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); Clear H5; Intros;
+ Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5));Intro;
+ Generalize (Rmin_Rgt_l ? ? ? H7);Intro;Elim H8;Intros;Clear H0 H8;
+ Apply Rplus_lt_le_lt.
+Apply Rmult_lt_0.
+Apply Rle_sym1.
+Exact (Rabsolu_pos (Rminus (g x2) l')).
+Rewrite (Rplus_sym R1 (Rabsolu l));Unfold Rgt;Apply Rlt_r_plus_R1;
+ Exact (Rabsolu_pos l).
+Unfold R_dist in H9;
+ Apply (Rlt_anti_compatibility (Ropp (Rabsolu l)) (Rabsolu (f x2))
+ (Rplus R1 (Rabsolu l))).
+Rewrite <- (Rplus_assoc (Ropp (Rabsolu l)) R1 (Rabsolu l));
+ Rewrite (Rplus_sym (Ropp (Rabsolu l)) R1);
+ Rewrite (Rplus_assoc R1 (Ropp (Rabsolu l)) (Rabsolu l));
+ Rewrite (Rplus_Ropp_l (Rabsolu l));
+ Rewrite (proj1 ? ? (Rplus_ne R1));
+ Rewrite (Rplus_sym (Ropp (Rabsolu l)) (Rabsolu (f x2)));
+ Generalize H9;
+Cut (Rle (Rminus (Rabsolu (f x2)) (Rabsolu l)) (Rabsolu (Rminus (f x2) l))).
+Exact (Rle_lt_trans ? ? ?).
+Exact (Rabsolu_triang_inv ? ?).
+Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));Trivial.
+Apply Rle_monotony.
+Exact (Rabsolu_pos l').
+Unfold Rle;Left;Assumption.
+Rewrite (Rmult_sym (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l')));
+ Rewrite (Rmult_sym (Rabsolu l') (Rmult eps (mul_factor l l')));
+ Rewrite <- (Rmult_Rplus_distr
+ (Rmult eps (mul_factor l l'))
+ (Rplus R1 (Rabsolu l))
+ (Rabsolu l'));
+ Rewrite (Rmult_assoc eps (mul_factor l l') (Rplus (Rplus R1 (Rabsolu l))
+ (Rabsolu l')));
+ Rewrite (Rplus_assoc R1 (Rabsolu l) (Rabsolu l'));Unfold mul_factor;
+ Rewrite (Rinv_l (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))
+ (mul_factor_wd l l'));
+ Rewrite (proj1 ? ? (Rmult_ne eps));Apply eq_Rle;Trivial.
+Ring.
Save.
(*********)
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
new file mode 100644
index 000000000..8e07739c3
--- /dev/null
+++ b/theories/Reals/Rsyntax.v
@@ -0,0 +1,182 @@
+(* $Id$ *)
+
+Require Export Rdefinitions.
+
+Axiom NRplus : R->R->R.
+
+Grammar rnatural ident :=
+ nat_id [ prim:var($id) ] -> [$id]
+
+with rnegnumber :=
+ neg_expr [ "-" rnumber ($c) ] -> [<<(Ropp $c)>>]
+
+with rnumber :=
+
+with rformula :=
+ form_expr [ rexpr($p) ] -> [$p]
+| form_eq [ rexpr($p) "==" rexpr($c) ] -> [<<(eqT R $p $c)>>]
+| form_le [ rexpr($p) "<=" rexpr($c) ] -> [<<(Rle $p $c)>>]
+| form_lt [ rexpr($p) "<" rexpr($c) ] -> [<<(Rlt $p $c)>>]
+| form_ge [ rexpr($p) ">=" rexpr($c) ] -> [<<(Rge $p $c)>>]
+| form_gt [ rexpr($p) ">" rexpr($c) ] -> [<<(Rgt $p $c)>>]
+| form_eq_eq [ rexpr($p) "==" rexpr($c) "==" rexpr($c1) ]
+ -> [<<(eqT R $p $c)/\(eqT R $c $c1)>>]
+| form_le_le [ rexpr($p) "<=" rexpr($c) "<=" rexpr($c1) ]
+ -> [<<(Rle $p $c)/\(Rle $c $c1)>>]
+| form_le_lt [ rexpr($p) "<=" rexpr($c) "<" rexpr($c1) ]
+ -> [<<(Rle $p $c)/\(Rlt $c $c1)>>]
+| form_lt_le [ rexpr($p) "<" rexpr($c) "<=" rexpr($c1) ]
+ -> [<<(Rlt $p $c)/\(Rle $c $c1)>>]
+| form_lt_lt [ rexpr($p) "<" rexpr($c) "<" rexpr($c1) ]
+ -> [<<(Rlt $p $c)/\(Rlt $c $c1)>>]
+| form_neq [ rexpr($p) "<>" rexpr($c) ] -> [<< ~(eqT R $p $c)>>]
+
+with rexpr :=
+ expr_plus [ rexpr($p) "+" rexpr($c) ] -> [<<(Rplus $p $c)>>]
+| expr_minus [ rexpr($p) "-" rexpr($c) ] -> [<<(Rminus $p $c)>>]
+| rexpr2 [ rexpr2($e) ] -> [$e]
+
+with rexpr2 :=
+ expr_mult [ rexpr2($p) "*" rexpr2($c) ] -> [<<(Rmult $p $c)>>]
+| rexpr0 [ rexpr0($e) ] -> [$e]
+
+
+with rexpr0 :=
+ expr_id [ constr:global($c) ] -> [$c]
+| expr_com [ "[" constr:constr($c) "]" ] -> [$c]
+| expr_appl [ "(" rapplication($a) ")" ] -> [$a]
+| expr_num [ rnumber($s) ] -> [$s ]
+| expr_negnum [ "-" rnegnumber($n) ] -> [ $n ]
+| expr_div [ rexpr0($p) "/" rexpr0($c) ] -> [<<(Rdiv $p $c)>>]
+| expr_opp [ "-" rexpr0($c) ] -> [<<(Ropp $c)>>]
+| expr_inv [ "1" "/" rexpr0($c) ] -> [<<(Rinv $c)>>]
+
+with rapplication :=
+ apply [ rapplication($p) rexpr($c1) ] -> [<<($p $c1)>>]
+| pair [ rexpr($p) "," rexpr($c) ] -> [<<($p, $c)>>]
+| appl0 [ rexpr($a) ] -> [$a].
+
+
+Grammar command command0 :=
+ r_in_com [ "``" rnatural:rformula($c) "``" ] -> [$c].
+
+Grammar command atomic_pattern :=
+ r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [$c].
+
+(** pp **)
+(* pb: on rajoute des () lorsque les constantes terminent par 1 lors de
+l'appel avec NRplus *)
+
+
+
+Syntax constr
+ level 0:
+ Rle [ (Rle $n1 $n2) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "<= " (REXPR $n2) "``"]]
+ | Rlt [ (Rlt $n1 $n2) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "< "(REXPR $n2) "``" ]]
+ | Rge [ (Rge $n1 $n2) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] ">= "(REXPR $n2) "``" ]]
+ | Rgt [ (Rgt $n1 $n2) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "> "(REXPR $n2) "``" ]]
+ | Req [ (eqT R $n1 $n2) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "== "(REXPR $n2)"``"]]
+ | Rneq [ ~(eqT R $n1 $n2) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "<> "(REXPR $n2) "``"]]
+ | Rle_Rle [ (Rle $n1 $n2)/\(Rle $n2 $n3) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "<= " (REXPR $n2)
+ [1 0] "<= " (REXPR $n3) "``"]]
+ | Rle_Rlt [ (Rle $n1 $n2)/\(Rlt $n2 $n3) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "<= "(REXPR $n2)
+ [1 0] "< " (REXPR $n3) "``"]]
+ | Rlt_Rle [ (Rlt $n1 $n2)/\(Rle $n2 $n3) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2)
+ [1 0] "<= " (REXPR $n3) "``"]]
+ | Rlt_Rlt [ (Rlt $n1 $n2)/\(Rlt $n2 $n3) ] ->
+ [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2)
+ [1 0] "< " (REXPR $n3) "``"]]
+ | Rzero [ R0 ] -> ["``0``"]
+ | Rone [ R1 ] -> ["``1``"]
+ | Rconst [(Rplus $r R1)] -> [$r:"r_printer"]
+ ;
+
+ level 7:
+ Rplus [ (Rplus $n1 $n2) ]
+ -> [ [<hov 0> "``"(REXPR $n1):E "+" [0 0] (REXPR $n2):L "``"] ]
+ | Rminus [ (Rminus $n1 $n2) ]
+ -> [ [<hov 0> "``"(REXPR $n1):E "-" [0 0] (REXPR $n2):L "``"] ]
+ ;
+
+ level 6:
+ Rmult [ (Rmult $n1 $n2) ]
+ -> [ [<hov 0> "``"(REXPR $n1):E "*" [0 0] (REXPR $n2):L "``"] ]
+ |Rdiv [ (Rdiv $n1 $n2) ]
+ -> [ [<hov 0> "``"(REXPR $n1):E "/" [0 0] (REXPR $n2):L "``"] ]
+ ;
+
+ level 8:
+ Ropp [(Ropp $n1)] -> [ [<hov 0> "``" "-"(REXPR $n1):E "``"] ]
+ |Rinv [(Rinv $n1)] -> [ [<hov 0> "``" "1""/"(REXPR $n1):E "``"] ]
+ ;
+
+ level 0:
+ rescape_inside [<< (REXPR $r) >>] -> [ "[" $r:E "]" ]
+ ;
+
+ level 4:
+ Rappl_inside [<<(REXPR (APPLIST $h ($LIST $t)))>>]
+ -> [ [<hov 0> "("(REXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E ")"] ]
+ | Rappl_inside_tail [<<(APPLINSIDETAIL $h ($LIST $t))>>]
+ -> [(REXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E]
+ | Rappl_inside_one [<<(APPLINSIDETAIL $e)>>] ->[(REXPR $e):E]
+ | rpair_inside [<<(REXPR <<(pair $s1 $s2 $r1 $r2)>>)>>]
+ -> [ [<hov 0> "("(REXPR $r1):E "," [1 0] (REXPR $r2):E ")"] ]
+ ;
+
+ level 3:
+ rvar_inside [<<(REXPR ($VAR $i))>>] -> [$i]
+ | rconst_inside [<<(REXPR (CONST $c))>>] -> [(CONST $c)]
+ | rmutind_inside [<<(REXPR (MUTIND $i $n))>>]
+ -> [(MUTIND $i $n)]
+ | rmutconstruct_inside [<<(REXPR (MUTCONSTRUCT $c1 $c2 $c3))>>]
+ -> [ (MUTCONSTRUCT $c1 $c2 $c3) ]
+ | rimplicit_head_inside [<<(REXPR (XTRA "!" $c))>>] -> [ $c ]
+ | rimplicit_arg_inside [<<(REXPR (XTRA "!" $n $c))>>] -> [ ]
+
+ ;
+
+
+ level 7:
+ Rplus_inside
+ [<<(REXPR <<(Rplus $n1 $n2)>>)>>]
+ -> [ (REXPR $n1):E "+" [0 0] (REXPR $n2):L ]
+ | Rminus_inside
+ [<<(REXPR <<(Rminus $n1 $n2)>>)>>]
+ -> [ (REXPR $n1):E "-" [0 0] (REXPR $n2):L ]
+ | NRplus_inside
+ [<<(REXPR <<(NRplus $n1 $n2)>>)>>]
+ -> ["(" (REXPR $n1):E "+" [0 0] (REXPR $n2):L ")"]
+ ;
+
+ level 6:
+ Rmult_inside
+ [<<(REXPR <<(Rmult $n1 $n2)>>)>>]
+ -> [ (REXPR $n1):E "*" [0 0] (REXPR $n2):L ]
+ |Rdiv_inside
+ [<<(REXPR <<(Rdiv $n1 $n2)>>)>>]
+ -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ]
+ ;
+
+ level 6:
+ Ropp_inside [<<(REXPR <<(Ropp $n1)>>)>>] -> [ "-" (REXPR $n1):E ]
+|Rinv_inside [<<(REXPR <<(Rinv $n1)>>)>>] -> [ "1""/" (REXPR $n1):E ]
+ ;
+
+ level 0:
+ Rzero_inside [<<(REXPR <<R0>>)>>] -> ["0"]
+ | Rone_inside [<<(REXPR <<R1>>)>>] -> ["1"]
+ | Rconst_inside [<<(REXPR <<(Rplus $r R1)>>)>>] -> [$r:"r_printer"].
+
+
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-02 02:00:21 +0000