-
Notifications
You must be signed in to change notification settings - Fork 76
/
hz.ctt
67 lines (54 loc) · 2.91 KB
/
hz.ctt
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
63
64
65
66
67
-- Z defined as a quotient of nat * nat by the relation:
-- (x1,x2) ~ (y1,y2) := (x1 + y2 = x2 + y1)
module hz where
import nat
import setquot
-- shorthand for nat x nat
nat2 : U = and nat nat
natlemma (a b c d : nat) : Path nat (add (add a b) (add c d)) (add (add a d) (add c b)) =
let rem : Path nat (add a (add b (add c d))) (add a (add d (add c b))) =
<i> add a (add_comm3 b c d @ i)
in <i> comp (<_> nat) (rem @ i) [ (i = 0) -> assocAdd a b (add c d)
, (i = 1) -> assocAdd a d (add c b) ]
rel : eqrel nat2 = (r,rem)
where
r : hrel nat2 = \(x y : nat2) ->
(Path nat (add x.1 y.2) (add x.2 y.1),natSet (add x.1 y.2) (add x.2 y.1))
rem : iseqrel nat2 r = ((rem1,rem2),rem3)
where
rem1 : istrans nat2 r =
\(x y z : nat2)
(h1 : Path nat (add x.1 y.2) (add x.2 y.1))
(h2 : Path nat (add y.1 z.2) (add y.2 z.1)) ->
let rem : Path nat (add (add x.1 y.2) (add y.1 z.2)) (add (add x.2 y.1) (add y.2 z.1)) =
<i> add (h1 @ i) (h2 @ i)
rem1 : Path nat (add (add x.1 y.2) (add y.1 z.2)) (add (add x.1 z.2) (add y.1 y.2)) =
natlemma x.1 y.2 y.1 z.2
rem2 : Path nat (add (add x.2 y.1) (add y.2 z.1)) (add (add x.2 z.1) (add y.2 y.1)) =
natlemma x.2 y.1 y.2 z.1
rem3 : Path nat (add (add x.2 z.1) (add y.2 y.1)) (add (add x.2 z.1) (add y.1 y.2)) =
<i> add (add x.2 z.1) (add_comm y.2 y.1 @ i)
rem4 : Path nat (add (add x.2 y.1) (add y.2 z.1)) (add (add x.2 z.1) (add y.1 y.2)) =
<i> comp (<_> nat) (add (add x.2 z.1) (add y.2 y.1)) [ (i = 0) -> <j> rem2 @ -j
, (i = 1) -> rem3 ]
rem5 : Path nat (add (add x.1 z.2) (add y.1 y.2)) (add (add x.2 z.1) (add y.1 y.2)) =
<i> comp (<_> nat) (rem @ i) [ (i = 0) -> rem1, (i = 1) -> rem4 ]
in natcancelr (add x.1 z.2) (add x.2 z.1) (add y.1 y.2) rem5
rem2 : isrefl nat2 r = \(x : nat2) -> add_comm x.1 x.2
rem3 : issymm nat2 r = \(x y : nat2) (h : Path nat (add x.1 y.2) (add x.2 y.1)) ->
let rem : Path nat (add x.2 y.1) (add y.2 x.1) =
<i> comp (<_> nat) (add x.1 y.2) [ (i = 0) -> h
, (i = 1) -> add_comm x.1 y.2 ]
in <i> comp (<_> nat) (add x.2 y.1) [ (i = 0) -> add_comm x.2 y.1
, (i = 1) -> rem ]
hz : U = setquot nat2 rel.1
zeroz : hz = setquotpr nat2 rel (zero,zero)
onez : hz = setquotpr nat2 rel (one,zero)
discretehz : discrete hz = isdiscretesetquot nat2 rel rem
where
rem (x y : nat2) : isdecprop (rel.1 x y).1 =
(natSet (add x.1 y.2) (add x.2 y.1),natDec (add x.1 y.2) (add x.2 y.1))
-- Use the decision procedure to compute if "0 = 1":
test01 : bool = discretetobool hz discretehz zeroz onez
-- Use the decision procedure to compute if "1 = 1":
test11 : bool = discretetobool hz discretehz onez onez