]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/dama/nat_ordered_set.ma
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / matita / library / dama / nat_ordered_set.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 "nat/compare.ma".
16 include "dama/bishop_set.ma". 
17
18 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
19
20 lemma nat_elim2: 
21   ∀R:nat → nat → CProp.
22   (∀ n:nat. R O n) → (∀n:nat. R (S n) O) → (∀n,m:nat. R n m → R (S n) (S m)) →
23     ∀n,m:nat. R n m.
24 intros 5;elim n; [apply H]
25 cases m;[ apply H1| apply H2; apply H3 ]
26 qed.
27
28 alias symbol "lt" = "natural 'less than'".
29 lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
30 intros (x y); apply (nat_elim2 ???? x y); 
31 [1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
32 |2: intro;right;apply lt_O_S;
33 |3: intros; cases H; 
34     [1: cases H1; [left; left; apply le_S_S; assumption]
35         left;right;rewrite > H2; reflexivity;
36     |2: right;apply le_S_S; assumption]]
37 qed.
38         
39 lemma nat_excess_cotransitive: cotransitive ? nat_excess.
40 intros 3 (x y z); unfold nat_excess; simplify; intros;
41 cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
42 [1: right; apply (trans_lt ??? H H2);
43 |2: right; rewrite < H2; assumption;]
44 qed.
45   
46 lemma nat_ordered_set : ordered_set.
47 letin hos ≝ (mk_half_ordered_set nat (λT,R:Type.λf:T→T→R.f) ? nat_excess ? nat_excess_cotransitive);
48 [ intros; left; intros; reflexivity;
49 | intro x; intro H; apply (not_le_Sn_n ? H);]
50 constructor 1;  apply hos;
51 qed.
52
53 interpretation "ordered set N" 'N = nat_ordered_set.
54
55 alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
56 lemma os_le_to_nat_le:
57   ∀a,b:nat_ordered_set.a ≤ b → le a b.
58 intros; normalize in H; apply (not_lt_to_le b a H);
59 qed.
60  
61 lemma nat_le_to_os_le:
62   ∀a,b:nat_ordered_set.le a b → a ≤ b.
63 intros 3; apply (le_to_not_lt a b);assumption;
64 qed.
65