]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/compare.ma
new apply almost there
[helm.git] / helm / software / matita / library / Z / 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 "Z/orders.ma".
16 include "nat/compare.ma".
17
18 (* boolean equality *)
19 definition eqZb : Z \to Z \to bool \def
20 \lambda x,y:Z.
21   match x with
22   [ OZ \Rightarrow 
23       match y with
24         [ OZ \Rightarrow true
25         | (pos q) \Rightarrow false
26         | (neg q) \Rightarrow false]
27   | (pos p) \Rightarrow 
28       match y with
29         [ OZ \Rightarrow false
30         | (pos q) \Rightarrow eqb p q
31         | (neg q) \Rightarrow false]     
32   | (neg p) \Rightarrow 
33       match y with
34         [ OZ \Rightarrow false
35         | (pos q) \Rightarrow false
36         | (neg q) \Rightarrow eqb p q]].
37
38 theorem eqZb_to_Prop: 
39 \forall x,y:Z. 
40 match eqZb x y with
41 [ true \Rightarrow x=y
42 | false \Rightarrow x \neq y].
43 intros.
44 elim x.
45   elim y.
46     simplify.reflexivity.
47     simplify.apply not_eq_OZ_pos.
48     simplify.apply not_eq_OZ_neg.
49   elim y.
50     simplify.unfold Not.intro.apply (not_eq_OZ_pos n).apply sym_eq.assumption.
51     simplify.apply eqb_elim.
52       intro.simplify.apply eq_f.assumption.
53       intro.simplify.unfold Not.intro.apply H.apply inj_pos.assumption.
54     simplify.apply not_eq_pos_neg.
55   elim y.
56     simplify.unfold Not.intro.apply (not_eq_OZ_neg n).apply sym_eq.assumption.
57     simplify.unfold Not.intro.apply (not_eq_pos_neg n1 n).apply sym_eq.assumption.
58     simplify.apply eqb_elim.
59       intro.simplify.apply eq_f.assumption.
60       intro.simplify.unfold Not.intro.apply H.apply inj_neg.assumption.
61 qed.
62
63 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
64 (x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
65 intros.
66 cut 
67 (match (eqZb x y) with
68 [ true \Rightarrow x=y
69 | false \Rightarrow x \neq y] \to P (eqZb x y)).
70 apply Hcut.
71 apply eqZb_to_Prop.
72 elim (eqZb).
73 apply (H H2).
74 apply (H1 H2).
75 qed.
76
77 definition Z_compare : Z \to Z \to compare \def
78 \lambda x,y:Z.
79   match x with
80   [ OZ \Rightarrow 
81     match y with 
82     [ OZ \Rightarrow EQ
83     | (pos m) \Rightarrow LT
84     | (neg m) \Rightarrow GT ]
85   | (pos n) \Rightarrow 
86     match y with 
87     [ OZ \Rightarrow GT
88     | (pos m) \Rightarrow (nat_compare n m)
89     | (neg m) \Rightarrow GT]
90   | (neg n) \Rightarrow 
91     match y with 
92     [ OZ \Rightarrow LT
93     | (pos m) \Rightarrow LT
94     | (neg m) \Rightarrow nat_compare m n ]].
95
96 theorem Z_compare_to_Prop : 
97 \forall x,y:Z. match (Z_compare x y) with
98 [ LT \Rightarrow x < y
99 | EQ \Rightarrow x=y
100 | GT \Rightarrow y < x]. 
101 intros.
102 elim x. 
103   elim y.
104     simplify.apply refl_eq.
105     simplify.exact I.
106     simplify.exact I.
107   elim y.
108     simplify.exact I.
109     simplify.
110       cut (match (nat_compare n n1) with
111       [ LT \Rightarrow n<n1
112       | EQ \Rightarrow n=n1
113       | GT \Rightarrow n1<n] \to 
114       match (nat_compare n n1) with
115       [ LT \Rightarrow (S n) \leq n1
116       | EQ \Rightarrow pos n = pos n1
117       | GT \Rightarrow (S n1) \leq n]). 
118         apply Hcut.apply nat_compare_to_Prop. 
119         elim (nat_compare n n1).
120           simplify.exact H.
121           simplify.apply eq_f.exact H.
122           simplify.exact H.
123     simplify.exact I.    
124   elim y. 
125     simplify.exact I.
126     simplify.exact I.
127     simplify. 
128       cut (match (nat_compare n1 n) with
129       [ LT \Rightarrow n1<n
130       | EQ \Rightarrow n1=n
131       | GT \Rightarrow n<n1] \to 
132       match (nat_compare n1 n) with
133       [ LT \Rightarrow (S n1) \leq n
134       | EQ \Rightarrow neg n = neg n1
135       | GT \Rightarrow (S n) \leq n1]). 
136         apply Hcut. apply nat_compare_to_Prop. 
137         elim (nat_compare n1 n).
138           simplify.exact H.
139           simplify.apply eq_f.apply sym_eq.exact H.
140           simplify.exact H.
141 qed.