]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_max.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_max.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_succ_tri.ma".
16
17 (* MAXIMUM FOR NON-NEGATIVE INTEGERS ****************************************)
18
19 (*** max *)
20 definition nmax: nat → nat → nat ≝
21            λm,n. ntri … m n n n m.
22
23 interpretation
24   "maximum (non-negative integers)"
25   'or m n = (nmax m n).
26
27 (* Basic constructions ******************************************************)
28
29 (*** max_O1 *)
30 lemma nmax_zero_sn (n2): n2 = (𝟎 ∨ n2).
31 * //
32 qed.
33
34 (*** max_O2 *)
35 lemma nmax_zero_dx (n1): n1 = (n1 ∨ 𝟎).
36 * //
37 qed.
38
39 (*** max_SS *)
40 lemma nmax_succ_bi (n1) (n2): ↑(n1 ∨ n2) = (↑n1 ∨ ↑n2).
41 #n1 #n2
42 @trans_eq [3: @ntri_succ_bi | skip ] (* * rewrite fails because δ-expansion gets in the way *)
43 <ntri_f_tri //
44 qed.
45
46 (* Advanced constructions ***************************************************)
47
48 (*** idempotent_max *)
49 lemma nmax_idem (n): n = (n ∨ n).
50 /2 width=1 by ntri_eq/ qed.
51
52 (*** commutative_max *)
53 lemma nmax_comm: commutative … nmax.
54 #m #n @(nat_ind_2_succ … m n) -m -n //
55 qed-.
56
57 (*** associative_max *)
58 lemma nmax_assoc: associative … nmax.
59 #n1 #n2 @(nat_ind_2_succ … n1 n2) -n1 -n2 //
60 #n1 #n2 #IH #n3 @(nat_ind_succ … n3) -n3 //
61 qed.
62
63 lemma nmax_max_comm_23 (o:nat) (m) (n): (o ∨ m ∨ n) = (o ∨ n ∨ m).
64 #o #m #n >nmax_assoc >nmax_assoc <nmax_comm in ⊢ (??(??%)?); //
65 qed.
66
67 (* Basic inversions *********************************************************)
68
69 lemma eq_inv_zero_nmax (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
70 #n1 #n2 @(nat_ind_2_succ … n1 n2) -n1 -n2 /2 width=1 by conj/
71 #n1 #n2 #_ <nmax_succ_bi #H
72 elim (eq_inv_zero_nsucc … H)
73 qed-.
74
75 (*** max_inv_O3 *)
76 lemma eq_inv_nmax_zero (n1) (n2): (n1 ∨ n2) = 𝟎 → ∧∧ 𝟎 = n1 & 𝟎 = n2.
77 /2 width=1 by eq_inv_zero_nmax/ qed-.