From 35e633b9f0e0ae36641e0f6d29aaed7ceb4e3c75 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 23 Aug 2012 17:15:24 +0000
Subject: [PATCH] we updated the contribution porting it to the new matita ...

---
 matita/matita/contribs/character/Makefile     |  18 ---
 .../contribs/character/classes/class.ma       |  95 ++++++++++++++++
 .../contribs/character/classes/class_pt.ma    |  74 ++++++++++++
 .../contribs/character/classes/props_pt.ma    | 107 ------------------
 .../character/classes/{defs.ma => triple.ma}  |  41 ++++---
 matita/matita/contribs/character/depends      |   5 -
 matita/matita/contribs/character/preamble.ma  |  93 ++++++---------
 7 files changed, 231 insertions(+), 202 deletions(-)
 delete mode 100644 matita/matita/contribs/character/Makefile
 create mode 100644 matita/matita/contribs/character/classes/class.ma
 create mode 100644 matita/matita/contribs/character/classes/class_pt.ma
 delete mode 100644 matita/matita/contribs/character/classes/props_pt.ma
 rename matita/matita/contribs/character/classes/{defs.ma => triple.ma} (53%)
 delete mode 100644 matita/matita/contribs/character/depends

diff --git a/matita/matita/contribs/character/Makefile b/matita/matita/contribs/character/Makefile
deleted file mode 100644
index 8262cd704..000000000
--- a/matita/matita/contribs/character/Makefile
+++ /dev/null
@@ -1,18 +0,0 @@
-BIN=../../
-
-DIR=$(shell basename $$PWD)
-
-H=@
-
-$(DIR) all:
-	$(H)$(BIN)matitac
-$(DIR).opt opt all.opt:
-	$(H)$(BIN)matitac.opt
-clean:
-	$(H)$(BIN)matitaclean
-clean.opt:
-	$(H)$(BIN)matitaclean.opt
-depend:
-	$(H)$(BIN)matitadep
-depend.opt:
-	$(H)$(BIN)matitadep.opt
diff --git a/matita/matita/contribs/character/classes/class.ma b/matita/matita/contribs/character/classes/class.ma
new file mode 100644
index 000000000..3cc8d08a7
--- /dev/null
+++ b/matita/matita/contribs/character/classes/class.ma
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* ?: MATITA SOURCE FILES
+ * Suggested invocation to start formal specifications with:
+ *   - Patience on me to gain peace and perfection! -
+ * 2008 September 22:
+ *   specification starts.
+ *)
+
+include "preamble.ma".
+
+(* CHARACTER CLASSES ********************************************************)
+
+(* Note: OEIS sequence identifiers 
+   P(n): A016777 "3n+1"
+   T(n): A155504 "(3h+1)*3^(k+1)"
+*)
+
+inductive P: predicate nat ≝
+   | p1: P 1
+   | p2: ∀i,j. T i → P j → P (i + j)
+with T: predicate nat ≝
+   | t1: ∀i. P i → T (i * 3)
+   | t2: ∀i. T i → T (i * 3)
+.
+
+inductive S: predicate nat ≝
+   | s1: ∀i. P i → S (i * 2)
+   | s2: ∀i. T i → S (i * 2)
+.
+
+inductive Q: predicate nat ≝
+   | q1: ∀i. P i → Q (i * 2 + 3)
+   | q2: ∀i. Q i → Q (i * 3)
+.
+
+(* Basic eliminators ********************************************************)
+
+axiom p_ind: ∀R:predicate nat. R 1 →
+             (∀i,j. T i → R j → R (i + j)) →
+             ∀j. P j → R j.
+
+axiom t_ind: ∀R:predicate nat.
+             (∀i. P i → R (i * 3)) →
+             (∀i. R i → R (i * 3)) →
+             ∀i. T i → R i.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact p_inv_O_aux: ∀i. P i → i = 0 → False.
+#i #H @(p_ind … H) -i
+[ #H destruct
+| #i #j #_ #IH #H 
+  elim (plus_inv_O3 … H) -H /2 width=1/
+]
+qed-.
+
+lemma p_inv_O: P 0 → False.
+/2 width=3 by p_inv_O_aux/ qed-.
+
+fact t_inv_O_aux: ∀i. T i → i = 0 → False.
+#i #H @(t_ind … H) -i #i #IH #H
+lapply (times_inv_S2_O3 … H) -H /2 width=1/
+/2 width=3 by p_inv_O_aux/
+qed-.
+
+lemma t_inv_O: T 0 → False.
+/2 width=3 by t_inv_O_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma t_3: T 3.
+/2 width=1/ qed.
+
+lemma p_pos: ∀i. P i → ∃k. i = k + 1.
+* /2 width=2/
+#H elim (p_inv_O … H) 
+qed.
+
+lemma t_pos: ∀i. T i → ∃k. i = k + 1.
+* /2 width=2/
+#H elim (t_inv_O … H) 
+qed.
diff --git a/matita/matita/contribs/character/classes/class_pt.ma b/matita/matita/contribs/character/classes/class_pt.ma
new file mode 100644
index 000000000..2533674df
--- /dev/null
+++ b/matita/matita/contribs/character/classes/class_pt.ma
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "classes/class.ma".
+
+(* CHARACTER CLASSES ********************************************************)
+
+(* Arithmetics of classes P and T *******************************************)
+
+lemma pt_inv_gen: ∀i.
+                  (P i → ∃h. i = h * 3 + 1) ∧
+                  (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
+#i @(nat_elim1 … i) -i #i #IH
+@conj #H
+[ inversion H -H
+  [ #H destruct /2 width=2/
+  | #i0 #j0 #Hi0 #Hj0 #H destruct
+    elim (t_pos … Hi0) #i #H destruct
+    elim (p_pos … Hj0) #j #H destruct
+    elim (IH (i+1) ?) // #_ #H
+    elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
+    elim (IH (j+1) ?) -IH // #H #_ -i
+    elim (H Hj0) -H -Hj0 #hj #H >H -j
+    <associative_plus >exp_n_m_plus_1 /2 width=2/
+  ]
+| @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
+  [ elim (p_pos … Hi0) #i #H destruct
+    elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
+    elim (H Hi0) -H -Hi0 #hi #H >H -i
+    @(ex1_2_intro … hi 0) //
+  | elim (t_pos … Hi0) #i #H destruct
+    elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
+    elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
+    >associative_times <exp_n_m_plus_1 /2 width=3/
+  ]
+]
+qed-.
+
+theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
+#i #Hi elim (pt_inv_gen i) /2 width=1/
+qed-.
+
+theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
+#i #Hi elim (pt_inv_gen i) /2 width=1/
+qed-.
+
+theorem p_gen: ∀i. P (i * 3 + 1).
+#i @(nat_ind_plus … i) -i //
+#i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
+qed.
+
+theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
+#i #j @(nat_ind_plus … j) -j /2 width=1/
+#j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
+qed.
+
+lemma pt_discr: ∀i. P i → T i → False.
+#i #Hp #Ht
+elim (p_inv_gen … Hp) -Hp #hp #Hp
+elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
+>exp_n_m_plus_1 in Ht; <associative_times #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
diff --git a/matita/matita/contribs/character/classes/props_pt.ma b/matita/matita/contribs/character/classes/props_pt.ma
deleted file mode 100644
index 58fbaf300..000000000
--- a/matita/matita/contribs/character/classes/props_pt.ma
+++ /dev/null
@@ -1,107 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "classes/defs.ma".
-
-theorem p_inv_O: P 0 → False.
- intros; inversion H;intros;
- [apply (not_eq_O_S ? H1)
- |autobatch.
- ]
-qed.
-
-theorem t_inv_O: T 0 → False.
- intros; inversion H; clear H; intros;
- [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
- | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
- ].
-qed.
-
-theorem p_pos: ∀i. P i → ∃k. i = S k.
- intros 1; elim i 0; clear i; intros;
- [ lapply linear p_inv_O to H; decompose
- | autobatch depth = 2
- ].
-qed.
-
-theorem t_pos: ∀i. T i → ∃k. i = S k.
- intros 1; elim i names 0; clear i; intros;
- [ lapply linear t_inv_O to H; decompose
- | autobatch depth = 2
- ].
-qed.
-
-theorem t_1: T 1 → False.
- intros; inversion H; clear H; intros;
- [ lapply not_3_divides_1 to H1; decompose
- | lapply not_3_divides_1 to H2; decompose
- ].
-qed.
-
-theorem t_3: T 3.
- change in ⊢ (? %) with (1 * 3);
- autobatch depth = 2.
-qed.
-
-theorem pt_inv_gen: ∀i. 
-                    (P i → ∃h. i = S (h * 3)) ∧
-                    (T i → ∃h,k. i = S (h * 3) * 3 \sup (S k)).
- intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
- [ lapply linear p_inv_O to H; decompose
- | lapply linear t_inv_O to H; decompose
- | inversion H1; clear H1; intros;
-   [ destruct; autobatch paramodulation
-   | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
-     lapply linear plus_inv_S_S_S to H4; decompose;
-     lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
-     lapply linear H to H2; lapply linear H5 to H1; decompose;
-     rewrite > H; rewrite > H2; clear H H2;
-     rewrite < plus_n_Sm; rewrite > times_exp_x_y_Sz; autobatch depth = 2
-   ]
- | inversion H1; clear H1; intros;
-   [ lapply linear times_inv_S_m_SS to H2 as H0;
-     lapply linear H to H0; decompose; clear H2;
-     lapply linear H to H1; decompose; destruct;
-     autobatch depth = 4
-   | clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
-     lapply linear H to H0; decompose; clear H;
-     lapply linear H2 to H1; decompose; destruct;
-     autobatch depth = 4
-   ]
- ].
-qed.
-
-theorem p_inv_gen: ∀i. P i → ∃h. i = S (h * 3).
- intros; lapply depth = 1 pt_inv_gen; decompose;
- lapply linear H1 to H as H0; autobatch depth = 1.
-qed.
-
-theorem t_inv_gen: ∀i. T i → ∃h,k. i = (S (h * 3)) * 3 \sup (S k).
- intros; lapply depth = 1 pt_inv_gen; decompose;
- lapply linear H2 to H as H0; autobatch depth = 2.
-qed.
-
-theorem p_gen: ∀i. P (S (i * 3)).
- intros; elim i names 0; clear i; intros;
- [ simplify; autobatch depth = 2
- | rewrite > plus_3_S3n ; autobatch depth = 2
- ].
-qed.
-
-theorem t_gen: ∀i,j. T (S (i * 3) * 3 \sup (S j)).
- intros; elim j names 0; clear j; intros;
- [ simplify in ⊢ (? (? ? %)); autobatch depth = 2
- | rewrite > times_exp_x_y_Sz; autobatch depth = 2
- ].
-qed.
diff --git a/matita/matita/contribs/character/classes/defs.ma b/matita/matita/contribs/character/classes/triple.ma
similarity index 53%
rename from matita/matita/contribs/character/classes/defs.ma
rename to matita/matita/contribs/character/classes/triple.ma
index 8283373db..6b85df2a0 100644
--- a/matita/matita/contribs/character/classes/defs.ma
+++ b/matita/matita/contribs/character/classes/triple.ma
@@ -12,22 +12,31 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "preamble.ma".
+include "classes/class_pt.ma".
 
-(* NOTE: OEIS sequence identifiers 
-   P(n): A016777 "3n+1"
-   T(n): A155504 "(3h+1)*3^(k+1)"
-*)
+(* TRIPLES OF CHARACTER CLASSES *********************************************)
 
-inductive P: nat → Prop ≝
-   | p1: P 1
-   | p2: ∀i,j. T i → P j → P (i + j)
-with T: nat → Prop ≝
-   | t1: ∀i. P i → T (i * 3)
-   | t2: ∀i. T i → T (i * 3)
-.
+lemma not_p_pS: ∀i. P i → P (i + 1) → False.
+#i #Hi #HSi
+elim (p_inv_gen … Hi) -Hi #hi #Hi
+elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
+lapply (injective_plus_l … HSi) -HSi #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
 
-inductive S: nat → Prop ≝
-   | s1: ∀i. P i → S (i * 2)
-   | s2: ∀i. T i → S (i * 2)
-.
+lemma not_p_pSS: ∀i. P i → P (i + 2) → False.
+#i #Hi #HSi
+elim (p_inv_gen … Hi) -Hi #hi #Hi
+elim (p_inv_gen … HSi) -HSi #hSi #HSi destruct
+>plus_plus_comm_23 in HSi; #H
+lapply (injective_plus_l … H) -H #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
+
+lemma not_p_tS: ∀i. P i → T (i + 1) → False.
+#i #Hp #Ht
+elim (p_inv_gen … Hp) -Hp #hp #Hp
+elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
+>exp_n_m_plus_1 in Ht; <associative_times >associative_plus #H
+elim (not_b_divides_nbr … H) -H //
+qed-.
diff --git a/matita/matita/contribs/character/depends b/matita/matita/contribs/character/depends
deleted file mode 100644
index 7079205b1..000000000
--- a/matita/matita/contribs/character/depends
+++ /dev/null
@@ -1,5 +0,0 @@
-preamble.ma nat/exp.ma nat/relevant_equations.ma
-classes/defs.ma preamble.ma
-classes/props_pt.ma classes/defs.ma
-nat/exp.ma 
-nat/relevant_equations.ma 
diff --git a/matita/matita/contribs/character/preamble.ma b/matita/matita/contribs/character/preamble.ma
index e2656f6c2..8d674d3e9 100644
--- a/matita/matita/contribs/character/preamble.ma
+++ b/matita/matita/contribs/character/preamble.ma
@@ -12,65 +12,46 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "nat/exp.ma".
-include "nat/relevant_equations.ma".
+include "arithmetics/exp.ma".
+include "../lambda_delta/ground_2/arith.ma".
 
-alias num (instance 0) = "natural number".
+lemma plus_inv_O3: ∀m,n. n + m = 0 → n = 0 ∧ m = 0.
+#m * /2 width=1/ normalize
+#n #H destruct
+qed-.
 
-theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
- intros 2; elim n names 0; clear n; simplify; intros;
- [ autobatch | destruct ].
-qed. 
+lemma times_inv_S2_O3: ∀m,n. n * (S m) = 0 → n = 0.
+#m #n <times_n_Sm #H
+elim (plus_inv_O3 … H) -H //
+qed-. 
 
-theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
- intros; rewrite < times_n_Sm in H;
- lapply linear plus_inv_O3 to H; decompose;autobatch.
-qed. 
+lemma exp_n_m_plus_1: ∀n,m. n ^ (m + 1) = (n ^ m) * n.
+// qed.
 
-theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
- intros 1; rewrite > sym_times; simplify;
- elim n names 0; simplify; intros; destruct;
- rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
+lemma times_n_plus_1_m: ∀n,m. (n + 1) * m = m + n * m.
+#n #m >distributive_times_plus_r //
 qed.
 
-variant le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n 
-≝ le_S_S_to_le.
-
-theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
- simplify; intros; destruct;autobatch.
-qed.
-
-theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
- intros 3; elim m names 0; clear m; simplify; intros; destruct;
- clear H; autobatch by le_S_S, transitive_le, le_plus_n, le_plus_n_r. 
-qed.
-
-theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
- intros; autobatch depth = 1.
-qed. 
-
-theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
- intros; autobatch depth = 1.
-qed.
-
-definition acc_nat: (nat → Prop) → nat →Prop ≝
-   λP:nat→Prop. λn. ∀m. m ≤ n → P m.
-
-theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
- unfold acc_nat; intros 4; elim n names 0; clear n;
- [ intros; autobatch by (eq_ind ? ? P), H, H2, le_n_O_to_eq.
-   (* lapply linear le_n_O_to_eq to H2; destruct; autobatch *)
- | intros 3; elim m; clear m; intros; clear H3;
-   [ clear H H1; autobatch depth = 2
-   | clear H; lapply linear le_inv_S_S to H4;
-     apply H1; clear H1; intros;
-     apply H2; clear H2; autobatch depth = 2
-   ]
- ].
-qed.
-
-theorem wf_nat_ind: 
-   ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
- intros; lapply linear depth=2 wf_le to H, H1 as H0; 
-  autobatch. 
-qed.
+lemma lt_plus_nmn_false: ∀m,n. n + m < n → False. 
+#m #n elim n -n
+[ #H elim (lt_zero_false … H)
+| /3 width=1/
+]
+qed-.
+
+lemma not_b_divides_nbr: ∀b,r. 0 < r → r < b → 
+                         ∀n,m. n * b + r = m * b → False.
+#b #r #Hr #Hrb #n elim n -n
+[ * normalize
+  [ -Hrb #H destruct elim (lt_refl_false … Hr)
+  | -Hr #m #H destruct
+    elim (lt_plus_nmn_false … Hrb)
+  ]
+| #n #IHn * normalize
+  [ -IHn -Hrb #H destruct
+    elim (plus_inv_O3 … H) -H #_ #H destruct
+    elim (lt_refl_false … Hr)
+  | -Hr -Hrb /3 width=3/
+  ]
+]
+qed-.
-- 
2.39.2