matita/matita/contribs/lambdadelta/ground/ynat/ynat_succ.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 "ground/ynat/ynat_pred.ma".
  16
  17 (* NATURAL NUMBERS WITH INFINITY ********************************************)
  18
  19 (* the successor function *)
  20 definition ysucc: ynat → ynat ≝ λm. match m with
  21 [ yinj m ⇒ ↑m
  22 | Y      ⇒ Y
  23 ].
  24
  25 interpretation "ynat successor" 'UpArrow m = (ysucc m).
  26
  27 lemma ysucc_inj: ∀m:nat. ↑(yinj m) = yinj (↑m).
  28 // qed.
  29
  30 lemma ysucc_Y: ↑(∞) = ∞.
  31 // qed.
  32
  33 (* Properties ***************************************************************)
  34
  35 lemma ypred_succ: ∀m. ↓↑m = m.
  36 * // qed.
  37
  38 lemma ynat_cases: ∀n:ynat. n = 0 ∨ ∃m:ynat. n = ↑m.
  39 *
  40 [ * /2 width=1 by or_introl/
  41   #n @or_intror @(ex_intro … n) // (**) (* explicit constructor *)
  42 | @or_intror @(ex_intro … (∞)) // (**) (* explicit constructor *)
  43 ]
  44 qed-.
  45
  46 lemma ysucc_iter_Y: ∀m. ysucc^m (∞) = ∞.
  47 #m elim m -m //
  48 #m #IHm whd in ⊢ (??%?); >IHm //
  49 qed.
  50
  51 (* Inversion lemmas *********************************************************)
  52
  53 lemma ysucc_inv_inj: ∀m,n. ↑m = ↑n → m = n.
  54 #m #n #H <(ypred_succ m) <(ypred_succ n) //
  55 qed-.
  56
  57 lemma ysucc_inv_refl: ∀m. ↑m = m → m = ∞.
  58 * //
  59 #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
  60 #H elim (lt_refl_false m) //
  61 qed-.
  62
  63 lemma ysucc_inv_inj_sn: ∀m2,n1. yinj m2 = ↑n1 →
  64                         ∃∃m1. n1 = yinj m1 & m2 = S m1.
  65 #m2 * normalize
  66 [ #n1 #H destruct /2 width=3 by ex2_intro/
  67 | #H destruct
  68 ]
  69 qed-.
  70
  71 lemma ysucc_inv_inj_dx: ∀m2,n1. ↑n1 = yinj m2  →
  72                         ∃∃m1. n1 = yinj m1 & m2 = S m1.
  73 /2 width=1 by ysucc_inv_inj_sn/ qed-.
  74
  75 lemma ysucc_inv_Y_sn: ∀m. ∞ = ↑m → m = ∞.
  76 * // normalize
  77 #m #H destruct
  78 qed-.
  79
  80 lemma ysucc_inv_Y_dx: ∀m. ↑m = ∞ → m = ∞.
  81 /2 width=1 by ysucc_inv_Y_sn/ qed-.
  82
  83 lemma ysucc_inv_O_sn: ∀m. yinj 0 = ↑m → ⊥. (**) (* explicit coercion *)
  84 #m #H elim (ysucc_inv_inj_sn … H) -H
  85 #n #_ #H destruct
  86 qed-.
  87
  88 lemma ysucc_inv_O_dx: ∀m:ynat. ↑m = 0 → ⊥.
  89 /2 width=2 by ysucc_inv_O_sn/ qed-.
  90
  91 (* Eliminators **************************************************************)
  92
  93 lemma ynat_ind: ∀R:predicate ynat.
  94                 R 0 → (∀n:nat. R n → R (↑n)) → R (∞) →
  95                 ∀x. R x.
  96 #R #H1 #H2 #H3 * // #n elim n -n /2 width=1 by/
  97 qed-.