X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FR%2Fr.ma;h=d47a1dc58bd18c0dbf472e35bc2e40d2a78717cc;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;hp=46a4e416bd6bcf96f439f9693bee525088c99cde;hpb=10dbebadd2931de5b93871a6b4989e07f668e166;p=helm.git

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index 46a4e416b..d47a1dc58 100644
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -58,8 +58,10 @@ axiom assoc_Rtimes : ∀x,y,z:R.(x*y)*z = x*(y*z).
 axiom Rtimes_x_R1 : ∀x.x * R1 = x.
 axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z.
 
+pump 200.
+
 lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
-intros;autobatch paramodulation;
+intros; demodulate all. (*autobatch paramodulation;*)
 qed.
 
 (* commutative field *)
@@ -201,15 +203,18 @@ intros;autobatch paramodulation;
 qed. *)
 
 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro;
+intro; demodulate all.
+(*
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
 rewrite < assoc_Rplus;
 apply eq_f2;autobatch paramodulation;
+*)
 qed.
 
 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro.
+intro. demodulate all. (*
+auto paramodulation.
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
 rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
@@ -219,6 +224,7 @@ rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?);
 apply eq_f2 [reflexivity]
 rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
 rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
+*)
 qed.
 
 lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
@@ -235,24 +241,24 @@ apply eq_Rtimes_l_to_r
 |apply Rinv_Rtimes_l;assumption] 
 qed.
 
-lemma Ropp_R0 : R0 = - R0.
-rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation;
+lemma Ropp_R0 : R0 = - R0. demodulate all. (*
+rewrite < eq_Rtimes_Ropp_R1_Ropp;autobatch paramodulation; *)
 qed.
 
 lemma distr_Ropp_Rplus : ∀x,y:R.-(x + y) = -x -y.
-intros;rewrite < eq_Rtimes_Ropp_R1_Ropp;
+intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp;
 rewrite > sym_Rtimes;rewrite > distr_Rtimes_Rplus_l;
-autobatch paramodulation;
+autobatch paramodulation;*)
 qed.
 
 lemma Ropp_Rtimes_l : ∀x,y:R.-(x*y) = -x*y.
-intros;rewrite < eq_Rtimes_Ropp_R1_Ropp;
-rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation;
+intros; demodulate all; (*rewrite < eq_Rtimes_Ropp_R1_Ropp;
+rewrite > sym_Rtimes;rewrite < assoc_Rtimes;autobatch paramodulation;*)
 qed.
 
 lemma Ropp_Rtimes_r : ∀x,y:R.-(x*y) = x*-y.
-intros;rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%);
-autobatch;
+intros; demodulate all; (*rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (???%);
+autobatch;*)
 qed.
 
 (* less than *)
@@ -284,11 +290,11 @@ qed.
 lemma pos_z_to_le_Rtimes_Rtimes_to_lt : ∀x,y,z.R0 < z → z*x ≤ z*y → x ≤ y.
 intros;cases H1
 [left;autobatch
-|right;rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%);
+|right; rewrite < Rtimes_x_R1;rewrite < Rtimes_x_R1 in ⊢ (???%);
  rewrite < sym_Rtimes;rewrite < sym_Rtimes in ⊢ (???%);
  rewrite < (Rinv_Rtimes_l z)
- [rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?));
-  autobatch paramodulation
+ [demodulate all; (*rewrite < sym_Rtimes in ⊢ (??(?%?)?);rewrite < sym_Rtimes in ⊢ (???(?%?));
+  autobatch paramodulation*)
  |intro;rewrite > H3 in H;apply (irrefl_Rlt R0);assumption]] 
 qed.
 
@@ -297,7 +303,8 @@ intros;rewrite > Ropp_inv in ⊢ (?%?);
 rewrite > Ropp_inv in ⊢ (??%);
 apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z))
 [rewrite > Ropp_R0;autobatch
-|rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?);
+|applyS H1; (*
+ rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (?(??%)?);
  rewrite < (eq_Rtimes_Ropp_R1_Ropp) in ⊢ (??(??%));
  do 2 rewrite < assoc_Rtimes;
  rewrite > eq_Rtimes_Ropp_R1_Ropp;
@@ -309,7 +316,7 @@ apply Rlt_to_Rlt_Ropp_Ropp;apply (pos_z_to_lt_Rtimes_Rtimes_to_lt ?? (-z))
  rewrite > eq_Rtimes_Ropp_R1_Ropp;
  rewrite < Ropp_inv;
  rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
- assumption]
+ assumption*)]
 qed.
 
 lemma lt_R0_Rinv : ∀x.R0 < x → R0 < Rinv x.
@@ -335,27 +342,37 @@ qed.
 lemma lt_Rinv : ∀x,y.R0 < x → x < y → Rinv y < Rinv x.
 intros;
 lapply (Rlt_times_l ? ? (Rinv x * Rinv y) H1)
-[rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
+[ lapply (Rinv_Rtimes_l x);[2: intro; destruct H2; autobatch;]
+  lapply (Rinv_Rtimes_l y);[2: intro; destruct H2; autobatch;]
+  cut ((x \sup -1/y*x<x \sup -1/y*y) = (y^-1 < x ^-1));[2:
+    demodulate all;]
+  rewrite < Hcut; assumption;
+ (*
+ rewrite > sym_Rtimes in Hletin;rewrite < assoc_Rtimes in Hletin;
  rewrite > assoc_Rtimes in Hletin:(??%);
  rewrite > sym_Rtimes in Hletin:(??(??%));
  rewrite > Rinv_Rtimes_l in Hletin
  [rewrite > Rinv_Rtimes_l in Hletin
-  [rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin;
-   rewrite > Rtimes_x_R1 in Hletin;assumption
+  [applyS Hletin;(*rewrite > Rtimes_x_R1 in Hletin;rewrite > sym_Rtimes in Hletin;
+   rewrite > Rtimes_x_R1 in Hletin;assumption*)
   |intro;rewrite > H2 in H1;apply (asym_Rlt ? ? H H1)]
- |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)]
+ |intro;rewrite > H2 in H;apply (irrefl_Rlt ? H)]*)
 |apply pos_times_pos_pos;apply lt_R0_Rinv;autobatch]
 qed.
 
 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros;rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
+intros; lapply (Rlt_plus_l ?? (-b) H); applyS Hletin;
+(*
+rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 rewrite < assoc_Rplus;
 rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
 apply Rlt_plus_l;assumption;
+*)
 qed.
 
 lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.
-intros;rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%);
+intros;
+rewrite > Ropp_inv;rewrite > Ropp_inv in ⊢ (??%);
 apply Rlt_to_Rlt_Ropp_Ropp;rewrite > distr_Ropp_Rplus;
 apply Rlt_plus_l_to_r;rewrite < distr_Ropp_Rplus;apply Rlt_to_Rlt_Ropp_Ropp;
 assumption;