helm/software/matita/nlibrary/arithmetics/compare.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16
  17 ninductive compare : Type[0] ≝
  18 | LT : compare
  19 | EQ : compare
  20 | GT : compare.
  21
  22 ndefinition compare_invert: compare → compare ≝
  23   λc.match c with
  24       [ LT ⇒ GT
  25       | EQ ⇒ EQ
  26       | GT ⇒ LT ].
  27
  28 nlet rec nat_compare n m: compare ≝
  29 match n with
  30 [ O ⇒ match m with
  31       [ O ⇒ EQ
  32       | (S q) ⇒ LT ]
  33 | S p ⇒ match m with
  34       [ O ⇒ GT
  35       | S q ⇒ nat_compare p q]].
  36
  37 ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ.
  38 #n;nelim n
  39 ##[//
  40 ##|#m;#IH;nnormalize;//]
  41 nqed.
  42
  43 ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m).
  44 //;
  45 nqed.
  46
  47 ntheorem nat_compare_pred_pred:
  48   ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m).
  49 #n;#m;#Hn;#Hm;
  50 napply (lt_O_n_elim n Hn);
  51 napply (lt_O_n_elim m Hm);
  52 #p;#q;//;
  53 nqed.
  54
  55 ntheorem nat_compare_to_Prop:
  56   ∀n,m.match (nat_compare n m) with
  57     [ LT ⇒ n < m
  58     | EQ ⇒ n = m
  59     | GT ⇒ m < n ].
  60 #n;#m;
  61 napply (nat_elim2 (λn,m.match (nat_compare n m) with
  62   [ LT ⇒ n < m
  63   | EQ ⇒ n = m
  64   | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *)
  65 ##[##1,2:#n1;ncases n1;//;
  66 ##|#n1;#m1;nnormalize;ncases (nat_compare n1 m1);
  67    ##[##1,3:nnormalize;#IH;napply le_S_S;//;
  68    ##|nnormalize;#IH;nrewrite > IH;//]
  69 nqed.
  70
  71 ntheorem nat_compare_n_m_m_n:
  72   ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n).
  73 #n;#m;
  74 napply (nat_elim2 (λn,m. nat_compare n m = compare_invert (nat_compare m n)))
  75 ##[##1,2:#n1;ncases n1;//;
  76 ##|#n1;#m1;#IH;nnormalize;napply IH]
  77 nqed.
  78
  79 ntheorem nat_compare_elim :
  80   ∀n,m. ∀P:compare → Prop.
  81     (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (nat_compare n m).
  82 #n;#m;#P;#Hlt;#Heq;#Hgt;
  83 ncut (match (nat_compare n m) with
  84     [ LT ⇒ n < m
  85     | EQ ⇒ n=m
  86     | GT ⇒ m < n] →
  87   P (nat_compare n m))
  88 ##[ncases (nat_compare n m);
  89    ##[napply Hlt
  90    ##|napply Heq
  91    ##|napply Hgt]
  92 ##|#Hcut;napply Hcut;//;
  93 nqed.
  94
  95 ninductive cmp_cases (n,m:nat) : CProp[0] ≝
  96   | cmp_le : n ≤ m → cmp_cases n m
  97   | cmp_gt : m < n → cmp_cases n m.
  98
  99 ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m.
 100 (* sic
 101 #n;#m;#H;nelim H
 102 ##[//
 103 ##|/2/] *)
 104 /2/; nqed.
 105
 106 nlemma cmp_nat: ∀n,m.cmp_cases n m.
 107 #n;#m; nlapply (nat_compare_to_Prop n m);
 108 ncases (nat_compare n m);nnormalize; /3/;
 109 nqed.