matita/matita/contribs/lambdadelta/ground/etc/ynat_old/ynat_le.etc

   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_2/star.ma".
  16 include "ground_2/ynat/ynat_iszero.ma".
  17 include "ground_2/ynat/ynat_pred.ma".
  18
  19 (* INFINITARY NATURAL NUMBERS ***********************************************)
  20
  21 (* order relation *)
  22 coinductive yle: relation ynat ≝
  23 | yle_O: ∀n. yle 0 n
  24 | yle_S: ∀m,n. yle m n → yle (⫯m) (⫯n)
  25 .
  26
  27 interpretation "natural 'less or equal to'" 'leq x y = (yle x y).
  28
  29 (* Inversion lemmas *********************************************************)
  30
  31 fact yle_inv_O2_aux: ∀m,x. m ≤ x → x = 0 → m = 0.
  32 #m #x * -m -x //
  33 #m #x #_ #H elim (discr_YS_YO … H) (**) (* destructing lemma needed *)
  34 qed-.
  35
  36 lemma yle_inv_O2: ∀m. m ≤ 0 → m = 0.
  37 /2 width =3 by yle_inv_O2_aux/ qed-.
  38
  39 fact yle_inv_S1_aux: ∀x,y. x ≤ y → ∀m. x = ⫯m → ∃∃n. m ≤ n & y = ⫯n.
  40 #x #y * -x -y
  41 [ #y #m #H elim (discr_YO_YS … H) (**) (* destructing lemma needed *)
  42 | #x #y #Hxy #m #H destruct /2 width=3 by ex2_intro/
  43 ]
  44 qed-.
  45
  46 lemma yle_inv_S1: ∀m,y.  ⫯m ≤ y → ∃∃n. m ≤ n & y = ⫯n.
  47 /2 width=3 by yle_inv_S1_aux/ qed-.
  48
  49 lemma yle_inv_S: ∀m,n. ⫯m ≤ ⫯n → m ≤ n.
  50 #m #n #H elim (yle_inv_S1 … H) -H
  51 #x #Hx #H destruct //
  52 qed-.
  53
  54 (* Properties ***************************************************************)
  55
  56 let corec yle_refl: reflexive … yle ≝ ?.
  57 * [ @yle_O | #x @yle_S // ]
  58 qed.
  59
  60 let corec yle_Y: ∀m. m ≤ ∞ ≝ ?.
  61 * [ @yle_O | #m <Y_rew @yle_S // ]
  62 qed.
  63
  64 let corec yle_S_dx: ∀m,n. m ≤ n → m ≤ ⫯n ≝ ?.
  65 #m #n * -m -n [ #n @yle_O | #m #n #H @yle_S /2 width=1 by/ ]
  66 qed.
  67
  68 lemma yle_refl_S_dx: ∀x. x ≤ ⫯x.
  69 /2 width=1 by yle_refl, yle_S_dx/ qed.
  70
  71 lemma yle_pred_sn: ∀m,n. m ≤ n → ⫰m ≤ n ≝ ?.
  72 * // #m #n #H elim (yle_inv_S1 … H) -H
  73 #x #Hm #H destruct /2 width=1 by yle_S_dx/
  74 qed.
  75
  76 lemma yle_refl_pred_sn: ∀x. ⫰x ≤ x.
  77 /2 width=1 by yle_refl, yle_pred_sn/ qed.
  78
  79 let corec yle_trans: Transitive … yle ≝ ?.
  80 #x #y * -x -y [ #x #z #_ @yle_O ]
  81 #x #y #Hxy #z #H elim (yle_inv_S1 … H) -H
  82 #n #Hyz #H destruct
  83 @yle_S @(yle_trans … Hxy … Hyz) (**) (* cofix not guarded by constructors *)
  84 qed-.