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