relations.why 3.47 KB
Newer Older
1 2
theory EndoRelation
  type t
3
  logic rel t t
4 5 6 7
end

theory Reflexive
  clone export EndoRelation
8
  axiom Refl : forall x:t. rel x x
9 10 11 12
end

theory Irreflexive
  clone export EndoRelation
13
  axiom Strict : forall x:t. not rel x x
14 15 16 17
end

theory Transitive
  clone export EndoRelation
18
  axiom Trans : forall x y z:t. rel x y -> rel y z -> rel x z
19 20 21 22
end

theory Symmetric
  clone export EndoRelation
23
  axiom Symm : forall x y:t. rel x y -> rel y x
24 25 26 27
end

theory Asymmetric
  clone export EndoRelation
28
  axiom Asymm : forall x y:t. rel x y -> not rel y x
29 30 31 32
end

theory Antisymmetric
  clone export EndoRelation
33
  axiom Antisymm : forall x y:t. rel x y -> rel y x -> x = y
34 35 36 37
end

theory Total
  clone export EndoRelation
38
  axiom Total : forall x y:t. rel x y or rel y x
39
end
MARCHE Claude's avatar
MARCHE Claude committed
40

MARCHE Claude's avatar
MARCHE Claude committed
41
theory PreOrder
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
  clone export Reflexive
  clone export Transitive with type t = t, logic rel = rel
end

theory Equivalence
  clone export PreOrder
  clone export Asymmetric with type t = t, logic rel = rel
end

theory TotalPreOrder
  clone export PreOrder
  clone export Total with type t = t, logic rel = rel
end

theory PartialOrder
  clone export PreOrder
  clone export Antisymmetric with type t = t, logic rel = rel
end
MARCHE Claude's avatar
MARCHE Claude committed
60

61 62 63 64 65 66 67 68 69 70 71 72
theory TotalOrder
  clone export PartialOrder
  clone export Total with type t = t, logic rel = rel
end

theory PartialStrictOrder
  clone export Transitive
  clone export Asymmetric with type t = t, logic rel = rel
end

theory TotalStrictOrder
  clone export PartialStrictOrder
73
  axiom Trichotomy : forall x y:t. rel x y or rel y x or x = y
74 75 76 77 78
end

theory Inverse
  clone export EndoRelation

79
  logic inv_rel (x y : t) = rel y x
80 81 82 83 84
end

theory ReflClosure
  clone export EndoRelation

85
  inductive relR t t =
86
  | BaseRefl : forall x:t. relR x x
87
  | StepRefl : forall x y:t. rel x y -> relR x y
88 89 90 91 92
end

theory TransClosure
  clone export EndoRelation

93
  inductive relT t t =
94 95
  | BaseTrans : forall x y:t. rel x y -> relT x y
  | StepTrans : forall x y z:t. relT x y -> rel y z -> relT x z
96 97 98 99 100
end

theory ReflTransClosure
  clone export EndoRelation

101
  inductive relTR t t =
102
  | BaseTransRefl : forall x:t. relTR x x
103
  | StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z
104 105 106 107 108 109
end

(*
theory PreOrder

  type t
110
  logic le t t
MARCHE Claude's avatar
MARCHE Claude committed
111
  axiom Refl : forall x:t. le(x,x)
112
  axiom Trans : forall x y z:t. le x y and le y z -> le x z
MARCHE Claude's avatar
MARCHE Claude committed
113

114
end
MARCHE Claude's avatar
MARCHE Claude committed
115

MARCHE Claude's avatar
MARCHE Claude committed
116 117
theory Equiv

MARCHE Claude's avatar
MARCHE Claude committed
118 119
  type t

120
  logic eq t t
MARCHE Claude's avatar
MARCHE Claude committed
121

MARCHE Claude's avatar
MARCHE Claude committed
122
  clone PreOrder with type t = t, logic le = eq
MARCHE Claude's avatar
MARCHE Claude committed
123

124
  axiom Symm : forall x y:t. eq x y -> eq y x
MARCHE Claude's avatar
MARCHE Claude committed
125

MARCHE Claude's avatar
MARCHE Claude committed
126
end
MARCHE Claude's avatar
MARCHE Claude committed
127

MARCHE Claude's avatar
MARCHE Claude committed
128 129
theory TotalPreOrder

130
  type t
131
  logic le t t
MARCHE Claude's avatar
MARCHE Claude committed
132 133 134

  clone export PreOrder with type t = t, logic le = le

135
  axiom Totality: forall x y:t. le x y or le y x
MARCHE Claude's avatar
MARCHE Claude committed
136 137

end
138 139
*)

MARCHE Claude's avatar
MARCHE Claude committed
140 141

(*
MARCHE Claude's avatar
MARCHE Claude committed
142
theory TotalOrder
MARCHE Claude's avatar
MARCHE Claude committed
143

MARCHE Claude's avatar
MARCHE Claude committed
144 145
  type t

146
  logic eq t t
MARCHE Claude's avatar
MARCHE Claude committed
147 148
  clone Equiv with type t = t, logic eq = eq

149
  logic le t t
MARCHE Claude's avatar
MARCHE Claude committed
150
  clone PreOrder with type t = t, logic le = le
MARCHE Claude's avatar
MARCHE Claude committed
151

152

153
  axiom Totality: forall x y:t. eq x y or le x y or le y x
MARCHE Claude's avatar
MARCHE Claude committed
154

155
  logic lt (x y : t) = le x y and not eq x y
MARCHE Claude's avatar
MARCHE Claude committed
156

157
  lemma Lt_antirefl: forall x:t. not lt x x
158 159 160
  lemma Lt_trans: forall x y z:t. lt x y and lt y z -> lt x z
  lemma Le_lt_trans: forall x y z:t. le x y and lt y z -> lt x z
  lemma Lt_le_trans: forall x y z:t. lt x y and le y z -> lt x z
MARCHE Claude's avatar
MARCHE Claude committed
161

162
end
MARCHE Claude's avatar
MARCHE Claude committed
163
*)
MARCHE Claude's avatar
MARCHE Claude committed
164

165 166 167 168 169
theory Lex

  type t1
  type t2
 
170 171
  logic rel1 t1 t1
  logic rel2 t2 t2
172 173

  inductive lex (t1, t2) (t1, t2) =
174 175 176 177
  | Lex_1: forall x1 x2 : t1, y1 y2 : t2. 
       rel1 x1 x2 -> lex (x1,y1) (x2,y2)
  | Lex_2: forall x : t1, y1 y2 : t2.
       rel2 y1 y2 -> lex (x,y1) (x,y2)
178 179 180

end

MARCHE Claude's avatar
MARCHE Claude committed
181
(*
MARCHE Claude's avatar
MARCHE Claude committed
182
theory MinMax
183

MARCHE Claude's avatar
MARCHE Claude committed
184 185
  clone export TotalOrder

186 187
  logic min t t : t
  logic max t t : t
MARCHE Claude's avatar
MARCHE Claude committed
188

189
end
MARCHE Claude's avatar
MARCHE Claude committed
190
*)
MARCHE Claude's avatar
MARCHE Claude committed
191 192 193


(*
194
Local Variables:
MARCHE Claude's avatar
MARCHE Claude committed
195
compile-command: "make -C .. test"
196
End:
MARCHE Claude's avatar
MARCHE Claude committed
197 198 199
*)