1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
18 include "ordered_divisible_group.ma".
20 definition strong_decidable ≝
23 theorem strong_decidable_to_Not_Not_eq:
24 ∀T:Type.∀eq: T → T → Prop.∀x,y:T.
25 strong_decidable (x=y) → ¬x≠y → x=y.
33 definition apartness_of_strong_decidable:
34 ∀T:Type.(∀x,y:T.strong_decidable (x=y)) → apartness.
38 | apply (λx,y:T.x ≠ y);
41 apply (H (refl_eq ??));
63 theorem strong_decidable_to_strong_ext:
64 ∀T:Type.∀sd:∀x,y:T.strong_decidable (x=y).
65 ∀op:T→T. strong_ext (apartness_of_strong_decidable ? sd) op.
73 theorem strong_decidable_to_transitive_to_cotransitive:
74 ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) →
75 transitive ? le → cotransitive ? (λx,y.¬ (le x y)).
93 theorem reflexive_to_coreflexive:
94 ∀T:Type.∀le:T→T→Prop.reflexive ? le → coreflexive ? (λx,y.¬(le x y)).
103 definition ordered_set_of_strong_decidable:
104 ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) →
105 transitive ? le → reflexive ? le → excess.
112 | apply (λx,y.¬(le x y));
113 | apply reflexive_to_coreflexive;
115 | apply strong_decidable_to_transitive_to_cotransitive;
121 definition abelian_group_of_strong_decidable:
122 ∀T:Type.∀plus:T→T→T.∀zero:T.∀opp:T→T.
123 (∀x,y:T.strong_decidable (x=y)) →
124 associative ? plus (eq T) →
125 commutative ? plus (eq T) →
126 (∀x:T. plus zero x = x) →
127 (∀x:T. plus (opp x) x = zero) →
131 [apply (apartness_of_strong_decidable ? f);]
133 [ change with (associative ? plus (λx,y:T.¬x≠y));
152 apply strong_decidable_to_strong_ext;
157 definition left_neutral ≝ λC:Type.λop.λe:C. ∀x:C. op e x = x.
158 definition left_inverse ≝ λC:Type.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e.
160 record nabelian_group : Type ≝
162 nplus: ncarr → ncarr → ncarr;
165 nplus_assoc: associative ? nplus (eq ncarr);
166 nplus_comm: commutative ? nplus (eq ncarr);
167 nzero_neutral: left_neutral ? nplus nzero;
168 nopp_inverse: left_inverse ? nplus nzero nopp
171 definition abelian_group_of_nabelian_group:
172 ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group.
174 apply abelian_group_of_strong_decidable;
182 | apply nzero_neutral;
187 definition Z_abelian_group: abelian_group.
188 apply abelian_group_of_nabelian_group;
197 apply associative_Zplus
208 generalize in match (eqZb_to_Prop x y);
217 record nordered_set: Type ≝
219 nos_le: nos_carr → nos_carr → Prop;
220 nos_reflexive: reflexive ? nos_le;
221 nos_transitive: transitive ? nos_le
224 definition excess_of_nordered_group:
225 ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess.
229 | apply (λx,y.¬(nos_le ? x y))
230 | apply reflexive_to_coreflexive;
232 | apply strong_decidable_to_transitive_to_cotransitive;
234 | apply nos_transitive
239 lemma non_deve_stare_qui: reflexive ? Zle.
248 axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y.
250 axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x.
252 definition Z_excess: excess.
253 apply excess_of_nordered_group;
257 | apply non_deve_stare_qui
258 | apply transitive_Zle
263 generalize in match (Z_compare_to_Prop x y);
264 cases (Z_compare x y); simplify; intro;
266 apply non_deve_stare_qui3;
270 apply non_deve_stare_qui
272 apply non_deve_stare_qui4;