relations.mlw 3.78 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2 3

(** {1 Relations} *)

4
(** {2 Relations and orders} *)
MARCHE Claude's avatar
MARCHE Claude committed
5

6
module EndoRelation
7
  type t
Andrei Paskevich's avatar
Andrei Paskevich committed
8
  predicate rel t t
9 10
end

11
module Reflexive
12
  clone export EndoRelation
13
  axiom Refl : forall x:t. rel x x
14 15
end

16
module Irreflexive
17
  clone export EndoRelation
18
  axiom Strict : forall x:t. not rel x x
19 20
end

21
module Transitive
22
  clone export EndoRelation
23
  axiom Trans : forall x y z:t. rel x y -> rel y z -> rel x z
24 25
end

26
module Symmetric
27
  clone export EndoRelation
28
  axiom Symm : forall x y:t. rel x y -> rel y x
29 30
end

31
module Asymmetric
32
  clone export EndoRelation
33
  axiom Asymm : forall x y:t. rel x y -> not rel y x
34 35
end

36
module Antisymmetric
37
  clone export EndoRelation
38
  axiom Antisymm : forall x y:t. rel x y -> rel y x -> x = y
39 40
end

41
module Total
42
  clone export EndoRelation
Andrei Paskevich's avatar
Andrei Paskevich committed
43
  axiom Total : forall x y:t. rel x y \/ rel y x
44
end
MARCHE Claude's avatar
MARCHE Claude committed
45

46
module PreOrder
47 48
  clone export Reflexive with axiom Refl
  clone export Transitive with type t = t, predicate rel = rel, axiom Trans
49 50
end

51
module Equivalence
52 53
  clone export PreOrder with axiom Refl, axiom Trans
  clone export Symmetric with type t = t, predicate rel = rel, axiom Symm
54 55
end

56
module TotalPreOrder
57 58
  clone export PreOrder with axiom Refl, axiom Trans
  clone export Total with type t = t, predicate rel = rel, axiom Total
59 60
end

61
module PartialOrder
62 63 64
  clone export PreOrder with axiom Refl, axiom Trans
  clone export Antisymmetric with
    type t = t, predicate rel = rel, axiom Antisymm
65
end
MARCHE Claude's avatar
MARCHE Claude committed
66

67
module TotalOrder
68 69
  clone export PartialOrder with axiom .
  clone export Total with type t = t, predicate rel = rel, axiom Total
70 71
end

72
module PartialStrictOrder
73 74
  clone export Transitive with axiom Trans
  clone export Asymmetric with type t = t, predicate rel = rel, axiom Asymm
75 76
end

77
module TotalStrictOrder
78
  clone export PartialStrictOrder with axiom Trans, axiom Asymm
Andrei Paskevich's avatar
Andrei Paskevich committed
79
  axiom Trichotomy : forall x y:t. rel x y \/ rel y x \/ x = y
80 81
end

82
module Inverse
83 84
  clone export EndoRelation

Andrei Paskevich's avatar
Andrei Paskevich committed
85
  predicate inv_rel (x y : t) = rel y x
86 87
end

88 89
(** {2 Closures} *)

90
module ReflClosure
91 92
  clone export EndoRelation

93
  inductive relR t t =
94
  | BaseRefl : forall x:t. relR x x
95
  | StepRefl : forall x y:t. rel x y -> relR x y
96 97
end

98
module TransClosure
99 100
  clone export EndoRelation

101
  inductive relT t t =
102 103
  | 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
104 105 106

  lemma relT_transitive:
    forall x y z: t. relT x y -> relT y z -> relT x z
107 108
end

109
module ReflTransClosure
110 111
  clone export EndoRelation

112
  inductive relTR t t =
113
  | BaseTransRefl : forall x:t. relTR x x
114
  | StepTransRefl : forall x y z:t. relTR x y -> rel y z -> relTR x z
115 116 117

  lemma relTR_transitive:
    forall x y z: t. relTR x y -> relTR y z -> relTR x z
118 119
end

120 121
(** {2 Lexicographic ordering} *)

122
module Lex
123 124 125

  type t1
  type t2
Andrei Paskevich's avatar
Andrei Paskevich committed
126 127 128

  predicate rel1 t1 t1
  predicate rel2 t2 t2
129 130

  inductive lex (t1, t2) (t1, t2) =
Andrei Paskevich's avatar
Andrei Paskevich committed
131
  | Lex_1: forall x1 x2 : t1, y1 y2 : t2.
132 133 134
       rel1 x1 x2 -> lex (x1,y1) (x2,y2)
  | Lex_2: forall x : t1, y1 y2 : t2.
       rel2 y1 y2 -> lex (x,y1) (x,y2)
135 136 137

end

138 139
(** {2 Minimum and maximum for total orders} *)

140
module MinMax
141

142
  type t
143
  predicate le t t
144

145
  clone TotalOrder as TO with type t = t, predicate rel = le, axiom .
146

147 148
  function min (x y : t) : t = if le x y then x else y
  function max (x y : t) : t = if le x y then y else x
149

150 151
  lemma Min_r : forall x y:t. le y x -> min x y = y
  lemma Max_l : forall x y:t. le y x -> max x y = x
152 153

  lemma Min_comm : forall x y:t. min x y = min y x
154
  lemma Max_comm : forall x y:t. max x y = max y x
MARCHE Claude's avatar
MARCHE Claude committed
155

156
  lemma Min_assoc : forall x y z:t. min (min x y) z = min x (min y z)
157
  lemma Max_assoc : forall x y z:t. max (max x y) z = max x (max y z)
MARCHE Claude's avatar
MARCHE Claude committed
158

159
end
MARCHE Claude's avatar
MARCHE Claude committed
160

161 162
(** {2 Well-founded relation} *)

163
module WellFounded
164

165 166 167 168 169 170 171 172
  inductive acc (r: 'a -> 'a -> bool) (x: 'a) =
  | acc_x: forall r, x: 'a. (forall y. r y x -> acc r y) -> acc r x

  predicate well_founded (r: 'a -> 'a -> bool) =
    forall x. acc r x

end