1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
// basic prelude
let set Empty = variant[]
let set Unit = record {}
let element pt : Unit = {}
// Bool is not inductive
let set Two = variant [ zero : Unit | one : Unit]
// the main thrust
let signature SetWithEquivRelation = theory {
Carrier :: Set,
Relation :: (x : set-of(Carrier)) (y: set-of(Carrier)) -> Set,
Reflexive :: (x : set-of(Carrier)) -> <set-of(Relation x x)>,
Symmetric :: (x : set-of(Carrier)) (y : set-of(Carrier)) (r : set-of(Relation x y))
-> <set-of(Relation y x)>,
Transitive :: (x : set-of(Carrier)) (y : set-of(Carrier)) (z : set-of(Carrier))
(r : set-of(Relation x y)) (s : set-of(Relation y z))
-> <set-of(Relation x z)>
}
// by cases we construct this on Two
let instance eqTwo :: SetWithEquivRelation = {
.Carrier = Two :: Set,
.Relation = for (x: Two) (y: Two),
case x of [ zero. _ => case y of [ zero. _ => Unit :: Set | one. _ => Empty :: Set ]
| one. _ => case y of [ zero. _ => Empty :: Set | one. _ => Unit :: Set ] ],
.Reflexive = for (x: Two), case x of [ zero. _ => <pt> | one. _ => <pt> ],
.Symmetric = for (x: Two) (y: Two) (r: set-of(Relation x y)),
case x of [ zero. _ => case y of [ zero. _ => <r> | one. _ => <r> ]
| one. _ => case y of [ zero. _ => <r> | one. _ => <r> ] ],
.Transitive = for (x: Two)(y: Two)(z: Two)(r: set-of(Relation x y))(s: set-of(Relation y z)),
case x of [ zero. _ => case y of // there are choices here to use <r> or <s> in places that are irrelevant
[ zero. _ => case z of [ zero. _ => <r> | one. _ => <s> ]
| one. _ => case z of [ zero. _ => <pt>| one. _ => <r> ] ]
| one. _ => case y of
[ zero. _ => case z of [ zero. _ => <r> | one. _ => <pt>]
| one. _ => case z of [ zero. _ => <s> | one. _ => <r> ] ] ]
}
// show off forming sets
let set Diagonal = record { x : set-of(eqTwo .Carrier), y : set-of(eqTwo .Carrier), equal : set-of((eqTwo .Relation) x y) }
let element oneEqualsOne : Diagonal = { .x = one. pt, .y = one. pt, .equal = pt }
// prove inequality
let instance zeroNeqOne
:: (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))) -> <Empty>
= for (r : set-of((eqTwo .Relation) (zero. pt) (one. pt))), <r>
// prove inequality the fun way
let signature NeqParticular = theory {
SE :: SetWithEquivRelation,
A :: <set-of(SE .Carrier)>,
B :: <set-of(SE .Carrier)>,
Neq :: (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))) -> <Empty>
}
let instance zeroNeqOneAgain :: NeqParticular = {
.SE = eqTwo,
.A = <zero. pt>,
.B = <one. pt>,
.Neq = for (r: set-of((SE .Relation) (element-of(A)) (element-of(B)))), <r>
}
|
