X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fdama%2Fdama%2FQ_is_orded_divisble_group.ma;fp=matita%2Fcontribs%2Fdama%2Fdama%2FQ_is_orded_divisble_group.ma;h=762554dd06817f4e2debca96478bcb9311475d0e;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma b/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma new file mode 100644 index 000000000..762554dd0 --- /dev/null +++ b/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma @@ -0,0 +1,272 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + + + +include "Q/q.ma". +include "ordered_divisible_group.ma". + +definition strong_decidable ≝ + λA:Prop.A ∨ ¬ A. + +theorem strong_decidable_to_Not_Not_eq: + ∀T:Type.∀eq: T → T → Prop.∀x,y:T. + strong_decidable (x=y) → ¬x≠y → x=y. + intros; + cases s; + [ assumption + | elim (H H1) + ] +qed. + +definition apartness_of_strong_decidable: + ∀T:Type.(∀x,y:T.strong_decidable (x=y)) → apartness. + intros; + constructor 1; + [ apply T + | apply (λx,y:T.x ≠ y); + | simplify; + intros 2; + apply (H (refl_eq ??)); + | simplify; + intros 4; + apply H; + symmetry; + assumption + | simplify; + intros; + elim (f x z); + [ elim (f z y); + [ elim H; + transitivity z; + assumption + | right; + assumption + ] + | left; + assumption + ] + ] +qed. + +theorem strong_decidable_to_strong_ext: + ∀T:Type.∀sd:∀x,y:T.strong_decidable (x=y). + ∀op:T→T. strong_ext (apartness_of_strong_decidable ? sd) op. + intros 6; + intro; + apply a; + apply eq_f; + assumption; +qed. + +theorem strong_decidable_to_transitive_to_cotransitive: + ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) → + transitive ? le → cotransitive ? (λx,y.¬ (le x y)). + intros; + whd; + simplify; + intros; + elim (f x z); + [ elim (f z y); + [ elim H; + apply (t ? z); + assumption + | right; + assumption + ] + | left; + assumption + ] +qed. + +theorem reflexive_to_coreflexive: + ∀T:Type.∀le:T→T→Prop.reflexive ? le → coreflexive ? (λx,y.¬(le x y)). + intros; + unfold; + simplify; + intros 2; + apply H1; + apply H; +qed. + +definition ordered_set_of_strong_decidable: + ∀T:Type.∀le:T→T→Prop.(∀x,y:T.strong_decidable (le x y)) → + transitive ? le → reflexive ? le → excess. + intros; + constructor 1; + [ apply T + | apply (λx,y.¬(le x y)); + | apply reflexive_to_coreflexive; + assumption + | apply strong_decidable_to_transitive_to_cotransitive; + assumption + ] +qed. + +definition abelian_group_of_strong_decidable: + ∀T:Type.∀plus:T→T→T.∀zero:T.∀opp:T→T. + (∀x,y:T.strong_decidable (x=y)) → + associative ? plus (eq T) → + commutative ? plus (eq T) → + (∀x:T. plus zero x = x) → + (∀x:T. plus (opp x) x = zero) → + abelian_group. + intros; + constructor 1; + [apply (apartness_of_strong_decidable ? f);] + try assumption; + [ change with (associative ? plus (λx,y:T.¬x≠y)); + simplify; + intros; + intro; + apply H2; + apply a; + | intros 2; + intro; + apply a1; + apply c; + | intro; + intro; + apply a1; + apply H + | intro; + intro; + apply a1; + apply H1 + | intros; + apply strong_decidable_to_strong_ext; + assumption + ] +qed. + +definition left_neutral ≝ λC:Type.λop.λe:C. ∀x:C. op e x = x. +definition left_inverse ≝ λC:Type.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e. + +record nabelian_group : Type ≝ + { ncarr:> Type; + nplus: ncarr → ncarr → ncarr; + nzero: ncarr; + nopp: ncarr → ncarr; + nplus_assoc: associative ? nplus (eq ncarr); + nplus_comm: commutative ? nplus (eq ncarr); + nzero_neutral: left_neutral ? nplus nzero; + nopp_inverse: left_inverse ? nplus nzero nopp + }. + +definition abelian_group_of_nabelian_group: + ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group. + intros; + apply abelian_group_of_strong_decidable; + [2: apply (nplus G) + | skip + | apply (nzero G) + | apply (nopp G) + | assumption + | apply nplus_assoc; + | apply nplus_comm; + | apply nzero_neutral; + | apply nopp_inverse + ] +qed. + +definition Z_abelian_group: abelian_group. + apply abelian_group_of_nabelian_group; + [ constructor 1; + [ apply Z + | apply Zplus + | apply OZ + | apply Zopp + | whd; + intros; + symmetry; + apply associative_Zplus + | apply sym_Zplus + | intro; + reflexivity + | intro; + rewrite > sym_Zplus; + apply Zplus_Zopp; + ] + | simplify; + intros; + unfold; + generalize in match (eqZb_to_Prop x y); + elim (eqZb x y); + simplify in H; + [ left ; assumption + | right; assumption + ] + ] +qed. + +record nordered_set: Type ≝ + { nos_carr:> Type; + nos_le: nos_carr → nos_carr → Prop; + nos_reflexive: reflexive ? nos_le; + nos_transitive: transitive ? nos_le + }. + +definition excess_of_nordered_group: + ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess. + intros; + constructor 1; + [ apply (nos_carr O) + | apply (λx,y.¬(nos_le ? x y)) + | apply reflexive_to_coreflexive; + apply nos_reflexive + | apply strong_decidable_to_transitive_to_cotransitive; + [ assumption + | apply nos_transitive + ] + ] +qed. + +lemma non_deve_stare_qui: reflexive ? Zle. + intro; + elim x; + [ exact I + |2,3: simplify; + apply le_n; + ] +qed. + +axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y. + +axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x. + +definition Z_excess: excess. + apply excess_of_nordered_group; + [ constructor 1; + [ apply Z + | apply Zle + | apply non_deve_stare_qui + | apply transitive_Zle + ] + | simplify; + intros; + unfold; + generalize in match (Z_compare_to_Prop x y); + cases (Z_compare x y); simplify; intro; + [ left; + apply non_deve_stare_qui3; + assumption + | left; + rewrite > H; + apply non_deve_stare_qui + | right; + apply non_deve_stare_qui4; + assumption + ] + ] +qed. \ No newline at end of file