matita/contribs/dama/dama/Q_is_orded_divisble_group.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "Q/q.ma".
  18 include "ordered_divisible_group.ma".
  19
  20 definition strong_decidable ≝
  21  λA:Prop.A ∨ ¬ A.
  22
  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.
  26  intros;
  27  cases s;
  28   [ assumption
  29   | elim (H H1)
  30   ]
  31 qed.
  32
  33 definition apartness_of_strong_decidable:
  34  ∀T:Type.(∀x,y:T.strong_decidable (x=y)) → apartness.
  35  intros;
  36  constructor 1;
  37   [ apply T
  38   | apply (λx,y:T.x ≠ y);
  39   | simplify;
  40     intros 2;
  41     apply (H (refl_eq ??));
  42   | simplify;
  43     intros 4;
  44     apply H;
  45     symmetry;
  46     assumption
  47   | simplify;
  48     intros;
  49     elim (f x z);
  50      [ elim (f z y);
  51        [ elim H;
  52          transitivity z;
  53          assumption
  54        | right;
  55          assumption
  56        ]
  57      | left;
  58        assumption
  59      ]
  60   ]
  61 qed.
  62
  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.
  66  intros 6;
  67  intro;
  68  apply a;
  69  apply eq_f;
  70  assumption;
  71 qed.
  72
  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)).
  76  intros;
  77  whd;
  78  simplify;
  79  intros;
  80  elim (f x z);
  81   [ elim (f z y);
  82     [ elim H;
  83       apply (t ? z);
  84       assumption
  85     | right;
  86       assumption
  87     ]
  88   | left;
  89     assumption
  90   ]
  91 qed.
  92
  93 theorem reflexive_to_coreflexive:
  94  ∀T:Type.∀le:T→T→Prop.reflexive ? le → coreflexive ? (λx,y.¬(le x y)).
  95  intros;
  96  unfold;
  97  simplify;
  98  intros 2;
  99  apply H1;
 100  apply H;
 101 qed.
 102
 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.
 106  intros;
 107  constructor 1;
 108   [ apply T
 109   | apply (λx,y.¬(le x y));
 110   | apply reflexive_to_coreflexive;
 111     assumption
 112   | apply strong_decidable_to_transitive_to_cotransitive;
 113     assumption
 114   ]
 115 qed.
 116
 117 definition abelian_group_of_strong_decidable:
 118  ∀T:Type.∀plus:T→T→T.∀zero:T.∀opp:T→T.
 119   (∀x,y:T.strong_decidable (x=y)) →
 120    associative ? plus (eq T) →
 121     commutative ? plus (eq T) →
 122      (∀x:T. plus zero x = x) →
 123       (∀x:T. plus (opp x) x = zero) →
 124        abelian_group.
 125  intros;
 126  constructor 1;
 127   [apply (apartness_of_strong_decidable ? f);]
 128  try assumption;
 129  [ change with (associative ? plus (λx,y:T.¬x≠y));
 130    simplify;
 131    intros;
 132    intro;
 133    apply H2;
 134    apply a;
 135  | intros 2;
 136    intro;
 137    apply a1;
 138    apply c;
 139  | intro;
 140    intro;
 141    apply a1;
 142    apply H
 143  | intro;
 144    intro;
 145    apply a1;
 146    apply H1
 147  | intros;
 148    apply strong_decidable_to_strong_ext;
 149    assumption
 150  ]
 151 qed.
 152
 153 definition left_neutral ≝ λC:Type.λop.λe:C. ∀x:C. op e x = x.
 154 definition left_inverse ≝ λC:Type.λop.λe:C.λinv:C→C. ∀x:C. op (inv x) x = e.
 155
 156 record nabelian_group : Type ≝
 157  { ncarr:> Type;
 158    nplus: ncarr → ncarr → ncarr;
 159    nzero: ncarr;
 160    nopp: ncarr → ncarr;
 161    nplus_assoc: associative ? nplus (eq ncarr);
 162    nplus_comm: commutative ? nplus (eq ncarr);
 163    nzero_neutral: left_neutral ? nplus nzero;
 164    nopp_inverse: left_inverse ? nplus nzero nopp
 165  }.
 166
 167 definition abelian_group_of_nabelian_group:
 168  ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group.
 169  intros;
 170  apply abelian_group_of_strong_decidable;
 171   [2: apply (nplus G)
 172   | skip
 173   | apply (nzero G)
 174   | apply (nopp G)
 175   | assumption
 176   | apply nplus_assoc;
 177   | apply nplus_comm;
 178   | apply nzero_neutral;
 179   | apply nopp_inverse
 180   ]
 181 qed.
 182
 183 definition Z_abelian_group: abelian_group.
 184  apply abelian_group_of_nabelian_group;
 185   [ constructor 1;
 186      [ apply Z
 187      | apply Zplus
 188      | apply OZ
 189      | apply Zopp
 190      | whd;
 191        intros;
 192        symmetry;
 193        apply associative_Zplus
 194      | apply sym_Zplus
 195      | intro;
 196        reflexivity
 197      | intro;
 198        rewrite > sym_Zplus;
 199        apply Zplus_Zopp;
 200      ]
 201   | simplify;
 202     intros;
 203     unfold;
 204     generalize in match (eqZb_to_Prop x y);
 205     elim (eqZb x y);
 206     simplify in H;
 207      [ left ; assumption
 208      | right; assumption
 209      ]
 210   ]
 211 qed.
 212
 213 record nordered_set: Type ≝
 214  { nos_carr:> Type;
 215    nos_le: nos_carr → nos_carr → Prop;
 216    nos_reflexive: reflexive ? nos_le;
 217    nos_transitive: transitive ? nos_le
 218  }.
 219
 220 definition excess_of_nordered_group:
 221  ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess.
 222  intros;
 223  constructor 1;
 224   [ apply (nos_carr O)
 225   | apply (λx,y.¬(nos_le ? x y))
 226   | apply reflexive_to_coreflexive;
 227     apply nos_reflexive
 228   | apply strong_decidable_to_transitive_to_cotransitive;
 229      [ assumption
 230      | apply nos_transitive
 231      ]
 232   ]
 233 qed.
 234
 235 lemma non_deve_stare_qui: reflexive ? Zle.
 236  intro;
 237  elim x;
 238   [ exact I
 239   |2,3: simplify;
 240     apply le_n;
 241   ]
 242 qed.
 243
 244 axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y.
 245
 246 axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x.
 247
 248 definition Z_excess: excess.
 249  apply excess_of_nordered_group;
 250   [ constructor 1;
 251      [ apply Z
 252      | apply Zle
 253      | apply non_deve_stare_qui
 254      | apply transitive_Zle
 255      ]
 256   | simplify;
 257     intros;
 258     unfold;
 259     generalize in match (Z_compare_to_Prop x y);
 260     cases (Z_compare x y); simplify; intro;
 261      [ left;
 262        apply non_deve_stare_qui3;
 263        assumption
 264      | left;
 265        rewrite > H;
 266        apply non_deve_stare_qui
 267      | right;
 268        apply non_deve_stare_qui4;
 269        assumption
 270      ]
 271   ]
 272 qed.