]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/Z/orders.ma
Even more Q stuff classified.
[helm.git] / helm / software / matita / library / Z / orders.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/orders".
16
17 include "Z/z.ma".
18 include "nat/orders.ma".
19
20 definition Zle : Z \to Z \to Prop \def
21 \lambda x,y:Z.
22   match x with
23   [ OZ \Rightarrow 
24     match y with 
25     [ OZ \Rightarrow True
26     | (pos m) \Rightarrow True
27     | (neg m) \Rightarrow False ]
28   | (pos n) \Rightarrow 
29     match y with 
30     [ OZ \Rightarrow False
31     | (pos m) \Rightarrow n \leq m
32     | (neg m) \Rightarrow False ]
33   | (neg n) \Rightarrow 
34     match y with 
35     [ OZ \Rightarrow True
36     | (pos m) \Rightarrow True
37     | (neg m) \Rightarrow m \leq n ]].
38
39 (*CSC: the URI must disappear: there is a bug now *)
40 interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
41 (*CSC: the URI must disappear: there is a bug now *)
42 interpretation "integer 'neither less nor equal to'" 'nleq x y =
43   (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
44
45 definition Zlt : Z \to Z \to Prop \def
46 \lambda x,y:Z.
47   match x with
48   [ OZ \Rightarrow 
49     match y with 
50     [ OZ \Rightarrow False
51     | (pos m) \Rightarrow True
52     | (neg m) \Rightarrow False ]
53   | (pos n) \Rightarrow 
54     match y with 
55     [ OZ \Rightarrow False
56     | (pos m) \Rightarrow n<m
57     | (neg m) \Rightarrow False ]
58   | (neg n) \Rightarrow 
59     match y with 
60     [ OZ \Rightarrow True
61     | (pos m) \Rightarrow True
62     | (neg m) \Rightarrow m<n ]].
63     
64 (*CSC: the URI must disappear: there is a bug now *)
65 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
66 (*CSC: the URI must disappear: there is a bug now *)
67 interpretation "integer 'not less than'" 'nless x y =
68   (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
69
70 theorem irreflexive_Zlt: irreflexive Z Zlt.
71 unfold irreflexive.unfold Not.
72 intro.elim x.exact H.
73 cut (neg n < neg n \to False).
74 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
75 cut (pos n < pos n \to False).
76 apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
77 qed.
78
79 (* transitivity *)
80 theorem transitive_Zle : transitive Z Zle.
81 unfold transitive.
82 intros 3.
83 elim x 0
84 [ (* x = OZ *)
85   elim y 0
86   [ intros. assumption 
87   | intro.
88     elim z
89     [ simplify. apply I 
90     | simplify. apply I
91     | simplify. simplify in H1. assumption
92     ]
93   | intro.
94     elim z
95     [ simplify. apply I
96     | simplify. apply I
97     | simplify. simplify in H. assumption
98     ]
99   ]
100 | (* x = (pos n) *)
101   intro.
102   elim y 0
103   [ intros. apply False_ind. apply H
104   | intros 2. 
105     elim z 0
106     [ simplify. intro. assumption
107     | intro. generalize in match H. simplify. apply trans_le 
108     | intro. simplify. intro. assumption
109     ]
110   | intros 2. apply False_ind. apply H
111   ]
112 | (* x = (neg n) *)
113   intro.
114   elim y 0
115   [ elim z 0
116     [ simplify. intros. assumption
117     | intro. simplify. intros. assumption
118     | intro. simplify. intros. apply False_ind. apply H1
119     ]
120   | intros 2.
121     elim z
122     [ apply False_ind. apply H1 
123     | simplify. apply I
124     | apply False_ind. apply H1
125     ]
126   | intros 2.
127     elim z 0
128     [ simplify. intro. assumption
129     | intro. simplify. intro. assumption
130     | intros. simplify. simplify in H. simplify in H1. 
131       generalize in match H. generalize in match H1. apply trans_le
132     ]
133   ]
134 ]
135 qed.
136
137 variant trans_Zle: transitive Z Zle
138 \def transitive_Zle.
139
140 theorem transitive_Zlt: transitive Z Zlt.
141 unfold.
142 intros 3.
143 elim x 0
144 [ (* x = OZ *)
145   elim y 0
146   [ intros. apply False_ind. apply H 
147   | intro.
148     elim z
149     [ simplify. apply H1 
150     | simplify. apply I
151     | simplify. apply H1
152     ]
153   | intros 2. apply False_ind. apply H
154   ]
155 | (* x = (pos n) *)
156   intro.
157   elim y 0
158   [ intros. apply False_ind. apply H
159   | intros 2. 
160     elim z 0
161     [ simplify. intro. assumption
162     | intro. generalize in match H. simplify. apply trans_lt 
163     | intro. simplify. intro. assumption
164     ]
165   | intros 2. apply False_ind. apply H
166   ]
167 | (* x = (neg n) *)
168   intro.
169   elim y 0
170   [ elim z 0
171     [ intros. simplify. apply I
172     | intro. simplify. intros. assumption
173     | intro. simplify. intros. apply False_ind. apply H1
174     ]
175   | intros 2.
176     elim z
177     [ apply False_ind. apply H1 
178     | simplify. apply I
179     | apply False_ind. apply H1
180     ]
181   | intros 2.
182     elim z 0
183     [ simplify. intro. assumption
184     | intro. simplify. intro. assumption
185     | intros. simplify. simplify in H. simplify in H1. 
186       generalize in match H. generalize in match H1. apply trans_lt
187     ]
188   ]
189 ]
190 qed.
191
192 variant trans_Zlt: transitive Z Zlt
193 \def transitive_Zlt.
194 theorem irrefl_Zlt: irreflexive Z Zlt
195 \def irreflexive_Zlt.
196
197 theorem Zlt_neg_neg_to_lt: 
198 \forall n,m:nat. neg n < neg m \to m < n.
199 intros.apply H.
200 qed.
201
202 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.m < n \to neg n < neg m. 
203 intros.
204 simplify.apply H.
205 qed.
206
207 theorem Zlt_pos_pos_to_lt: 
208 \forall n,m:nat. pos n < pos m \to n < m.
209 intros.apply H.
210 qed.
211
212 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.n < m \to pos n < pos m. 
213 intros.
214 simplify.apply H.
215 qed.
216
217 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
218 intros 2.
219 elim x.
220 (* goal: x=OZ *)
221   cut (OZ < y \to Zsucc OZ \leq y).
222     apply Hcut. assumption.
223     simplify.elim y. 
224       simplify.exact H1.
225       simplify.apply le_O_n.
226       simplify.exact H1.
227 (* goal: x=pos *)      
228   exact H.
229 (* goal: x=neg *)      
230   cut (neg n < y \to Zsucc (neg n) \leq y).
231     apply Hcut. assumption.
232     elim n.
233       cut (neg O < y \to Zsucc (neg O) \leq y).
234         apply Hcut. assumption.
235         simplify.elim y.
236           simplify.exact I.
237           simplify.exact I.
238           simplify.apply (not_le_Sn_O n1 H2).
239       cut (neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y).
240         apply Hcut. assumption.simplify.
241         elim y.
242           simplify.exact I.
243           simplify.exact I.
244           simplify.apply (le_S_S_to_le n2 n1 H3).
245 qed.