matita/matita/contribs/BTM/character/class_pt.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "character/class.ma".
  16
  17 (* CHARACTER CLASSES ********************************************************)
  18
  19 (* Arithmetics of classes P and T *******************************************)
  20
  21 lemma pt_inv_gen: ∀i.
  22                   (P i → ∃h. i = h * 3 + 1) ∧
  23                   (T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1)).
  24 #i @(nat_elim1 … i) -i #i #IH
  25 @conj #H
  26 [ inversion H -H
  27   [ #H destruct /2 width=2/
  28   | #i0 #j0 #Hi0 #Hj0 #H destruct
  29     elim (t_pos … Hi0) #i #H destruct
  30     elim (p_pos … Hj0) #j #H destruct
  31     elim (IH (i+1) ?) // #_ #H
  32     elim (H Hi0) -H -Hi0 #hi #ki #H >H -H
  33     elim (IH (j+1) ?) -IH // #H #_ -i
  34     elim (H Hj0) -H -Hj0 #hj #H >H -j
  35     <associative_plus >exp_n_m_plus_1 /2 width=2/
  36   ]
  37 | @(T_inv_ind … H) -H #i0 #Hi0 #H destruct
  38   [ elim (p_pos … Hi0) #i #H destruct
  39     elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #H #_
  40     elim (H Hi0) -H -Hi0 #hi #H >H -i
  41     @(ex1_2_intro … hi 0) //
  42   | elim (t_pos … Hi0) #i #H destruct
  43     elim (IH (i+1) ?) -IH /2 width=1 by monotonic_le_plus_r/ #_ #H
  44     elim (H Hi0) -H -Hi0 #hi #ki #H >H -i
  45     >associative_times <exp_n_m_plus_1 /2 width=3/
  46   ]
  47 ]
  48 qed-.
  49
  50 theorem p_inv_gen: ∀i. P i → ∃h. i = h * 3 + 1.
  51 #i #Hi elim (pt_inv_gen i) /2 width=1/
  52 qed-.
  53
  54 theorem t_inv_gen: ∀i. T i → ∃∃h,k. i = (h * 3 + 1) * 3 ^ (k + 1).
  55 #i #Hi elim (pt_inv_gen i) /2 width=1/
  56 qed-.
  57
  58 theorem p_gen: ∀i. P (i * 3 + 1).
  59 #i @(nat_ind_plus … i) -i //
  60 #i #IHi >times_n_plus_1_m >associative_plus /2 width=1/
  61 qed.
  62
  63 theorem t_gen: ∀i,j. T ((i * 3 + 1) * 3 ^ (j + 1)).
  64 #i #j @(nat_ind_plus … j) -j /2 width=1/
  65 #j #IH >exp_n_m_plus_1 <associative_times /2 width=1/
  66 qed.
  67
  68 lemma pt_discr: ∀i. P i → T i → False.
  69 #i #Hp #Ht
  70 elim (p_inv_gen … Hp) -Hp #hp #Hp
  71 elim (t_inv_gen … Ht) -Ht #ht #kt #Ht destruct
  72 >exp_n_m_plus_1 in Ht; <associative_times #H
  73 elim (not_b_divides_nbr … H) -H //
  74 qed-.