helm/software/matita/dama/divisible_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 set "baseuri" "cic:/matita/divisible_group/".
  16
  17 include "nat/orders.ma".
  18 include "group.ma".
  19
  20 let rec pow (G : abelian_group) (x : G) (n : nat) on n : G ≝
  21   match n with [ O ⇒ 0 | S m ⇒ x + pow ? x m].
  22
  23 interpretation "abelian group pow" 'exp x n =
  24   (cic:/matita/divisible_group/pow.con _ x n).
  25
  26 record dgroup : Type ≝ {
  27   dg_carr:> abelian_group;
  28   dg_prop: ∀x:dg_carr.∀n:nat.∃y.pow ? y (S n) ≈ x
  29 }.
  30
  31 lemma divide: ∀G:dgroup.G → nat → G.
  32 intros (G x n); cases (dg_prop G x n); apply w;
  33 qed.
  34
  35 interpretation "divisible group divide" 'divide x n =
  36   (cic:/matita/divisible_group/divide.con _ x n).
  37
  38 lemma divide_divides:
  39   ∀G:dgroup.∀x:G.∀n. pow ? (x / n) (S n) ≈ x.
  40 intro G; cases G; unfold divide; intros (x n); simplify;
  41 cases (f x n); simplify; exact H;
  42 qed.
  43
  44 lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → pow ? x n ≈ pow ? y n.
  45 intros (G x y n H); elim n; [apply eq_reflexive]
  46 simplify; apply (Eq≈ (x + (pow ? y n1)) H1);
  47 apply (Eq≈ (y+pow ? y n1) H (eq_reflexive ??));
  48 qed.
  49
  50 lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x.
  51 intro G; cases G; unfold divide; intros; simplify;
  52 cases (f x O); simplify; simplify in H; intro; apply H;
  53 apply (ap_rewl ???? (plus_comm ???));
  54 apply (ap_rewl ???w (zero_neutral ??)); assumption;
  55 qed.