matita/matita/contribs/BTM/character/class.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 (* BTM: MATITA SOURCE FILES
  16  * Suggested invocation to start formal specifications with:
  17  *   - Patience on me to gain peace and perfection! -
  18  * 2008 September 22:
  19  *   specification starts.
  20  *)
  21
  22 include "arith.ma".
  23
  24 (* CHARACTER CLASSES ********************************************************)
  25
  26 (* Note: OEIS sequence identifiers
  27    P(n): A016777 "3n+1"
  28    T(n): A155504 "(3h+1)*3^(k+1)"
  29 *)
  30
  31 inductive P: predicate nat ≝
  32    | p1: P 1
  33    | p2: ∀i,j. T i → P j → P (i + j)
  34 with T: predicate nat ≝
  35    | t1: ∀i. P i → T (i * 3)
  36    | t2: ∀i. T i → T (i * 3)
  37 .
  38
  39 inductive S: predicate nat ≝
  40    | s1: ∀i. P i → S (i * 2)
  41    | s2: ∀i. T i → S (i * 2)
  42 .
  43
  44 inductive Q: predicate nat ≝
  45    | q1: ∀i. P i → Q (i * 2 + 3)
  46    | q2: ∀i. Q i → Q (i * 3)
  47 .
  48
  49 (* Basic eliminators ********************************************************)
  50
  51 axiom p_ind: ∀R:predicate nat. R 1 →
  52              (∀i,j. T i → R j → R (i + j)) →
  53              ∀j. P j → R j.
  54
  55 axiom t_ind: ∀R:predicate nat.
  56              (∀i. P i → R (i * 3)) →
  57              (∀i. R i → R (i * 3)) →
  58              ∀i. T i → R i.
  59
  60 (* Basic inversion lemmas ***************************************************)
  61
  62 fact p_inv_O_aux: ∀i. P i → i = 0 → False.
  63 #i #H @(p_ind … H) -i
  64 [ #H destruct
  65 | #i #j #_ #IH #H
  66   elim (plus_inv_O3 … H) -H /2 width=1/
  67 ]
  68 qed-.
  69
  70 lemma p_inv_O: P 0 → False.
  71 /2 width=3 by p_inv_O_aux/ qed-.
  72
  73 fact t_inv_O_aux: ∀i. T i → i = 0 → False.
  74 #i #H @(t_ind … H) -i #i #IH #H
  75 lapply (times_inv_S2_O3 … H) -H /2 width=1/
  76 /2 width=3 by p_inv_O_aux/
  77 qed-.
  78
  79 lemma t_inv_O: T 0 → False.
  80 /2 width=3 by t_inv_O_aux/ qed-.
  81
  82 (* Basic properties *********************************************************)
  83
  84 lemma t_3: T 3.
  85 /2 width=1/ qed.
  86
  87 lemma p_pos: ∀i. P i → ∃k. i = k + 1.
  88 * /2 width=2/
  89 #H elim (p_inv_O … H)
  90 qed.
  91
  92 lemma t_pos: ∀i. T i → ∃k. i = k + 1.
  93 * /2 width=2/
  94 #H elim (t_inv_O … H)
  95 qed.