-
Notifications
You must be signed in to change notification settings - Fork 3
/
dk_nat.dk
142 lines (119 loc) · 3.49 KB
/
dk_nat.dk
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
#NAME dk_nat.
def Bool : Type := dk_bool.Bool.
nat : cc.uT.
Nat : Type.
[] cc.eT nat --> Nat.
O : Nat.
S : Nat -> Nat.
(; Order ;)
def lt : Nat -> Nat -> Bool.
[] lt O (S _) --> dk_bool.true
[] lt _ O --> dk_bool.false
[n,m] lt (S n) (S m) --> lt n m.
def gt : Nat -> Nat -> Bool.
[n,m] gt n m --> lt m n.
def leq : Nat -> Nat -> Bool.
[] leq O _ --> dk_bool.true
[] leq (S _) O --> dk_bool.false
[n,m] leq (S n) (S m) --> leq n m.
def geq : Nat -> Nat -> Bool.
[n,m] geq n m --> leq m n.
(; Equality ;)
def eq : Nat -> Nat -> Bool.
[n,m] eq n m --> dk_bool.and (leq n m) (geq n m).
(; Alternative_definition ;)
(; [] eq O O --> dk_bool.true ;)
(; [ m : Nat ] eq O (S m) --> dk_bool.false ;)
(; [ n : Nat ] eq (S n) O --> dk_bool.false ;)
(; [ n : Nat, m : Nat ] eq (S n) (S m) --> eq n m. ;)
(; Operations ;)
(; Addition ;)
(; This definition of plus is compatible with dependant list concatenation ;)
def plus : Nat -> Nat -> Nat.
[m] plus O m --> m
[n,m] plus (S n) m --> S (plus n m)
(; We also need symmetric rewrite rules for confluence of dk_int.leq ;)
(; Counter-example: dk_int.leq (dk_int.make a b) (dk_int.make (S c) (S d)) ;)
[n] plus n O --> n
[n,m] plus n (S m) --> S (plus n m).
(; Product ;)
def mult : Nat -> Nat -> Nat.
[] mult O _ --> O
[n,m] mult (S n) m --> plus (mult n m) m.
(; Min and Max ;)
def max : Nat -> Nat -> Nat.
[m,n] max m n --> dk_bool.ite nat (leq m n) n m.
def min : Nat -> Nat -> Nat.
[] min O _ --> O
[] min _ O --> O
[m,n] min (S m) (S n) --> S (min m n).
(; [m,n] ;)
(; min m n --> dk_bool.ite nat (leq m n) m n. ;)
(; Euclidian division ;)
(; invariants : n + r mod m, r < m ;)
def mod_aux : Nat -> Nat -> Nat -> Nat.
[r] mod_aux O _ r --> r
[n,m,r]
mod_aux (S n) m r --> mod_aux n m (dk_bool.ite nat (lt (S r) m) (S r) O).
def mod : Nat -> Nat -> Nat.
[n,m] mod n m --> mod_aux n m O.
def quo_aux : Nat -> Nat -> Nat -> Nat.
[] quo_aux O _ _ --> O
[n,m,r]
quo_aux (S n) m r
-->
dk_bool.ite nat (lt (S r) m) (quo_aux n m (S r)) (S (quo_aux n m O)).
def quo : Nat -> Nat -> Nat.
[n,m] quo n m --> quo_aux n m O.
(; exponentiation ;)
def pow : Nat -> Nat -> Nat.
[] pow _ O --> S O
[n,k] pow n (S k) --> mult n (pow n k).
(; Decimal representation ;)
Digit : cc.uT.
_0 : cc.eT Digit.
_1 : cc.eT Digit.
_2 : cc.eT Digit.
_3 : cc.eT Digit.
_4 : cc.eT Digit.
_5 : cc.eT Digit.
_6 : cc.eT Digit.
_7 : cc.eT Digit.
_8 : cc.eT Digit.
_9 : cc.eT Digit.
def 0 : Nat := O.
def 1 : Nat := S 0.
def 2 : Nat := S 1.
def 3 : Nat := S 2.
def 4 : Nat := S 3.
def 5 : Nat := S 4.
def 6 : Nat := S 5.
def 7 : Nat := S 6.
def 8 : Nat := S 7.
def 9 : Nat := S 8.
def 10 : Nat := S 9.
def digit_to_nat : cc.eT Digit -> Nat.
[] digit_to_nat _0 --> 0
[] digit_to_nat _1 --> 1
[] digit_to_nat _2 --> 2
[] digit_to_nat _3 --> 3
[] digit_to_nat _4 --> 4
[] digit_to_nat _5 --> 5
[] digit_to_nat _6 --> 6
[] digit_to_nat _7 --> 7
[] digit_to_nat _8 --> 8
[] digit_to_nat _9 --> 9.
(; Conversion from a list of digits (weakest digit at head) to_nat a nat ;)
def list_to_nat : cc.eT (dk_list.list Digit) -> Nat.
[ ] list_to_nat (dk_list.nil Digit) --> O
[d,l]
list_to_nat (dk_list.cons Digit d l)
-->
plus (digit_to_nat d) (mult 10 (list_to_nat l)).
(; Notation with weakest digit on the right side ;)
def diglist : cc.uT := dk_list.list Digit.
def dnil : cc.eT diglist := dk_list.nil Digit.
def dcons : cc.eT diglist -> cc.eT Digit -> cc.eT diglist
:= l : cc.eT diglist => d : cc.eT Digit => dk_list.cons Digit d l.
(; Example ;)
def 42 : Nat := list_to_nat (dcons (dcons dnil _4) _2).