From db3104b6a36b957d7be4c79e50f22fd0ffd90f0d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 18:40:03 +0000
Subject: [PATCH] refactoring of some lemmas, shorter proofs

---
 helm/software/matita/dama/divisible_group.ma  |  8 +--
 helm/software/matita/dama/metric_lattice.ma   |  3 +-
 .../matita/dama/ordered_divisible_group.ma    | 14 ++---
 helm/software/matita/dama/ordered_group.ma    |  8 +++
 helm/software/matita/dama/sandwich.ma         | 52 ++++++++-----------
 5 files changed, 42 insertions(+), 43 deletions(-)

diff --git a/helm/software/matita/dama/divisible_group.ma b/helm/software/matita/dama/divisible_group.ma
index 7d2eeed45..44db35a15 100644
--- a/helm/software/matita/dama/divisible_group.ma
+++ b/helm/software/matita/dama/divisible_group.ma
@@ -41,7 +41,7 @@ intro G; cases G; unfold divide; intros (x n); simplify;
 cases (f x n); simplify; exact H;
 qed.  
   
-lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → n * x ≈ n * y.
+lemma feq_mul: ∀G:dgroup.∀x,y:G.∀n.x≈y → n * x ≈ n * y.
 intros (G x y n H); elim n; [apply eq_reflexive]
 simplify; apply (Eq≈ (x + (n1 * y)) H1);
 apply (Eq≈ (y+n1*y) H (eq_reflexive ??));
@@ -54,7 +54,7 @@ apply (ap_rewl ???? (plus_comm ???));
 apply (ap_rewl ???w (zero_neutral ??)); assumption;
 qed.
 
-lemma appow_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y.
+lemma apmul_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y.
 intros 4 (G x y n); elim n; [2:
   simplify in a;
   cases (applus ????? a); [assumption]
@@ -62,7 +62,7 @@ intros 4 (G x y n); elim n; [2:
 apply (plus_cancr_ap ??? 0); assumption;
 qed.
 
-lemma pluspow: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y.
+lemma plusmul: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y.
 intros (G x y n); elim n; [
   simplify; apply (Eq≈ 0 ? (zero_neutral ? 0)); apply eq_reflexive]
 simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [
@@ -78,7 +78,7 @@ simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [
 apply feq_plusl; apply eq_sym; assumption;
 qed. 
 
-lemma powzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G]
+lemma mulzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G]
 intros; elim n; [simplify; apply eq_reflexive]
 simplify; apply (Eq≈ ? (zero_neutral ??)); assumption; 
 qed.
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index cca643098..b5261b9dc 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -92,7 +92,8 @@ lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy
 apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
 apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
 apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z) (meq_l ????? Dxj));
-apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z)) (meq_r ????? Dyj));
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [
+  apply (feq_plusl ? (δ(x∧y) (y∧z)) ?? (meq_r ??? (x∨y) ? Dyj));]
 apply (Eq≈ ? (plus_comm ???));
 apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)) (meq_l ????? (join_comm ?x y)));
 apply feq_plusl;
diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma
index cae552114..a6c13e189 100644
--- a/helm/software/matita/dama/ordered_divisible_group.ma
+++ b/helm/software/matita/dama/ordered_divisible_group.ma
@@ -32,19 +32,19 @@ qed.
 
 coercion cic:/matita/ordered_divisible_group/todg_division.con.
 
-lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
+lemma mul_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
 intros (G x n); elim n; simplify; [apply le_reflexive]
 apply (le_transitive ???? H1); 
 apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??));
 apply fle_plusr; assumption;
 qed. 
 
-lemma lt_ltpow: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
+lemma lt_ltmul: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
 intros; elim n; [simplify; apply flt_plusr; assumption]
 simplify; apply (ltplus); [assumption] assumption;
 qed.
 
-lemma ltpow_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
+lemma ltmul_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
 intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
 simplify in l; cases (ltplus_orlt ????? l); [assumption]
 apply f; assumption;
@@ -53,16 +53,16 @@ qed.
 lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
 intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
 unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (ltpow_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
+apply (ltmul_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
 apply (lt_rewl ???? (zero_neutral ??)); 
 apply (lt_rewl ???? (zero_neutral ??)); 
-apply (lt_rewl ???? (powzero ?n1));
+apply (lt_rewl ???? (mulzero ?n1));
 assumption;
 qed.
 
-lemma poweqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+lemma muleqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
    0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
-intros (G x y n m H1 H2 H3); apply (ltpow_lt ??? n); apply (lt_rewr ???? H3);
+intros (G x y n m H1 H2 H3); apply (ltmul_lt ??? n); apply (lt_rewr ???? H3);
 clear H3; elim m; [
   rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+n*y))); [
     apply eq_sym; apply zero_neutral]
diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 9b70c4f62..e6b6f55ef 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -181,6 +181,14 @@ apply (lt_rewl ??? x (zero_neutral ??));
 assumption; 
 qed.
 
+lemma lt_opp_x_zero_to_lt_zero_x: 
+  ∀G:pogroup.∀x:G. -x < 0 → 0 < x.
+intros (G x Lx0); apply (plus_cancr_lt ??? (-x));
+apply (lt_rewl ??? (-x) (zero_neutral ??));
+apply (lt_rewr ??? (-x+x) (plus_comm ???));
+apply (lt_rewr ??? 0 (opp_inverse ??));
+assumption; 
+qed.
 
 lemma lt0plus_orlt: 
   ∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
index c83136c77..10b54b3e4 100644
--- a/helm/software/matita/dama/sandwich.ma
+++ b/helm/software/matita/dama/sandwich.ma
@@ -36,13 +36,13 @@ cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
 cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
 intro H3;
 cut (0<w1) as H4; [2: 
-  apply (ltpow_lt ??? 2); apply (lt_rewr ???? H2);
-  apply (lt_rewl ???? (powzero ? 3)); assumption]
+  apply (ltmul_lt ??? 2); apply (lt_rewr ???? H2);
+  apply (lt_rewl ???? (mulzero ? 3)); assumption]
 cut (0<w) as H5; [2:
-  apply (ltpow_lt ??? 3); apply (lt_rewr ???? H1);
-  apply (lt_rewl ???? (powzero ? 4)); assumption]
+  apply (ltmul_lt ??? 3); apply (lt_rewr ???? H1);
+  apply (lt_rewl ???? (mulzero ? 4)); assumption]
 cut (w<w1) as H6; [2: 
-  apply (poweqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
+  apply (muleqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
 apply (plus_cancr_lt ??? w1);
 apply (lt_rewl ??? (w+e)); [
   apply (Eq≈ (w+3*w1) ? H2);
@@ -77,47 +77,37 @@ constructor 1; [apply (n1 + n2);] intros (n3 Hn3);
 lapply (ltwr ??? Hn3) as Hn1n3; lapply (ltwl ??? Hn3) as Hn2n3;
 elim (H1 ? Hn1n3) (H3 H4); elim (H2 ? Hn2n3) (H5 H6); clear Hn1n3 Hn2n3;
 elim (H n3) (H7 H8); clear H H1 H2; 
-lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym;
+lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym; 
 (* the main step *)
-cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2:
+cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
   apply (le_transitive ???? (mtineq ???? (an n3)));
-  lapply (le_mtri ????? H7 H8);
-  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin);
-  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [2:
+  lapply (le_mtri ????? H7 H8) as H9;
+  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
+  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [2:
     apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
     apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
     apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??));
     apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
-    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear Hletin1;
-  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[
-    apply feq_plusr; apply msymmetric;]
-  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[
-    apply feq_plusr; assumption;]
-  clear Hcut Hletin Dym Dxm H8 H7 H6 H5 H4 H3;
-  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x));[
-    apply feq_plusr; apply plus_comm;]
+    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear H10;
+  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));    
+  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
+  clear Dym Dxm H8 H7 H6 H5 H4 H3;
+  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3))));
   apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
   apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
   apply lew_opp; [apply mpositive] apply fle_plusr;
   apply (le_rewr ???? (plus_comm ???));
   apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
   apply mtineq;]
-split; [
+split; [ (* first the trivial case *)
   apply (lt_le_transitive ????? (mpositive ????));
-  split; elim He; [apply  le_zero_x_to_le_opp_x_zero; assumption;]
-  cases t1; [ 
-    left; apply exc_zero_opp_x_to_exc_x_zero;
-    apply (Ex≫ ? (eq_opp_opp_x_x ??));assumption;]
-  right;  apply exc_opp_x_zero_to_exc_zero_x;
-  apply (Ex≪ ? (eq_opp_opp_x_x ??)); assumption;]
-clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2;
+  apply lt_zero_x_to_lt_opp_x_zero; assumption;]  
+clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2; cases H4 (H7 H8); clear H4;
 apply (le_lt_transitive ???? ? (sandwich_ineq ?? He));
-apply (le_transitive ???? Hcut);
+apply (le_transitive ???? main_ineq);
 apply (le_transitive ??  (e/3+ δ(an n3) x+ δ(an n3) x)); [
   repeat apply fle_plusr; cases H6; assumption;]
-apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x)); [
-  apply fle_plusr; apply fle_plusl; cases H4; assumption;]
-apply (le_transitive ??  (e/3+ e/2 + e/2)); [
-  apply fle_plusl; cases H4; assumption;]
+apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x) ); [apply fle_plusr; apply fle_plusl; assumption]
+apply (le_transitive ??  (e/3+ e/2 + e/2)); [apply fle_plusl; assumption;]
 apply le_reflexive;
 qed.
-- 
2.39.2