43 lines
1.1 KiB
Plaintext
43 lines
1.1 KiB
Plaintext
|
// Preorder: a set with a reflexive, transitive relation
|
||
|
|
//
|
||
|
|
// This demonstrates RELATIONS (predicates) as opposed to functions.
|
||
|
|
// A relation R : A -> Prop is a predicate on A.
|
||
|
|
// For binary relations, we use a product domain: R : [x: A, y: A] -> Prop
|
||
|
|
|
||
|
|
theory Preorder {
|
||
|
|
X : Sort;
|
||
|
|
|
||
|
|
// The ordering relation: x ≤ y
|
||
|
|
leq : [x: X, y: X] -> Prop;
|
||
|
|
|
||
|
|
// Reflexivity: x ≤ x
|
||
|
|
ax/refl : forall x : X.
|
||
|
|
|- [x: x, y: x] leq;
|
||
|
|
|
||
|
|
// Transitivity: x ≤ y ∧ y ≤ z → x ≤ z
|
||
|
|
ax/trans : forall x : X, y : X, z : X.
|
||
|
|
[x: x, y: y] leq, [x: y, y: z] leq |- [x: x, y: z] leq;
|
||
|
|
}
|
||
|
|
|
||
|
|
// The discrete preorder: only reflexive pairs
|
||
|
|
// (no elements are comparable except to themselves)
|
||
|
|
// Uses `chase` to automatically derive reflexive pairs from axiom ax/refl.
|
||
|
|
instance Discrete3 : Preorder = chase {
|
||
|
|
a : X;
|
||
|
|
b : X;
|
||
|
|
c : X;
|
||
|
|
}
|
||
|
|
|
||
|
|
// A total order on 3 elements: a ≤ b ≤ c
|
||
|
|
// Uses `chase` to derive reflexive and transitive closure.
|
||
|
|
instance Chain3 : Preorder = chase {
|
||
|
|
bot : X;
|
||
|
|
mid : X;
|
||
|
|
top : X;
|
||
|
|
|
||
|
|
// Assert the basic ordering; chase will add reflexive pairs
|
||
|
|
// and transitive closure (bot ≤ top)
|
||
|
|
[x: bot, y: mid] leq;
|
||
|
|
[x: mid, y: top] leq;
|
||
|
|
}
|