matita/library_auto/auto/nat/nat.ma

   1 (**************************************************************************)
   2 (*       ___                                                                  *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/library_auto/nat/nat".
  16
  17 include "higher_order_defs/functions.ma".
  18
  19 inductive nat : Set \def
  20   | O : nat
  21   | S : nat \to nat.
  22
  23 definition pred: nat \to nat \def
  24  \lambda n:nat. match n with
  25  [ O \Rightarrow  O
  26  | (S p) \Rightarrow p ].
  27
  28 theorem pred_Sn : \forall n:nat.n=(pred (S n)).
  29   auto.
  30  (*intros. reflexivity.*)
  31 qed.
  32
  33 theorem injective_S : injective nat nat S.
  34  unfold injective.
  35  intros.
  36  rewrite > pred_Sn.
  37  rewrite > (pred_Sn y).
  38  auto.
  39  (*apply eq_f.
  40  assumption.*)
  41 qed.
  42
  43 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m \def
  44  injective_S.
  45
  46 theorem not_eq_S  : \forall n,m:nat.
  47  \lnot n=m \to S n \neq S m.
  48  intros.
  49  unfold Not.
  50  intros.
  51  auto.
  52  (*apply H.
  53  apply injective_S.
  54  assumption.*)
  55 qed.
  56
  57 definition not_zero : nat \to Prop \def
  58  \lambda n: nat.
  59   match n with
  60   [ O \Rightarrow False
  61   | (S p) \Rightarrow True ].
  62
  63 theorem not_eq_O_S : \forall n:nat. O \neq S n.
  64  intros.
  65  unfold Not.
  66  intros.
  67  cut (not_zero O)
  68  [exact Hcut
  69  |rewrite > H.exact I]
  70 qed.
  71
  72 theorem not_eq_n_Sn : \forall n:nat. n \neq S n.
  73  intros.
  74  elim n
  75  [apply not_eq_O_S
  76  |apply not_eq_S.assumption]
  77 qed.
  78
  79 theorem nat_case:
  80  \forall n:nat.\forall P:nat \to Prop.
  81   P O \to  (\forall m:nat. P (S m)) \to P n.
  82   intros.
  83
  84   elim n
  85   [ assumption
  86   | apply H1 ]
  87 qed.
  88
  89 theorem nat_case1:
  90  \forall n:nat.\forall P:nat \to Prop.
  91   (n=O \to P O) \to  (\forall m:nat. (n=(S m) \to P (S m))) \to P n.
  92 intros 2;
  93 elim n
  94   [ auto
  95     (*apply H;
  96     reflexivity*)
  97   | auto
  98     (*apply H2;
  99     reflexivity*) ]
 100 qed.
 101
 102 theorem nat_elim2 :
 103  \forall R:nat \to nat \to Prop.
 104   (\forall n:nat. R O n)
 105   \to (\forall n:nat. R (S n) O)
 106   \to (\forall n,m:nat. R n m \to R (S n) (S m))
 107   \to \forall n,m:nat. R n m.
 108  intros 5;
 109  elim n
 110   [ apply H
 111   | apply (nat_case m)
 112     [ apply H1
 113     |intro;
 114      auto
 115      (*apply H2;
 116      apply H3*)
 117     ]
 118   ]
 119 qed.
 120
 121 theorem decidable_eq_nat : \forall n,m:nat.decidable (n=m).
 122  intros.unfold decidable.
 123  apply (nat_elim2 (\lambda n,m.(Or (n=m) ((n=m) \to False))))
 124  [ intro; elim n1
 125    [auto
 126     (*left;
 127     reflexivity*)
 128    |auto
 129    (*right;
 130    apply not_eq_O_S*) ]
 131  | intro;
 132    right;
 133    intro;
 134    apply (not_eq_O_S n1);
 135    auto
 136    (*apply sym_eq;
 137    assumption*)
 138  | intros; elim H
 139    [  auto
 140       (*left;
 141       apply eq_f;
 142       assumption*)
 143    | right;
 144      intro;
 145      auto
 146      (*apply H1;
 147      apply inj_S;
 148      assumption*)
 149    ]
 150  ]
 151 qed.