algebra.why 2.71 KB
Newer Older
1 2 3

theory Assoc
  type t
4
  logic 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
10
  logic 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
16
  logic op t t : t
17 18
  clone Assoc with type t = t, logic op = op
  clone Comm  with type t = t, logic op = op
19
  meta AC logic op (*, prop Assoc.Assoc, prop Comm.Comm*)
20 21 22 23
end

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

25
  logic unit : t
MARCHE Claude's avatar
MARCHE Claude committed
26

27 28
  logic op t t : t
  logic inv t : t
MARCHE Claude's avatar
MARCHE Claude committed
29

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

  clone Assoc with type t = t, logic op = op

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

theory CommutativeGroup
  clone export Group
  clone Comm with type t = t, logic op = op
40
  meta AC logic op (*, prop Assoc.Assoc, prop Comm.Comm*)
41 42 43 44 45
end

theory Ring
  type t
  logic zero : t
46 47 48
  logic (+) t t : t
  logic (-_) t : t
  logic (*) t t : t
49 50 51 52 53 54 55 56

  clone CommutativeGroup with type t = t,
                              logic unit = zero,
                              logic op = (+),
                              logic inv = (-_)

  clone Assoc with type t = t, logic op = (*)

57
  axiom Mul_distr: forall x y z : t. x * (y + z) = x * y + x * z
58

59
  logic (-) (x y : t) : t = x + -y
60 61 62 63 64
end

theory CommutativeRing
  clone export Ring
  clone Comm with type t = t, logic op = (*)
65
  meta AC logic (*) (*, prop Assoc.Assoc, prop Comm.Comm*)
66 67 68 69 70 71
end

theory UnitaryCommutativeRing
  clone export CommutativeRing
  logic one : t
  axiom Unitary : forall x:t. one * x = x
72
  axiom NonTrivialRing : zero <> one
73 74
end

75 76 77 78 79 80
theory OrderedUnitaryCommutativeRing
  clone export UnitaryCommutativeRing
  logic (<=) t t
  logic (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, logic rel = (<=)

81 82 83 84
  axiom CompatOrderAdd  : 
    forall x y z : t. x <= y -> x + z <= y + z
  axiom CompatOrderMult : 
    forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
85 86
end

87
theory Field
MARCHE Claude's avatar
MARCHE Claude committed
88
  clone export UnitaryCommutativeRing
89
  logic inv t : t
90
  axiom Inverse : forall x:t. x <> zero -> x * inv x = one
91
  logic (/) (x y : t) : t = x * inv y
92
end
93 94 95 96 97 98 99 100 101 102 103

theory OrderedField
  clone export Field

  logic (<=) t t
  logic (>=) (x y : t) = y <= x
  clone export relations.TotalOrder with type t = t, logic rel = (<=)

  axiom CompatOrderAdd  : forall x y z : t. x <= y -> x + z <= y + z
  axiom CompatOrderMult : forall x y z : t. x <= y -> zero <= z -> x * z <= y * z
end
104

Jean-Christophe's avatar
Jean-Christophe committed
105 106 107 108 109 110 111 112 113 114 115 116 117


(* 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
*)