]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_tri.ma
update in delayed_updating
[helm.git] / 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.