algebra.why 3.24 KB
Newer Older
1 2 3

theory Assoc
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
4
  function op t t : t
5
  axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)
6 7 8 9
end

theory Comm
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
10
  function op t t : t
11
  axiom Comm : forall x y : t. op x y = op y x
12 13 14 15
end

theory AC
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
16 17 18 19
  function op t t : t
  clone Assoc with type t = t, function op = op
  clone Comm  with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
20 21 22 23
end

theory Group
  type t
MARCHE Claude's avatar
MARCHE Claude committed
24

Andrei Paskevich's avatar
Andrei Paskevich committed
25
  function unit : t
MARCHE Claude's avatar
MARCHE Claude committed
26

Andrei Paskevich's avatar
Andrei Paskevich committed
27 28
  function op t t : t
  function inv t : t
MARCHE Claude's avatar
MARCHE Claude committed
29

30
  axiom Unit_def : forall x:t. op x unit = x
31

Andrei Paskevich's avatar
Andrei Paskevich committed
32
  clone Assoc with type t = t, function op = op
33

34
  axiom Inv_def : forall x:t. op x (inv x) = unit
35 36 37

  lemma Inv_unit : forall x y:t. op x (inv y) = unit -> x = y

38 39 40 41
end

theory CommutativeGroup
  clone export Group
Andrei Paskevich's avatar
Andrei Paskevich committed
42 43
  clone Comm with type t = t, function op = op
  meta AC function op (*, prop Assoc.Assoc, prop Comm.Comm*)
44 45 46 47
end

theory Ring
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
48 49 50 51
  function zero : t
  function (+) t t : t
  function (-_) t : t
  function (*) t t : t
52 53

  clone CommutativeGroup with type t = t,
Andrei Paskevich's avatar
Andrei Paskevich committed
54 55 56
                              function unit = zero,
                              function op = (+),
                              function inv = (-_)
57

Andrei Paskevich's avatar
Andrei Paskevich committed
58
  clone Assoc with type t = t, function op = (*)
59

60
  axiom Mul_distr: forall x y z : t. x * (y + z) = x * y + x * z
61

Andrei Paskevich's avatar
Andrei Paskevich committed
62
  function (-) (x y : t) : t = x + -y
63 64 65 66
end

theory CommutativeRing
  clone export Ring
Andrei Paskevich's avatar
Andrei Paskevich committed
67 68
  clone Comm with type t = t, function op = (*)
  meta AC function (*) (*, prop Assoc.Assoc, prop Comm.Comm*)
69 70 71 72
end

theory UnitaryCommutativeRing
  clone export CommutativeRing
Andrei Paskevich's avatar
Andrei Paskevich committed
73
  function one : t
74
  axiom Unitary : forall x:t. one * x = x
75
  axiom NonTrivialRing : zero <> one
76 77
end

78 79
theory OrderedUnitaryCommutativeRing
  clone export UnitaryCommutativeRing
Andrei Paskevich's avatar
Andrei Paskevich committed
80 81 82
  predicate (<=) t t
  predicate (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, predicate rel = (<=)
83

84
  axiom CompatOrderAdd  :
85
    forall x y z : t. x <= y -> x + z <= y + z
86
  axiom CompatOrderMult :
87
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
88 89
end

90
theory Field
MARCHE Claude's avatar
MARCHE Claude committed
91
  clone export UnitaryCommutativeRing
Andrei Paskevich's avatar
Andrei Paskevich committed
92
  function inv t : t
93
  axiom Inverse : forall x:t. x <> zero -> x * inv x = one
Andrei Paskevich's avatar
Andrei Paskevich committed
94
  function (/) (x y : t) : t = x * inv y
MARCHE Claude's avatar
MARCHE Claude committed
95

MARCHE Claude's avatar
MARCHE Claude committed
96
  lemma assoc_mul_div: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
97 98 99
    (* todo: discard the hypothesis ? *)
     z <> zero -> (x*y)/z = x*(y/z)

MARCHE Claude's avatar
MARCHE Claude committed
100
  lemma assoc_div_mul: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
101 102 103
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> (x/y)/z = x/(y*z)

MARCHE Claude's avatar
MARCHE Claude committed
104
  lemma assoc_div_div: forall x y z:t.
MARCHE Claude's avatar
MARCHE Claude committed
105 106 107
    (* todo: discard the hypothesis ? *)
     y <> zero /\ z <> zero -> x/(y/z) = (x*z)/y

108
end
109 110 111 112

theory OrderedField
  clone export Field

Andrei Paskevich's avatar
Andrei Paskevich committed
113 114 115
  predicate (<=) t t
  predicate (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, predicate rel = (<=)
116 117

  axiom CompatOrderAdd  : forall x y z : t. x <= y -> x + z <= y + z
Andrei Paskevich's avatar
Andrei Paskevich committed
118 119
  axiom CompatOrderMult :
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
120
end
121

Jean-Christophe's avatar
Jean-Christophe committed
122 123 124 125 126 127 128 129 130 131
(* to be discussed: should we add the following lemmas, and where

  lemma InvMult : forall x y : t. (-x) * y = - (x * y) = x * (-y)
  lemma InvSquare : forall x : t. x * x = (-x) * (-x)
  lemma ZeroMult : forall x : t. x * zero = zero = zero * x
  lemma SquareNonNeg1 : forall x : t. x <= zero -> zero <= x * x
  lemma SquareNonNeg : forall x : t. zero <= x * x
  lemma ZeroLessOne : zero <= one
*)