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