helm/software/matita/contribs/character/classes/props_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 "classes/defs.ma".
  16
  17 theorem p_inv_O: P 0 \to False.
  18  intros; inversion H; clear H; intros;
  19  [ destruct
  20  | lapply linear plus_inv_O3 to H3; decompose; destruct;
  21    autobatch depth = 2
  22  ].
  23 qed.
  24
  25 theorem t_inv_O: T 0 \to False.
  26  intros; inversion H; clear H; intros;
  27  [ lapply linear times_inv_O3_S to H1; destruct; autobatch depth = 2
  28  | lapply linear times_inv_O3_S to H2; destruct; autobatch depth = 2
  29  ].
  30 qed.
  31
  32 theorem p_pos: \forall i. P i \to \exists k. i = S k.
  33  intros 1; elim i names 0; clear i; intros;
  34  [ lapply linear p_inv_O to H; decompose
  35  | autobatch depth = 2
  36  ].
  37 qed.
  38
  39 theorem t_pos: \forall i. T i \to \exists k. i = S k.
  40  intros 1; elim i names 0; clear i; intros;
  41  [ lapply linear t_inv_O to H; decompose
  42  | autobatch depth = 2
  43  ].
  44 qed.
  45
  46 theorem t_1: T 1 \to False.
  47  intros; inversion H; clear H; intros;
  48  [ lapply not_3_divides_1 to H1; decompose
  49  | lapply not_3_divides_1 to H2; decompose
  50  ].
  51 qed.
  52
  53 theorem t_3: T 3.
  54  change in \vdash (? %) with (1 * 3);
  55  autobatch depth = 2.
  56 qed.
  57
  58 theorem pt_inv_gen: \forall i.
  59                     (P i \to \exists h. i = S (h * 3)) \land
  60                     (T i \to \exists h,k. i = S (h * 3) * 3 \sup (S k)).
  61  intros 1; elim i using wf_nat_ind names 0; clear i; intros; split; intros;
  62  [ lapply linear p_inv_O to H; decompose
  63  | lapply linear t_inv_O to H; decompose
  64  | inversion H1; clear H1; intros;
  65    [ destruct; autobatch depth = 3
  66    | clear H3; lapply t_pos to H1; lapply p_pos to H2; decompose; destruct;
  67      lapply linear plus_inv_S_S_S to H4; decompose;
  68      lapply H to H4; lapply H to H3; clear H H4 H3; decompose; clear H3 H4;
  69      lapply linear H to H2; lapply linear H5 to H1; decompose;
  70      rewrite > H; rewrite > H2; clear H H2;
  71      rewrite < plus_n_Sm; rewrite > times_exp_x_y_Sz; autobatch depth = 2
  72    ]
  73  | inversion H1; clear H1; intros;
  74    [ lapply linear times_inv_S_m_SS to H2 as H0;
  75      lapply linear H to H0; decompose; clear H2;
  76      lapply linear H to H1; decompose; destruct;
  77      autobatch depth = 4
  78    | clear H2; lapply linear times_inv_S_m_SS to H3 as H0;
  79      lapply linear H to H0; decompose; clear H;
  80      lapply linear H2 to H1; decompose; destruct;
  81      autobatch depth = 3
  82    ]
  83  ].
  84 qed.
  85
  86 theorem p_inv_gen: \forall i. P i \to \exists h. i = S (h * 3).
  87  intros; lapply depth = 1 pt_inv_gen; decompose;
  88  lapply linear H1 to H as H0; autobatch depth = 1.
  89 qed.
  90
  91 theorem t_inv_gen: \forall i. T i \to \exists h,k. i = (S (h * 3)) * 3 \sup (S k).
  92  intros; lapply depth = 1 pt_inv_gen; decompose;
  93  lapply linear H2 to H as H0; autobatch depth = 2.
  94 qed.
  95
  96 theorem p_gen: \forall i. P (S (i * 3)).
  97  intros; elim i names 0; clear i; intros;
  98  [ simplify; autobatch depth = 2
  99  | rewrite > plus_3_S3n ; autobatch depth = 2
 100  ].
 101 qed.
 102
 103 theorem t_gen: \forall i,j. T (S (i * 3) * 3 \sup (S j)).
 104  intros; elim j names 0; clear j; intros;
 105  [ simplify in \vdash (? (? ? %)); autobatch depth = 2
 106  | rewrite > times_exp_x_y_Sz; autobatch depth = 2
 107  ].
 108 qed.