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  [ constructor 1;
 109    [ constructor 1;
 110      [ constructor 1;
 111        [ apply T
 112        | apply (λx,y.¬(le x y));
 113        | apply reflexive_to_coreflexive;
 114          assumption
 115        | apply strong_decidable_to_transitive_to_cotransitive;
 116          assumption]
 117      no ported to duality
 118   ]
 119 qed.
 120
 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) →
 128        abelian_group.
 129  intros;
 130  constructor 1;
 131   [apply (apartness_of_strong_decidable ? f);]
 132  try assumption;
 133  [ change with (associative ? plus (λx,y:T.¬x≠y));
 134    simplify;
 135    intros;
 136    intro;
 137    apply H2;
 138    apply a;
 139  | intros 2;
 140    intro;
 141    apply a1;
 142    apply c;
 143  | intro;
 144    intro;
 145    apply a1;
 146    apply H
 147  | intro;
 148    intro;
 149    apply a1;
 150    apply H1
 151  | intros;
 152    apply strong_decidable_to_strong_ext;
 153    assumption
 154  ]
 155 qed.
 156
 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.
 159
 160 record nabelian_group : Type ≝
 161  { ncarr:> Type;
 162    nplus: ncarr → ncarr → ncarr;
 163    nzero: ncarr;
 164    nopp: 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
 169  }.
 170
 171 definition abelian_group_of_nabelian_group:
 172  ∀G:nabelian_group.(∀x,y:G.strong_decidable (x=y)) → abelian_group.
 173  intros;
 174  apply abelian_group_of_strong_decidable;
 175   [2: apply (nplus G)
 176   | skip
 177   | apply (nzero G)
 178   | apply (nopp G)
 179   | assumption
 180   | apply nplus_assoc;
 181   | apply nplus_comm;
 182   | apply nzero_neutral;
 183   | apply nopp_inverse
 184   ]
 185 qed.
 186
 187 definition Z_abelian_group: abelian_group.
 188  apply abelian_group_of_nabelian_group;
 189   [ constructor 1;
 190      [ apply Z
 191      | apply Zplus
 192      | apply OZ
 193      | apply Zopp
 194      | whd;
 195        intros;
 196        symmetry;
 197        apply associative_Zplus
 198      | apply sym_Zplus
 199      | intro;
 200        reflexivity
 201      | intro;
 202        rewrite > sym_Zplus;
 203        apply Zplus_Zopp;
 204      ]
 205   | simplify;
 206     intros;
 207     unfold;
 208     generalize in match (eqZb_to_Prop x y);
 209     elim (eqZb x y);
 210     simplify in H;
 211      [ left ; assumption
 212      | right; assumption
 213      ]
 214   ]
 215 qed.
 216
 217 record nordered_set: Type ≝
 218  { nos_carr:> Type;
 219    nos_le: nos_carr → nos_carr → Prop;
 220    nos_reflexive: reflexive ? nos_le;
 221    nos_transitive: transitive ? nos_le
 222  }.
 223
 224 definition excess_of_nordered_group:
 225  ∀O:nordered_set.(∀x,y:O. strong_decidable (nos_le ? x y)) → excess.
 226  intros;
 227  constructor 1;
 228   [ apply (nos_carr O)
 229   | apply (λx,y.¬(nos_le ? x y))
 230   | apply reflexive_to_coreflexive;
 231     apply nos_reflexive
 232   | apply strong_decidable_to_transitive_to_cotransitive;
 233      [ assumption
 234      | apply nos_transitive
 235      ]
 236   ]
 237 qed.
 238
 239 lemma non_deve_stare_qui: reflexive ? Zle.
 240  intro;
 241  elim x;
 242   [ exact I
 243   |2,3: simplify;
 244     apply le_n;
 245   ]
 246 qed.
 247
 248 axiom non_deve_stare_qui3: ∀x,y:Z. x < y → x ≤ y.
 249
 250 axiom non_deve_stare_qui4: ∀x,y:Z. x < y → y ≰ x.
 251
 252 definition Z_excess: excess.
 253  apply excess_of_nordered_group;
 254   [ constructor 1;
 255      [ apply Z
 256      | apply Zle
 257      | apply non_deve_stare_qui
 258      | apply transitive_Zle
 259      ]
 260   | simplify;
 261     intros;
 262     unfold;
 263     generalize in match (Z_compare_to_Prop x y);
 264     cases (Z_compare x y); simplify; intro;
 265      [ left;
 266        apply non_deve_stare_qui3;
 267        assumption
 268      | left;
 269        rewrite > H;
 270        apply non_deve_stare_qui
 271      | right;
 272        apply non_deve_stare_qui4;
 273        assumption
 274      ]
 275   ]
 276 qed.