-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathEvenOdd.idr
145 lines (106 loc) · 4.66 KB
/
EvenOdd.idr
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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
module EvenOdd
data Even : Nat -> Type where
EvenZeroP : Even Z
EvenStepP : Even n -> Even (S (S n))
data Odd : Nat -> Type where
OddOnesP : Odd (S Z)
OddStepP : Odd n -> Odd (S (S n))
||| Proof that
||| \forall n \in N. n is even or n is odd
number_odd_or_even : (n : Nat) -> Either (Even n) (Odd n)
number_odd_or_even Z = Left EvenZeroP
number_odd_or_even (S Z) = Right OddOnesP
number_odd_or_even (S (S n)) = case number_odd_or_even n of
Left p => Left (EvenStepP p)
Right p => Right (OddStepP p)
odd_follows_even : Even n -> Odd (S n)
odd_follows_even EvenZeroP = OddOnesP
odd_follows_even (EvenStepP x) = let r = odd_follows_even x
in (OddStepP r)
even_follows_odd : Odd n -> Even (S n)
even_follows_odd OddOnesP = EvenStepP EvenZeroP
even_follows_odd (OddStepP x) = EvenStepP (even_follows_odd x)
even_preds_odd : Odd (S n) -> Even n
even_preds_odd OddOnesP = EvenZeroP
even_preds_odd (OddStepP OddOnesP) = EvenStepP EvenZeroP
even_preds_odd (OddStepP (OddStepP x)) = EvenStepP (even_preds_odd (OddStepP x))
odd_preds_even : Even (S (S n)) -> Odd (S n)
odd_preds_even (EvenStepP EvenZeroP) = OddOnesP
odd_preds_even (EvenStepP (EvenStepP x)) = OddStepP (odd_preds_even (EvenStepP x))
||| Proof that
||| \forall n, m \in N. S (n + m) = n + (S m)
stmt_1 : S (n + m) = n + (S m)
stmt_1 {n = Z} = Refl
stmt_1 {n = S k} {m} = let rec = stmt_1 {n = k} {m}
in cong {f = S} rec
pred : (n : Nat) -> Nat
pred Z = Z
pred (S n) = n
stmt_3 : S n = S (k + S k) -> n = k + S k
stmt_3 = cong {f = EvenOdd.pred}
stmt_4 : S (k + S k) = S k + S k
stmt_4 = Refl
stmt_5 : S (S k + k) = S k + S k
stmt_5 {k} = rewrite plusCommutative {left = S k} {right = k} in stmt_4
stmt_6 : S n = S k + S k -> S n = S (k + S k)
stmt_6 {n} {k} p = p
stmt_7 : S n = S k + S k -> n = k + S k
stmt_7 p = stmt_3 (stmt_6 p)
stmt_8 : S n = S k + S k -> n = S k + k
stmt_8 {k} p = rewrite plusCommutative {left = S k} {right = k} in stmt_7 p
stmt_9 : S (S n) = S k + S k -> S n = S k + k
stmt_9 {n} {k} p = stmt_8 {n = S n} {k = k} p
stmt_10 : S n = S k + k -> n = k + k
stmt_10 {n} {k} p = cong {f = EvenOdd.pred} p
stmt_11 : S (S n) = S k + S k -> n = k + k
stmt_11 p = let r = stmt_9 p in stmt_10 r
stmt_12 : S (S n) = S (S k + S k) -> n = S (k + k)
stmt_12 {k} p = let r = cong {f = EvenOdd.pred} p
r' = stmt_7 r
in rewrite stmt_1 {n = k} {m = k} in r'
||| Proof that
||| \forall n' . n' is even => \forall n. n' = S (n + n) => False
stmt_2 : Even m -> (n : Nat) -> m = S (n + n) -> Void
stmt_2 {m = Z} EvenZeroP Z Refl impossible
stmt_2 {m = Z} EvenZeroP (S _) Refl impossible
stmt_2 (EvenStepP _) Z Refl impossible
stmt_2 (EvenStepP x) (S k) p = let rec = stmt_2 x k (stmt_12 p) in rec
plus_Z : plus n Z = n
plus_Z {n = Z} = Refl
plus_Z {n = S k} = let r = plus_Z {n = k}
in cong r
distr : S n = S (m + m) -> S n = m + S m
distr {m} p = rewrite sym (stmt_1 {n = m} {m = m}) in p
add_two : n = m + m -> S (S n) = S m + S m
add_two {m} p = let r = cong {f = S} p
s = distr r
t = cong {f = S} s
in t
lem_3 : S (S Z) * n = n + n
lem_3 {n} = rewrite sym (plus_Z {n = n}) in Refl
lem_4 : (\x1 => n = (S (S Z)) * x1) x -> (\x1 => n = x1 + x1) x
lem_4 {x} p = rewrite sym (lem_3 {n = x}) in p
lem_2 : (x ** n = (S (S Z)) * x) -> (x ** n = x + x)
lem_2 (x ** p) = let q = lem_4 p
in (x ** q)
lem_6 : plus y y = plus y (plus y Z)
lem_6 {y} = rewrite plus_Z {n = y} in Refl
lem_7 : S (S n) = m + m -> S (S n) = m + (plus m Z)
lem_7 {m} p = rewrite sym (lem_6 {y = m}) in p
||| Proof that
||| \forall n. n is even => \exists x. n = 2 * x
even_mult_2 : Even n -> (x ** n = S (S Z) * x)
even_mult_2 EvenZeroP = (0 ** Refl)
even_mult_2 (EvenStepP x) = let r = even_mult_2 x
(y ** p) = lem_2 r
q = add_two p
w = lem_7 q
in (S y ** w)
even_or_odd : Even n -> Odd n -> Void
even_or_odd EvenZeroP OddOnesP impossible
even_or_odd EvenZeroP (OddStepP _) impossible
even_or_odd (EvenStepP x) (OddStepP y) = let r = even_or_odd x y in r
zeroE : Even 0
zeroE = EvenZeroP
sixteenE : Even 16
sixteenE = EvenStepP (EvenStepP (EvenStepP (EvenStepP (EvenStepP (EvenStepP (EvenStepP (EvenStepP EvenZeroP)))))))