matita/matita/contribs/lambdadelta/ground/arith/nat_tri.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/pnat_tri.ma".
  16 include "ground/arith/nat.ma".
  17
  18 (* TRICHOTOMY OPERATOR FOR NON-NEGATIVE INTEGERS ****************************)
  19
  20 (* Note: this is "if eqb n1 n2 then a2 else if leb n1 n2 then a1 else a3" *)
  21 (*** tri *)
  22 definition ntri (A:Type[0]) (n1) (n2) (a1) (a2) (a3): A ≝
  23   match n1 with
  24   [ nzero    ⇒ match n2 with [ nzero ⇒ a2 | ninj p2 ⇒ a1 ]
  25   | ninj  p1 ⇒ match n2 with [ nzero ⇒ a3 | ninj p2 ⇒ ptri A p1 p2 a1 a2 a3 ]
  26   ].
  27
  28 (* Basic constructions ******************************************************)
  29
  30 lemma ntri_zero_bi (A) (a1) (a2) (a3):
  31       a2 = ntri A (𝟎) (𝟎) a1 a2 a3.
  32 // qed.
  33
  34 lemma ntri_zero_inj (A) (a1) (a2) (a3) (p):
  35       a1 = ntri A (𝟎) (ninj p) a1 a2 a3.
  36 // qed.
  37
  38 lemma ntri_inj_zero (A) (a1) (a2) (a3) (p):
  39       a3 = ntri A (ninj p) (𝟎) a1 a2 a3.
  40 // qed.
  41
  42 lemma ntri_inj_bi (A) (a1) (a2) (a3) (p1) (p2):
  43       ptri A (p1) (p2) a1 a2 a3 = ntri A (p1) (p2) a1 a2 a3.
  44 // qed.
  45
  46 (* Advanced constructions ***************************************************)
  47
  48 (*** tri_eq *)
  49 lemma ntri_eq (A) (a1) (a2) (a3) (n): a2 = ntri A n n a1 a2 a3.
  50 #A #a1 #a2 #a3 * //
  51 qed.
  52
  53 lemma ntri_f_tri (A) (B) (f) (a1) (a2) (a3) (n1) (n2):
  54       f (ntri A n1 n2 a1 a2 a3) = ntri B n1 n2 (f a1) (f a2) (f a3).
  55 #A #B #f #a1 #a2 #a3
  56 * [| #p1 ] * // #p2
  57 <ntri_inj_bi <ntri_inj_bi //
  58 qed.