helm/software/matita/tests/luo.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 include "logic/equality.ma".
  16
  17 inductive unit (A : Type) (a : A) : Type := mk_unit : unit A a.
  18
  19 definition k : ∀A,a.unit A a → A := λA,a.λx:unit A a.a.
  20 coercion k.
  21
  22 record monoid : Type := {
  23   mC :> Type;
  24   mOp : mC -> mC -> mC;
  25   m1 : mC;
  26   mP : ∀x:mC.x = mOp x m1
  27 }.
  28
  29 record group : Type := {
  30   gC :> Type;
  31   gOp : gC -> gC -> gC;
  32   gInv : gC -> gC;
  33   g1 : gC;
  34   gP : ∀x:gC.gOp x (gInv x) = g1
  35 }.
  36
  37 (*
  38 record monoid_aux (x : Type) : Type := {
  39   xC :> unit ? x;
  40   xOp : let xC := k ?? xC in xC -> xC -> xC;
  41   x1  : let xC := k ?? xC in xC;
  42   xP  : let xC := k ?? xC in ∀x:xC. x = xOp x x1
  43 }.
  44 *)
  45
  46 record monoid_aux (xC : Type) : Type := {
  47   (*xC :> unit ? x;*)
  48   xOp : (*let xC := k ?? xC in*) xC -> xC -> xC;
  49   x1  : (*let xC := k ?? xC in*) xC;
  50   xP  : (*let xC := k ?? xC in*) ∀x:xC. x = xOp x x1
  51 }.
  52
  53
  54 definition m_sub := λT:Type.λx:monoid_aux T.
  55   mk_monoid (*k ?? (xC T x)*) T (xOp ? x) (x1 ? x) (xP ? x).
  56 coercion m_sub.
  57
  58 lemma test : ∀G:group.∀M:monoid_aux (gC G).gC G = mC (m_sub ? M).
  59 intros; reflexivity;
  60 qed.
  61
  62 record ring : Type := {
  63   rG :> group;
  64   rM :> monoid_aux (gC rG);
  65   rP : ∀x,y,z:rG. mOp rM x (gOp rG y z) = gOp rG (mOp rM x y) (mOp rM x z)
  66 }.
  67
  68 lemma prova : ∀R:ring.∀x:R. x = mOp R x (m1 R).
  69 intros;
  70 apply (mP (rM R));
  71 qed.
  72
  73 include "Z/times.ma".
  74
  75 lemma e_g : group.
  76 constructor 1;
  77 [ apply Z;
  78 | apply Zplus;
  79 | apply (λx.-x);
  80 | apply OZ;
  81 | intros; autobatch;]
  82 qed.
  83
  84 lemma e_m : monoid.
  85 constructor 1;
  86 [ apply Z;
  87 | apply Ztimes;
  88 | apply (pos O);
  89 | intros; autobatch;]
  90 qed.
  91
  92 lemma em_1 : monoid_aux Z.
  93 constructor 1;
  94 [ apply Ztimes;
  95 | apply (pos O);
  96 | intros; autobatch;]
  97 qed.
  98
  99 lemma e_r : ring.
 100 constructor 1;
 101 [ apply e_g; | apply em_1;| intros; unfold e_g; unfold em_1; simplify; autobatch;]
 102 qed.
 103
 104 lemma test1 : ∀x:Z.x = x * pos O.
 105 intros; apply (mP e_r x);
 106 qed.
 107
 108
 109
 110