matita/matita/contribs/lambdadelta/ground/arith/ynat_lminus.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/arith/nat_minus.ma".
  16 include "ground/arith/ynat_pred.ma".
  17
  18 (* LEFT SUBTRACTION FOR NON-NEGATIVE INTEGERS WITH INFINITY *****************)
  19
  20 (*** yminus_sn *)
  21 definition ylminus (x) (n): ynat ≝
  22            (ypred^n) x.
  23
  24 interpretation
  25   "left minus (non-negative integers with infinity)"
  26   'minus x n = (ylminus x n).
  27
  28 (* Basic constructions ******************************************************)
  29
  30 (*** yminus_O2 *)
  31 lemma ylminus_zero_dx (x:ynat): x = x - 𝟎 .
  32 // qed.
  33
  34 (*** yminus_pred1 *)
  35 lemma yminus_pred_sn (x) (n): ↓(x-n) = ↓x - n.
  36 #x #n @(niter_appl … ypred)
  37 qed.
  38
  39 (*** yminus_succ2 yminus_S2 *)
  40 lemma ylminus_succ_dx (x:ynat) (n): ↓(x-n) = x - ↑n.
  41 #x #n @(niter_succ … ypred)
  42 qed.
  43
  44 (*** yminus_SO2 *)
  45 lemma ylminus_unit_dx (x): ↓x = x - (𝟏).
  46 // qed.
  47
  48 (*** yminus_Y_inj *)
  49 lemma ylminus_inf_sn (n): ∞ = ∞ - n.
  50 #n @(nat_ind_succ … n) -n //
  51 qed.
  52
  53 (* Constructions with nminus ************************************************)
  54
  55 (*** yminus_inj *)
  56 lemma ylminus_inj_sn (m) (n): yinj_nat (m - n) = yinj_nat m - n.
  57 #m #n
  58 @(niter_compose ???? yinj_nat)
  59 @ypred_inj
  60 qed.
  61
  62 (* Advanced constructions ***************************************************)
  63
  64 (*** yminus_O1 *)
  65 lemma ylminus_zero_sn (n): 𝟎 = 𝟎 - n.
  66 // qed.
  67
  68 (*** yminus_refl *)
  69 lemma ylminus_refl (n): 𝟎 = yinj_nat n - n.
  70 // qed.
  71
  72 (*** yminus_minus_comm *)
  73 lemma ylminus_minus_comm (x) (n) (o):
  74       x - n - o = x - o - n.
  75 #x @(ynat_split_nat_inf … x) -x //
  76 qed.