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.*)
+pump 40.
+
lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
-intros;autobatch paramodulation;
+intros; autobatch;
qed.
(* commutative field *)
lemma trans_Rle : ∀x,y,z:R.x ≤ y → y ≤ z → x ≤ z.
intros;cases H
-[cases H1
+[cases H1; unfold; autobatch;
+|autobatch;]
+(*
[left;autobatch
|rewrite < H3;assumption]
-|rewrite > H2;assumption]
+|rewrite > H2;assumption]*)
qed.
-axiom Rlt_plus_l : ∀x,y,z:R.x < y → z + x < z + y.
-axiom Rlt_times_l : ∀x,y,z:R.x < y → R0 < z → z*x < z*y.
+axiom Rlt_plus_l : ∀z,x,y:R.x < y → z + x < z + y.
+axiom Rlt_times_l : ∀z,x,y:R.x < y → R0 < z → z*x < z*y.
(* FIXME: these should be lemmata *)
-axiom Rle_plus_l : ∀x,y,z:R.x ≤ y → z + x ≤ z + y.
-axiom Rle_times_l : ∀x,y,z:R.x ≤ y → R0 < z → z*x ≤ z*y.
+axiom Rle_plus_l : ∀z,x,y:R.x ≤ y → z + x ≤ z + y.
+axiom Rle_times_l : ∀z,x,y:R.x ≤ y → R0 < z → z*x ≤ z*y.
-lemma Rle_plus_r : ∀x,y,z:R.x ≤ y → x + z ≤ y + z.
-intros;
-rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%);
-autobatch;
+lemma Rle_plus_r : ∀z,x,y:R.x ≤ y → x + z ≤ y + z.
+intros; autobatch.
qed.
-lemma Rle_times_r : ∀x,y,z:R.x ≤ y → R0 < z → x*z ≤ y*z.
+lemma Rle_times_r : ∀z,x,y:R.x ≤ y → R0 < z → x*z ≤ y*z.
intros;
-rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%);
+(* rewrite > sym_Rtimes;rewrite > sym_Rtimes in ⊢ (??%); *)
autobatch;
qed.
qed. *)
lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro;
+(*intro; autobatch paramodulation.*)
+intros;
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. (*autobatch paramodulation.*)
+
rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
rewrite < (Rplus_Ropp x) 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).
|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 *)
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.
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;
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.
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 (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
+[ 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:autobatch
+(* end auto($Revision: 9716 $) proof: TIME=2.24 SIZE=100 DEPTH=100 *) ;]
+ 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;
+autobatch by H, (Rlt_plus_l (-b) (a+b) c);
+(*
+rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
rewrite < assoc_Rplus;
rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
-apply Rlt_plus_l;assumption;
+apply (Rlt_plus_l (-b) (a+b) c);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;