helm/software/matita/contribs/character/preamble.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 "nat/exp.ma".
  16 include "nat/relevant_equations.ma".
  17
  18 alias num (instance 0) = "natural number".
  19
  20 theorem plus_inv_O3: ∀m,n. 0 = n + m → 0 = n ∧ 0 = m.
  21  intros 2; elim n names 0; clear n; simplify; intros;
  22  [ autobatch | destruct ].
  23 qed.
  24
  25 theorem times_inv_O3_S: ∀x,y. 0 = x * (S y) → x = 0.
  26  intros; rewrite < times_n_Sm in H;
  27  lapply linear plus_inv_O3 to H; decompose; destruct; autobatch.
  28 qed.
  29
  30 theorem not_3_divides_1: ∀n. 1 = n * 3 → False.
  31  intros 1; rewrite > sym_times; simplify;
  32  elim n names 0; simplify; intros; destruct;
  33  rewrite > sym_plus in Hcut; simplify in Hcut; destruct Hcut.
  34 qed.
  35
  36 theorem le_inv_S_S: ∀m,n. S m ≤ S n → m ≤ n.
  37  intros; inversion H; clear H; intros; destruct; autobatch.
  38 qed.
  39
  40 theorem plus_inv_S_S_S: ∀x,y,z. S x = S y + S z → S y ≤ x ∧ S z ≤ x.
  41  simplify; intros; destruct;
  42  rewrite < plus_n_Sm in ⊢ (? (? ? %) ?); autobatch.
  43 qed.
  44
  45 theorem times_inv_S_m_SS: ∀k,n,m. S n = m * (S (S k)) → m ≤ n.
  46  intros 3; elim m names 0; clear m; simplify; intros; destruct;
  47  clear H; apply le_S_S; rewrite < sym_times; simplify;
  48  autobatch depth = 2.
  49 qed.
  50
  51 theorem plus_3_S3n: ∀n. S (S n * 3) = 3 + S (n * 3).
  52  intros; simplify; autobatch depth = 1.
  53 qed.
  54
  55 theorem times_exp_x_y_Sz: ∀x,y,z. x * y \sup (S z) = (x * y \sup z) * y.
  56  intros; simplify; autobatch depth = 1.
  57 qed.
  58
  59 definition acc_nat: (nat → Prop) → nat →Prop ≝
  60    λP:nat→Prop. λn. ∀m. m ≤ n → P m.
  61
  62 theorem wf_le: ∀P. P 0 → (∀n. acc_nat P n → P (S n)) → ∀n. acc_nat P n.
  63  unfold acc_nat; intros 4; elim n names 0; clear n;
  64  [ intros; lapply linear le_n_O_to_eq to H2; destruct; autobatch
  65  | intros 3; elim m; clear m; intros; clear H3;
  66    [ clear H H1; autobatch depth = 2
  67    | clear H; lapply linear le_inv_S_S to H4;
  68      apply H1; clear H1; intros;
  69      apply H2; clear H2; autobatch depth = 2
  70    ]
  71  ].
  72 qed.
  73
  74 theorem wf_nat_ind:
  75    ∀P:nat→Prop. P O → (∀n. (∀m. m ≤ n → P m) → P (S n)) → ∀n. P n.
  76  intros; lapply linear depth=2 wf_le to H, H1 as H0;
  77  unfold acc_nat in H0; apply (H0 n n); autobatch depth = 1.
  78 qed.