]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/Z/orders.ma
unreleased version of the bindings, with more gtkmathview method bounds and dependenc...
[helm.git] / helm / 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
19 definition Zle : Z \to Z \to Prop \def
20 \lambda x,y:Z.
21   match x with
22   [ OZ \Rightarrow 
23     match y with 
24     [ OZ \Rightarrow True
25     | (pos m) \Rightarrow True
26     | (neg m) \Rightarrow False ]
27   | (pos n) \Rightarrow 
28     match y with 
29     [ OZ \Rightarrow False
30     | (pos m) \Rightarrow n \leq m
31     | (neg m) \Rightarrow False ]
32   | (neg n) \Rightarrow 
33     match y with 
34     [ OZ \Rightarrow True
35     | (pos m) \Rightarrow True
36     | (neg m) \Rightarrow m \leq n ]].
37
38 (*CSC: the URI must disappear: there is a bug now *)
39 interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
40
41 definition Zlt : Z \to Z \to Prop \def
42 \lambda x,y:Z.
43   match x with
44   [ OZ \Rightarrow 
45     match y with 
46     [ OZ \Rightarrow False
47     | (pos m) \Rightarrow True
48     | (neg m) \Rightarrow False ]
49   | (pos n) \Rightarrow 
50     match y with 
51     [ OZ \Rightarrow False
52     | (pos m) \Rightarrow n<m
53     | (neg m) \Rightarrow False ]
54   | (neg n) \Rightarrow 
55     match y with 
56     [ OZ \Rightarrow True
57     | (pos m) \Rightarrow True
58     | (neg m) \Rightarrow m<n ]].
59     
60 (*CSC: the URI must disappear: there is a bug now *)
61 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
62
63 theorem irreflexive_Zlt: irreflexive Z Zlt.
64 change with \forall x:Z. x < x \to False.
65 intro.elim x.exact H.
66 cut neg n < neg n \to False.
67 apply Hcut.apply H.simplify.apply not_le_Sn_n.
68 cut pos n < pos n \to False.
69 apply Hcut.apply H.simplify.apply not_le_Sn_n.
70 qed.
71
72 theorem irrefl_Zlt: irreflexive Z Zlt
73 \def irreflexive_Zlt.
74
75 definition Z_compare : Z \to Z \to compare \def
76 \lambda x,y:Z.
77   match x with
78   [ OZ \Rightarrow 
79     match y with 
80     [ OZ \Rightarrow EQ
81     | (pos m) \Rightarrow LT
82     | (neg m) \Rightarrow GT ]
83   | (pos n) \Rightarrow 
84     match y with 
85     [ OZ \Rightarrow GT
86     | (pos m) \Rightarrow (nat_compare n m)
87     | (neg m) \Rightarrow GT]
88   | (neg n) \Rightarrow 
89     match y with 
90     [ OZ \Rightarrow LT
91     | (pos m) \Rightarrow LT
92     | (neg m) \Rightarrow nat_compare m n ]].
93
94 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
95 theorem Zlt_neg_neg_to_lt: 
96 \forall n,m:nat. neg n < neg m \to lt m n.
97 intros.apply H.
98 qed.
99
100 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
101 theorem lt_to_Zlt_neg_neg: \forall n,m:nat.lt m n \to neg n < neg m. 
102 intros.
103 simplify.apply H.
104 qed.
105
106 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
107 theorem Zlt_pos_pos_to_lt: 
108 \forall n,m:nat. pos n < pos m \to lt n m.
109 intros.apply H.
110 qed.
111
112 (*CSC: qui uso lt perche' ho due istanze diverse di < *)
113 theorem lt_to_Zlt_pos_pos: \forall n,m:nat.lt n m \to pos n < pos m. 
114 intros.
115 simplify.apply H.
116 qed.
117
118 theorem Z_compare_to_Prop : 
119 \forall x,y:Z. match (Z_compare x y) with
120 [ LT \Rightarrow x < y
121 | EQ \Rightarrow x=y
122 | GT \Rightarrow y < x]. 
123 intros.
124 elim x. elim y.
125 simplify.apply refl_eq.
126 simplify.exact I.
127 simplify.exact I.
128 elim y. simplify.exact I.
129 simplify. 
130 (*CSC: qui uso le perche' altrimenti ci sono troppe scelte
131   per via delle coercions! *)
132 cut match (nat_compare n1 n) with
133 [ LT \Rightarrow n1<n
134 | EQ \Rightarrow n1=n
135 | GT \Rightarrow n<n1] \to 
136 match (nat_compare n1 n) with
137 [ LT \Rightarrow (le (S n1) n)
138 | EQ \Rightarrow neg n = neg n1
139 | GT \Rightarrow (le (S n) n1)]. 
140 apply Hcut. apply nat_compare_to_Prop. 
141 elim (nat_compare n1 n).
142 simplify.exact H.
143 simplify.exact H.
144 simplify.apply eq_f.apply sym_eq.exact H.
145 simplify.exact I.
146 elim y.simplify.exact I.
147 simplify.exact I.
148 simplify.
149 (*CSC: qui uso le perche' altrimenti ci sono troppe scelte
150   per via delle coercions! *)
151 cut match (nat_compare n n1) with
152 [ LT \Rightarrow n<n1
153 | EQ \Rightarrow n=n1
154 | GT \Rightarrow n1<n] \to 
155 match (nat_compare n n1) with
156 [ LT \Rightarrow (le (S n) n1)
157 | EQ \Rightarrow pos n = pos n1
158 | GT \Rightarrow (le (S n1) n)]. 
159 apply Hcut. apply nat_compare_to_Prop. 
160 elim (nat_compare n n1).
161 simplify.exact H.
162 simplify.exact H.
163 simplify.apply eq_f.exact H.
164 qed.
165
166 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
167 intros 2.elim x.
168 cut OZ < y \to Zsucc OZ \leq y.
169 apply Hcut. assumption.simplify.elim y.
170 simplify.exact H1.
171 simplify.exact H1.
172 simplify.apply le_O_n.
173 cut neg n < y \to Zsucc (neg n) \leq y.
174 apply Hcut. assumption.elim n.
175 cut neg O < y \to Zsucc (neg O) \leq y.
176 apply Hcut. assumption.simplify.elim y.
177 simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
178 simplify.exact I.
179 cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
180 apply Hcut. assumption.simplify.
181 elim y.
182 simplify.exact I.
183 simplify.apply le_S_S_to_le n2 n1 H3.
184 simplify.exact I.
185 exact H.
186 qed.