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
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
|
module Encoded.Arith
import Data.Nat
import Encoded.Bool
import Encoded.Pair
import Syntax.PreorderReasoning
import Term.Semantics
import Term.Syntax
-- Utilities -------------------------------------------------------------------
export
rec : {ty : Ty} -> Term (N ~> ty ~> (N * ty ~> ty) ~> ty) ctx
rec = Abs $ Abs $ Abs $
let n = Var $ There $ There Here in
let z = Var $ There Here in
let s = Var Here in
let
p : Term (N * ty) (ctx :< N :< ty :< (N * ty ~> ty))
p = Rec n
(App pair [<Zero, z])
(Abs' (\p =>
App pair
[<Suc (App fst [<p])
, App (shift s) [<p]]))
in
App snd [<p]
export
plus : Term (N ~> N ~> N) ctx
plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .)))
export
pred : Term (N ~> N) ctx
-- pred = Abs' (\n => App rec [<n, Zero, fst])
pred = Abs'
(\n => App
(Rec n
(Const Zero)
(Abs $ Abs $
let f = Var (There Here) in
let k = Var Here in
Rec k
(Suc Zero)
(Const $ Rec (App f [<Zero])
Zero
(Const $ Suc $ App f [<Lit 1]))))
[<Lit 1])
export
minus : Term (N ~> N ~> N) ctx
minus = Abs $ Abs $
let m = Var $ There Here in
let n = Var Here in
Rec n m pred
export
mult : Term (N ~> N ~> N) ctx
mult = Abs' (\n =>
Rec n
(Const Zero)
(Abs $ Abs $
let f = Var $ There Here in
let m = Var Here in
App plus [<m, App f [<m]]))
export
lte : Term (N ~> N ~> B) ctx
lte = Abs' (\m => isZero . App minus [<m])
export
equal : Term (N ~> N ~> B) ctx
equal = Abs $ Abs $
let m = Var $ There Here in
let n = Var Here in
App and [<App lte [<m, n], App lte [<n, m]]
export
divmod : Term (N ~> N ~> N * N) ctx
divmod = Abs $ Abs $
let n = Var (There Here) in
let d = Var Here in
Rec
n
(App pair [<Zero, Zero])
(Abs' (\p =>
App if'
[<App lte [<shift d, App (Abs' Suc . snd) [<p]]
, App pair [<Suc (App fst [<p]), Zero]
, App mapSnd [<Abs' Suc, p]]))
-- Properties ------------------------------------------------------------------
-- Redefinition in Idris
namespace Sem
public export
recHelper : Nat -> a -> ((Nat, a) -> a) -> (Nat, a)
recHelper k z s = rec k (0, z) (\p => (S (fst p), s p))
public export
rec' : Nat -> a -> ((Nat, a) -> a) -> a
rec' k z s = snd (recHelper k z s)
public export
slowPred : Nat -> Nat
slowPred n = rec' n 0 fst
public export
predHelper : Nat -> Nat -> Nat
predHelper n =
rec n
(const 0)
(\f, k =>
rec k
1
(const $ rec (f 0)
0
(const $ S $ f 1)))
public export
pred' : Nat -> Nat
pred' n = predHelper n 1
public export
divmodStep : Nat -> (Nat, Nat) -> (Nat, Nat)
divmodStep d (div, mod) =
if d <= S mod
then
(S div, 0)
else
(div, S mod)
public export
divmod : Nat -> Nat -> (Nat, Nat)
divmod n d = rec n (0, 0) (divmodStep d)
-- Proofs
export
fstRecHelper : (k : Nat) -> (0 z : a) -> (0 s : (Nat, a) -> a) -> fst (recHelper k z s) = k
fstRecHelper 0 z s = Refl
fstRecHelper (S k) z s = cong S $ fstRecHelper k z s
export
slowPredCorrect : (k : Nat) -> slowPred k = pred k
slowPredCorrect 0 = Refl
slowPredCorrect (S k) = fstRecHelper k 0 fst
export
predCorrect : (k : Nat) -> pred' k = pred k
predCorrect 0 = Refl
predCorrect 1 = Refl
predCorrect (S (S k)) = cong S $ predCorrect (S k)
-- divmodSmall :
-- (d, div, mod : Nat) ->
-- {auto 0 ok : NonZero d} ->
-- mod <= d
export
divmodCorrect :
(n, d : Nat) ->
{auto 0 ok : NonZero d} ->
n = fst (divmod n d) * d + snd (divmod n d)
divmodCorrect 0 d = Refl
divmodCorrect (S k) d = ?divmodCorrect_rhs_1
|
