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