From 0b69be40774bf7f75c8ed8a75c02998437ebbdbb Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 14 Oct 2007 15:56:00 +0000
Subject: [PATCH] Some lemmas moves to the file they belong to. Broken
 references to renamed errors fixed.

---
 matita/library/Q/Qaxioms.ma                   |   4 +-
 matita/library/algebra/finite_groups.ma       | 139 +-----------------
 matita/library/assembly/byte.ma               |   4 +-
 matita/library/assembly/exadecimal.ma         |   3 +-
 .../demo/propositional_sequent_calculus.ma    |  15 +-
 matita/library/nat/compare.ma                 |  49 +++++-
 matita/library/nat/ord.ma                     |   5 +-
 matita/library/nat/orders.ma                  |  75 ++++++++++
 matita/library/nat/relevant_equations.ma      |  10 ++
 9 files changed, 145 insertions(+), 159 deletions(-)

diff --git a/matita/library/Q/Qaxioms.ma b/matita/library/Q/Qaxioms.ma
index 6cf6b6994..da8e9e7a6 100644
--- a/matita/library/Q/Qaxioms.ma
+++ b/matita/library/Q/Qaxioms.ma
@@ -65,7 +65,7 @@ axiom frac_Qinv1: \forall a,b:nat.Qinv(frac a b) = frac b a.
 axiom frac_Qinv2: \forall a,b:nat.Qinv(frac (Zopp a) b) = frac (Zopp b) a.
 
 definition sigma_Q \def \lambda n,p,f.iter_p_gen n p Q f QO Qplus. 
-
+(*
 theorem geometric: \forall q.\exists k. 
 Qlt q (sigma_Q k (\lambda x.true) (\lambda x. frac (S O) x)).
-    
\ No newline at end of file
+*)  
\ No newline at end of file
diff --git a/matita/library/algebra/finite_groups.ma b/matita/library/algebra/finite_groups.ma
index 7f76ae0c8..0c7bd0b64 100644
--- a/matita/library/algebra/finite_groups.ma
+++ b/matita/library/algebra/finite_groups.ma
@@ -60,140 +60,6 @@ interpretation "Index_of_finite_enumerable representation"
 
 (* several definitions/theorems to be moved somewhere else *)
 
-definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
-
-theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
-intros;
-elim (le_to_or_lt_eq ? ? H1);
-[ assumption
-| elim (H H2)
-].
-qed.
-
-theorem ltb_to_Prop :
- ∀n,m.
-  match ltb n m with
-  [ true ⇒ n < m
-  | false ⇒ n ≮ m
-  ].
-intros;
-unfold ltb;
-apply leb_elim;
-apply eqb_elim;
-intros;
-simplify;
-[ rewrite < H;
-  apply le_to_not_lt;
-  constructor 1
-| apply (not_eq_to_le_to_lt ? ? H H1)
-| rewrite < H;
-  apply le_to_not_lt;
-  constructor 1
-| apply le_to_not_lt;
-  generalize in match (not_le_to_lt ? ? H1);
-  clear H1;
-  intro;
-  apply lt_to_le;
-  assumption
-].
-qed.
-
-theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
-(n < m → (P true)) → (n ≮ m → (P false)) →
-P (ltb n m).
-intros.
-cut
-(match (ltb n m) with
-[ true  ⇒ n < m
-| false ⇒ n ≮ m] → (P (ltb n m))).
-apply Hcut.apply ltb_to_Prop.
-elim (ltb n m).
-apply ((H H2)).
-apply ((H1 H2)).
-qed.
-
-theorem Not_lt_n_n: ∀n. n ≮ n.
-intro;
-unfold Not;
-intro;
-unfold lt in H;
-apply (not_le_Sn_n ? H).
-qed.
-
-theorem eq_pred_to_eq:
- ∀n,m. O < n → O < m → pred n = pred m → n = m.
-intros;
-generalize in match (eq_f ? ? S ? ? H2);
-intro;
-rewrite < S_pred in H3;
-rewrite < S_pred in H3;
-assumption.
-qed.
-
-theorem le_pred_to_le:
- ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
-intros 2;
-elim n;
-[ apply le_O_n
-| simplify in H2;
-  rewrite > (S_pred m);
-  [ apply le_S_S;
-    assumption
-  | assumption
-  ]
-].
-qed.
-
-theorem le_to_le_pred:
- ∀n,m. n ≤ m → pred n ≤ pred m.
-intros 2;
-elim n;
-[ simplify;
-  apply le_O_n
-| simplify;
-  generalize in match H1;
-  clear H1;
-  elim m;
-  [ elim (not_le_Sn_O ? H1)
-  | simplify;
-    apply le_S_S_to_le;
-    assumption
-  ]
-].
-qed.
-
-theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
-intros;
-unfold Not;
-intro;
-unfold lt in H;
-unfold lt in H1;
-generalize in match (le_S_S ? ? H);
-intro;
-generalize in match (transitive_le ? ? ? H2 H1);
-intro;
-apply (not_le_Sn_n ? H3).
-qed.
-
-
-
-(* moved to nat/order.ma 
-theorem lt_O_S: ∀n. O < S n.
-intro;
-unfold lt;
-apply le_S_S;
-apply le_O_n.
-qed. *)
-
-theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
-intros;
-unfold lt in H1;
-generalize in match (le_S_S_to_le ? ? H1);
-intro;
-apply cic:/matita/nat/orders/antisym_le.con;
-assumption.
-qed.
-
 theorem pigeonhole:
  ∀n:nat.∀f:nat→nat.
   (∀x,y.x≤n → y≤n → f x = f y → x=y) →
@@ -307,7 +173,7 @@ elim n;
             apply (ltb_elim (f (S n1)) (f a));
             [ simplify;
               intros;
-              generalize in match (lt_S_S ? ? H5);
+              generalize in match (lt_to_lt_S_S ? ? H5);
               intro;
               rewrite < S_pred in H6;
               [ elim (lt_n_m_to_not_lt_m_Sn ? ? H4 H6)
@@ -385,7 +251,8 @@ elim n;
       [ apply (H1 ? ? ? ? Hcut);
         apply le_S;
         assumption
-      | apply eq_pred_to_eq;
+      | alias id "eq_pred_to_eq" = "cic:/matita/nat/relevant_equations/eq_pred_to_eq.con".
+apply eq_pred_to_eq;
         [ apply (ltn_to_ltO ? ? H7)
         | apply (ltn_to_ltO ? ? H6)
         | assumption
diff --git a/matita/library/assembly/byte.ma b/matita/library/assembly/byte.ma
index f2d1dc156..2bf233ec1 100644
--- a/matita/library/assembly/byte.ma
+++ b/matita/library/assembly/byte.ma
@@ -283,9 +283,9 @@ lemma eq_bpred_S_a_a:
     rewrite > nat_of_exadecimal_exadecimal_of_nat in Hletin1;
     elim (eq_mod_O_to_exists ? ? Hletin1); clear Hletin1;
     rewrite > H1;
-    rewrite > div_times_ltO; [2: autobatch | ]
+    rewrite > lt_O_to_div_times; [2: autobatch | ]
     lapply (eq_f ? ? (λx.x/16) ? ? H1);
-    rewrite > div_times_ltO in Hletin; [2: autobatch | ]
+    rewrite > lt_O_to_div_times in Hletin; [2: autobatch | ]
     lapply (eq_f ? ? (λx.x \mod 16) ? ? H1);
     rewrite > eq_mod_times_n_m_m_O in Hletin1;
     elim daemon
diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma
index 761c06c94..c059b43fa 100644
--- a/matita/library/assembly/exadecimal.ma
+++ b/matita/library/assembly/exadecimal.ma
@@ -768,8 +768,7 @@ lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
  elim b;
  simplify;
  [
- |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
-   repeat (apply lt_S_S)
+ |*: repeat (apply lt_to_lt_S_S)
  ];
  autobatch.
 qed.
diff --git a/matita/library/demo/propositional_sequent_calculus.ma b/matita/library/demo/propositional_sequent_calculus.ma
index 9bd89394d..4498676a3 100644
--- a/matita/library/demo/propositional_sequent_calculus.ma
+++ b/matita/library/demo/propositional_sequent_calculus.ma
@@ -157,13 +157,13 @@ inductive derive: sequent → Prop ≝
  | NotL: ∀l1,l2,f.
     derive 〈l1,f::l2〉 → derive 〈FNot f :: l1,l2〉.
 
-alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
 let rec and_of_list l ≝
  match l with
-  [ Nil ⇒ FTrue
-  | Cons F l' ⇒ FAnd F (and_of_list l')
+  [ nil ⇒ FTrue
+  | cons F l' ⇒ FAnd F (and_of_list l')
   ].
 
+alias id "Nil" = "cic:/matita/list/list.ind#xpointer(1/1/1)".
 let rec or_of_list l ≝
  match l with
   [ Nil ⇒ FFalse
@@ -276,7 +276,6 @@ theorem soundness: ∀F. derive F → is_tautology (formula_of_sequent F).
 qed.
 
 alias num (instance 0) = "natural number".
-alias symbol "plus" = "natural plus".
 let rec size F ≝
  match F with
   [ FTrue ⇒ 0
@@ -289,8 +288,8 @@ let rec size F ≝
 
 let rec sizel l ≝
  match l with
-  [ Nil ⇒ 0
-  | Cons F l' ⇒ size F + sizel l'
+  [ nil ⇒ 0
+  | cons F l' ⇒ size F + sizel l'
   ].
 
 definition size_of_sequent ≝
@@ -311,8 +310,7 @@ definition same_atom : Formula → Formula → bool.
 qed.
 
 definition symmetricb ≝
- λA:Type.λeq:A → A → bool.
-  ∀x,y. eq x y = eq y x.
+ λA:Type.λeq:A → A → bool. ∀x,y. eq x y = eq y x.
 
 theorem symmetricb_eqb: symmetricb ? eqb.
  intro;
@@ -918,4 +916,3 @@ qed.
   | apply NotR;
     simplify in H1;
 *)
-*)
diff --git a/matita/library/nat/compare.ma b/matita/library/nat/compare.ma
index c701cd2e7..78dc50318 100644
--- a/matita/library/nat/compare.ma
+++ b/matita/library/nat/compare.ma
@@ -181,6 +181,50 @@ apply ((H1 H2)).
 qed.
 *)
 
+definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
+
+theorem ltb_to_Prop :
+ ∀n,m.
+  match ltb n m with
+  [ true ⇒ n < m
+  | false ⇒ n ≮ m
+  ].
+intros;
+unfold ltb;
+apply leb_elim;
+apply eqb_elim;
+intros;
+simplify;
+[ rewrite < H;
+  apply le_to_not_lt;
+  constructor 1
+| apply (not_eq_to_le_to_lt ? ? H H1)
+| rewrite < H;
+  apply le_to_not_lt;
+  constructor 1
+| apply le_to_not_lt;
+  generalize in match (not_le_to_lt ? ? H1);
+  clear H1;
+  intro;
+  apply lt_to_le;
+  assumption
+].
+qed.
+
+theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
+(n < m → (P true)) → (n ≮ m → (P false)) →
+P (ltb n m).
+intros.
+cut
+(match (ltb n m) with
+[ true  ⇒ n < m
+| false ⇒ n ≮ m] → (P (ltb n m))).
+apply Hcut.apply ltb_to_Prop.
+elim (ltb n m).
+apply ((H H2)).
+apply ((H1 H2)).
+qed.
+
 let rec nat_compare n m: compare \def
 match n with
 [ O \Rightarrow 
@@ -203,11 +247,6 @@ nat_compare n m = nat_compare (S n) (S m).
 intros.simplify.reflexivity.
 qed.
 
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
-apply eq_f.apply pred_Sn.
-qed.
-
 theorem nat_compare_pred_pred: 
 \forall n,m:nat.lt O n \to lt O m \to 
 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index 5895b3bcd..340e33a86 100644
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -166,8 +166,7 @@ apply p_ord_exp
   apply le_times_l.
   assumption.
   apply le_times_r.assumption.
-alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
-apply not_eq_to_le_to_lt.
+  apply not_eq_to_le_to_lt.
   unfold.intro.apply H1.
   rewrite < H3.
   apply (witness ? r r ?).simplify.apply plus_n_O.
@@ -456,4 +455,4 @@ theorem mod_p_ord_inv:
 intros.rewrite > eq_p_ord_inv.
 apply mod_plus_times.
 assumption.
-qed.
\ No newline at end of file
+qed.
diff --git a/matita/library/nat/orders.ma b/matita/library/nat/orders.ma
index 42454393c..caecbe063 100644
--- a/matita/library/nat/orders.ma
+++ b/matita/library/nat/orders.ma
@@ -130,6 +130,43 @@ apply nat_elim2
   ]
 qed.
 
+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
+apply eq_f.apply pred_Sn.
+qed.
+
+theorem le_pred_to_le:
+ ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
+intros 2;
+elim n;
+[ apply le_O_n
+| simplify in H2;
+  rewrite > (S_pred m);
+  [ apply le_S_S;
+    assumption
+  | assumption
+  ]
+].
+qed.
+
+theorem le_to_le_pred:
+ ∀n,m. n ≤ m → pred n ≤ pred m.
+intros 2;
+elim n;
+[ simplify;
+  apply le_O_n
+| simplify;
+  generalize in match H1;
+  clear H1;
+  elim m;
+  [ elim (not_le_Sn_O ? H1)
+  | simplify;
+    apply le_S_S_to_le;
+    assumption
+  ]
+].
+qed.
+
 (* le to lt or eq *)
 theorem le_to_or_lt_eq : \forall n,m:nat. 
 n \leq m \to n < m \lor n = m.
@@ -138,6 +175,14 @@ right.reflexivity.
 left.unfold lt.apply le_S_S.assumption.
 qed.
 
+theorem Not_lt_n_n: ∀n. n ≮ n.
+intro;
+unfold Not;
+intro;
+unfold lt in H;
+apply (not_le_Sn_n ? H).
+qed.
+
 (* not eq *)
 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
 unfold Not.intros.cut ((le (S n) m) \to False).
@@ -158,6 +203,19 @@ apply (lt_to_not_eq b b)
 ]
 qed.
 
+theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
+intros;
+unfold Not;
+intro;
+unfold lt in H;
+unfold lt in H1;
+generalize in match (le_S_S ? ? H);
+intro;
+generalize in match (transitive_le ? ? ? H2 H1);
+intro;
+apply (not_le_Sn_n ? H3).
+qed.
+
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
 simplify.intros.unfold lt in H.elim H.
@@ -197,6 +255,14 @@ apply lt_to_not_le.unfold lt.
 apply le_S_S.assumption.
 qed.
 
+theorem not_eq_to_le_to_lt: ∀n,m. n≠m → n≤m → n<m.
+intros;
+elim (le_to_or_lt_eq ? ? H1);
+[ assumption
+| elim (H H2)
+].
+qed.
+
 (* le elimination *)
 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 intro.elim n.reflexivity.
@@ -279,6 +345,15 @@ qed.
 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 \def antisymmetric_le.
 
+theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
+intros;
+unfold lt in H1;
+generalize in match (le_S_S_to_le ? ? H1);
+intro;
+apply antisym_le;
+assumption.
+qed.
+
 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 intros.
 apply (nat_elim2 (\lambda n,m.decidable (n \leq m))).
diff --git a/matita/library/nat/relevant_equations.ma b/matita/library/nat/relevant_equations.ma
index 9e275aa9c..6e6417080 100644
--- a/matita/library/nat/relevant_equations.ma
+++ b/matita/library/nat/relevant_equations.ma
@@ -50,3 +50,13 @@ rewrite > distr_times_plus.
 rewrite > distr_times_plus.
 rewrite < assoc_plus.reflexivity.
 qed.
+
+theorem eq_pred_to_eq:
+ ∀n,m. O < n → O < m → pred n = pred m → n = m.
+intros;
+generalize in match (eq_f ? ? S ? ? H2);
+intro;
+rewrite < S_pred in H3;
+rewrite < S_pred in H3;
+assumption.
+qed.
-- 
2.39.2