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