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 rewrites ***********************************************************)
  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 rewrites ********************************************************)
  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_2 … m n) -m -n //
  56 qed-.
  57
  58 (*** associative_max *)
  59 lemma nmax_assoc: associative … nmax.
  60 #n1 elim n1 -n1 //
  61 #n1 #IH #n2 elim n2 -n2 //
  62 #n2 #_ #n3 elim n3 -n3 //
  63 qed-.
  64
  65 (* Basic inversions *********************************************************)
  66
  67 (*** max_inv_O3 *)
  68 lemma nmax_inv_zero (n1) (n2): 𝟎 = (n1 ∨ n2) → ∧∧ 𝟎 = n1 & 𝟎 = n2.
  69 #n1 elim n1 -n1 [ /2 width=1 by conj/ ]
  70 #n1 #_ #n2 elim n2 -n2 [ /2 width=1 by conj/ ]
  71 #n2 #_ <nmax_succ_bi #H
  72 elim (eq_inv_nzero_succ … H)
  73 qed-.