1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 include "arithmetics/nat.ma".
17 ninductive compare : Type[0] ≝
22 ndefinition compare_invert: compare → compare ≝
28 nlet rec nat_compare n m: compare ≝
35 | S q ⇒ nat_compare p q]].
37 ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ.
40 ##|#m;#IH;nnormalize;//]
43 ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m).
47 ntheorem nat_compare_pred_pred:
48 ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m).
50 napply (lt_O_n_elim n Hn);
51 napply (lt_O_n_elim m Hm);
55 ntheorem nat_compare_to_Prop:
56 ∀n,m.match (nat_compare n m) with
61 napply (nat_elim2 (λn,m.match (nat_compare n m) with
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;//]
71 ntheorem nat_compare_n_m_m_n:
72 ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n).
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]
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
88 ##[ncases (nat_compare n m);
92 ##|#Hcut;napply Hcut;//;
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.
99 ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m.
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/;