Nats.hs 8.95 KB
Newer Older
1
2
module Nats where

jan  mas rovira's avatar
jan mas rovira committed
3
import Base
jan  mas rovira's avatar
jan mas rovira committed
4
import Data.Type.Equality
5
6
7
8
9

data Nat where
  Zero :: Nat
  Suc :: Nat -> Nat
  deriving (Show, Eq, Ord)
jan  mas rovira's avatar
jan mas rovira committed
10
11
12
13
14

data SNat (n :: Nat) where
  SZero :: SNat 'Zero
  SSuc :: SNat n -> SNat ('Suc n)

jan  mas rovira's avatar
jan mas rovira committed
15
type N0 = 'Zero
jan  mas rovira's avatar
jan mas rovira committed
16
17
type One = 'Suc N0
type Two = 'Suc One
18
19

type family (a :: Nat) :+: (b :: Nat) :: Nat where
jan  mas rovira's avatar
jan mas rovira committed
20
21
  'Zero :+: b = b
  'Suc a :+: b = 'Suc (a :+: b)
22

jan  mas rovira's avatar
jan mas rovira committed
23
24
25
26
27
28
29
onePlusOne :: (One :+: One) :~: Two
onePlusOne = Refl

nPlusZero :: SNat n -> (n :+: 'Zero) :~: n
nPlusZero SZero = Refl
nPlusZero (SSuc m) = congSuc (nPlusZero m)

jan  mas rovira's avatar
jan mas rovira committed
30
type family (a :: Nat) :*: (b :: Nat) :: Nat where
jan  mas rovira's avatar
jan mas rovira committed
31
32
  'Zero :*: b = 'Zero
  'Suc a :*: b = b :+: (a :*: b) -- Requires UndecidableInstances
jan  mas rovira's avatar
jan mas rovira committed
33

jan  mas rovira's avatar
jan mas rovira committed
34
type family (a :: Nat) :^: (b :: Nat) :: Nat where
jan  mas rovira's avatar
jan mas rovira committed
35
36
  a :^: 'Zero = 'Suc 'Zero
  a :^: 'Suc b = a :*: (a :^: b)  -- Requires UndecidableInstances
37

jan  mas rovira's avatar
jan mas rovira committed
38
39
40
41
42
(.+.) :: SNat a -> SNat b -> SNat (a :+: b)
(.+.) SZero b    = b
(.+.) (SSuc n) b = SSuc (n .+. b)

(.*.) :: SNat a -> SNat b -> SNat (a :*: b)
jan  mas rovira's avatar
jan mas rovira committed
43
(.*.) SZero _    = SZero
jan  mas rovira's avatar
jan mas rovira committed
44
45
(.*.) (SSuc a) b = b .+. (a .*. b)

jan  mas rovira's avatar
jan mas rovira committed
46
47
48
49
(.^.) :: SNat a -> SNat b -> SNat (a :^: b)
(.^.) _ SZero    = SSuc SZero
(.^.) a (SSuc b) = a .*. (a .^. b)

50
51
52
congSuc :: a :~: b -> 'Suc a :~: 'Suc b
congSuc = cong

jan  mas rovira's avatar
jan mas rovira committed
53
54
plusZeroL :: ('Zero :+: b) :~: b
plusZeroL = Refl
55

jan  mas rovira's avatar
jan mas rovira committed
56
plusZeroR :: SNat sn -> (sn :+: 'Zero) :~: sn
57
plusZeroR SZero = Refl
jan  mas rovira's avatar
jan mas rovira committed
58
plusZeroR (SSuc (n :: SNat n)) = congSuc (plusZeroR n)
59

jan  mas rovira's avatar
jan mas rovira committed
60
61
plusSucL :: SNat a -> SNat b -> ('Suc a :+: b) :~: 'Suc (a :+: b)
plusSucL _ _ = Refl
jan  mas rovira's avatar
jan mas rovira committed
62

jan  mas rovira's avatar
jan mas rovira committed
63
64
65
plusSucR :: forall a b. SNat a -> SNat b -> (a :+: 'Suc b) :~: 'Suc (a :+: b)
plusSucR SZero _ = Refl
plusSucR (SSuc (pa :: SNat pa)) b = congSuc indh
jan  mas rovira's avatar
jan mas rovira committed
66
67
  where
    indh :: (pa :+: 'Suc b) :~: 'Suc (pa :+: b)
jan  mas rovira's avatar
jan mas rovira committed
68
    indh = plusSucR pa b
jan  mas rovira's avatar
jan mas rovira committed
69
70
71
72
73

plusEqL :: SNat k -> a :~: b -> k :+: a :~: k :+: b
plusEqL SZero Refl = Refl
plusEqL (SSuc n) p = congSuc (plusEqL n p)

jan  mas rovira's avatar
jan mas rovira committed
74
plusEqR :: forall k a b. SNat k -> SNat a -> a :~: b -> a :+: k :~: b :+: k
jan  mas rovira's avatar
jan mas rovira committed
75
plusEqR _k _a Refl = Refl
jan  mas rovira's avatar
jan mas rovira committed
76

77
plusAssoc :: forall a b c. SNat a -> SNat b -> SNat c -> (a :+: b) :+: c :~: a :+: (b :+: c)
jan  mas rovira's avatar
jan mas rovira committed
78
plusAssoc SZero _ _ = Refl
jan  mas rovira's avatar
jan mas rovira committed
79
plusAssoc (SSuc (pa :: SNat pa)) b c = congSuc (plusAssoc pa b c)
80
81
82

plusCommut :: forall a b. SNat a -> SNat b -> (a :+: b) :~: (b :+: a)
plusCommut SZero b = sym (plusZeroR b)
jan  mas rovira's avatar
jan mas rovira committed
83
plusCommut (SSuc (pa :: SNat pa)) b = congSuc indh `trans` sym (plusSucR b pa)
84
85
86
  where
    indh :: (pa :+: b) :~: (b :+: pa)
    indh = plusCommut pa b
jan  mas rovira's avatar
jan mas rovira committed
87

jan  mas rovira's avatar
jan mas rovira committed
88
plusTransL :: SNat b -> c :~: a :+: b -> a :~: a' -> c :~: a' :+: b
jan  mas rovira's avatar
jan mas rovira committed
89
90
plusTransL _ Refl Refl = Refl

jan  mas rovira's avatar
jan mas rovira committed
91
plusTransR :: SNat a -> c :~: a :+: b -> b :~: b' -> c :~: a :+: b'
jan  mas rovira's avatar
jan mas rovira committed
92
93
plusTransR _ Refl Refl = Refl

jan  mas rovira's avatar
jan mas rovira committed
94
95
96
97
98
99
100
101
102
103
prodZeroL :: SNat n -> 'Zero :*: n :~: 'Zero
prodZeroL _n = Refl

prodZeroR :: SNat sn -> (sn :*: 'Zero) :~: 'Zero
prodZeroR SZero = Refl
prodZeroR (SSuc (n :: SNat n)) = indh
  where
    indh :: (n :*: 'Zero) :~: 'Zero
    indh = prodZeroR n

jan  mas rovira's avatar
jan mas rovira committed
104
prodOneL :: SNat sn -> (One :*: sn) :~: sn
jan  mas rovira's avatar
jan mas rovira committed
105
106
prodOneL = plusZeroR

jan  mas rovira's avatar
jan mas rovira committed
107
prodOneR :: SNat sn -> (sn :*: One) :~: sn
jan  mas rovira's avatar
jan mas rovira committed
108
109
110
111
112
prodOneR SZero = Refl
prodOneR (SSuc (n :: SNat n)) = congSuc indh
  where
    indh = prodOneR n

jan  mas rovira's avatar
jan mas rovira committed
113
114
115
prodSucL :: forall a b. SNat a -> SNat b -> ('Suc a :*: b) :~: b :+: (a :*: b)
prodSucL _ _ = Refl

jan  mas rovira's avatar
jan mas rovira committed
116
117
118
119
120
121
122
123
124
125
126
prodSucR :: forall a b. SNat a -> SNat b -> (a :*: 'Suc b) :~: a :+: (a :*: b)
prodSucR SZero _ = Refl
prodSucR (SSuc (n :: SNat n)) b = congSuc s3
  where
    indh :: (n :*: 'Suc b) :~: (n :+: (n :*: b))
    indh = prodSucR n b
    nb = n .*. b
    s1 :: (b :+: (n :*: 'Suc b)) :~: ((b :+: n) :+: (n :*: b))
    s1 = plusEqL b indh
      `trans` sym (plusAssoc b n nb)
    s2 :: (b :+: (n :*: 'Suc b)) :~: ((n :+: b) :+: (n :*: b))
jan  mas rovira's avatar
jan mas rovira committed
127
    s2 = plusTransL nb s1 (plusCommut b n)
jan  mas rovira's avatar
jan mas rovira committed
128
129
130
    s3 :: (b :+: (n :*: 'Suc b)) :~: (n :+: (b :+: (n :*: b)))
    s3 = s2 `trans` plusAssoc n b nb

jan  mas rovira's avatar
jan mas rovira committed
131
132
133
134
135
136
prodTransL :: SNat b -> c :~: a :*: b -> a :~: a' -> c :~: a' :*: b
prodTransL _ Refl Refl = Refl

prodTransR :: SNat a -> c :~: a :*: b -> b :~: b' -> c :~: a :*: b'
prodTransR _ Refl Refl = Refl

jan  mas rovira's avatar
jan mas rovira committed
137
138
prodDistribR :: forall a b c. SNat a -> SNat b -> SNat c
  -> (a :+: b) :*: c :~: (a :*: c) :+: (b :*: c)
jan  mas rovira's avatar
jan mas rovira committed
139
prodDistribR SZero _b _c = Refl
jan  mas rovira's avatar
jan mas rovira committed
140
141
142
143
144
145
146
147
148
149
150
prodDistribR (SSuc (n :: SNat n)) b c = s1 `trans` sym (plusAssoc c nc bc)
  where
    indh :: ((n :+: b) :*: c) :~: ((n :*: c) :+: (b :*: c))
    indh = prodDistribR n b c
    s1 :: c :+: ((n :+: b) :*: c) :~: c :+: ((n :*: c) :+: (b :*: c))
    s1 = plusEqL c indh
    nc :: SNat (n :*: c)
    nc = n .*. c
    bc :: SNat (b :*: c)
    bc = b .*. c

jan  mas rovira's avatar
jan mas rovira committed
151
152
prodDistribL :: forall a b c. SNat a -> SNat b -> SNat c
  -> a :*: (b :+: c) :~: (a :*: b) :+: (a :*: c)
jan  mas rovira's avatar
jan mas rovira committed
153
prodDistribL SZero _b _c = Refl
jan  mas rovira's avatar
jan mas rovira committed
154
155
156
157
158
159
160
161
162
163
164
prodDistribL (SSuc (n :: SNat n)) b c = s6
  where
    nb = n .*. b
    nc = n .*. c
    indh :: (n :*: (b :+: c)) :~: ((n :*: b) :+: (n :*: c))
    s1 :: ((b :+: c) :+: (n :*: (b :+: c))) :~: ((b :+: c) :+: ((n :*: b) :+: (n :*: c)))
    s2 :: ((b :+: c) :+: (n :*: (b :+: c))) :~: (b :+: (c :+: ((n :*: b) :+: (n :*: c))))
    s3 :: ((b :+: c) :+: (n :*: (b :+: c))) :~: (b :+: ((c :+: (n :*: b)) :+: (n :*: c)))
    s4 :: ((b :+: c) :+: (n :*: (b :+: c))) :~: (b :+: (((n :*: b) :+: c) :+: (n :*: c)))
    s5 :: ((b :+: c) :+: (n :*: (b :+: c))) :~: (b :+: ((n :*: b) :+: (c :+: (n :*: c))))
    s6 :: ((b :+: c) :+: (n :*: (b :+: c))) :~: ((b :+: (n :*: b)) :+: (c :+: (n :*: c)))
jan  mas rovira's avatar
clean    
jan mas rovira committed
165
166
167
    indh = prodDistribL n b c
    s1 = plusEqL (b .+. c) indh
    s2 = s1 `trans` plusAssoc b c (nb .+. nc)
jan  mas rovira's avatar
jan mas rovira committed
168
169
170
    s3 = plusTransR b s2 (sym (plusAssoc c nb nc))
    s4 = plusTransR b s3 (plusEqR nc (c .+. nb)(plusCommut c nb))
    s5 = plusTransR b s4 (plusAssoc nb c nc)
jan  mas rovira's avatar
jan mas rovira committed
171
172
173
    s6 = s5 `trans` sym (plusAssoc b nb (c .+. nc))


jan  mas rovira's avatar
jan mas rovira committed
174
prodAssoc :: forall a b c. SNat a -> SNat b -> SNat c -> (a :*: b) :*: c :~: a :*: (b :*: c)
jan  mas rovira's avatar
jan mas rovira committed
175
176
177
178
179
180
181
182
183
prodAssoc SZero _b _c = Refl
prodAssoc (SSuc (n :: SNat n)) b c = plusEqL bc indh `transL` sym (prodDistribR b nb c)
  where
    indh :: ((n :*: b) :*: c) :~: (n :*: (b :*: c))
    indh = prodAssoc n b c
    bc :: SNat (b :*: c)
    bc = b .*. c
    nb :: SNat (n :*: b)
    nb = n .*. b
jan  mas rovira's avatar
jan mas rovira committed
184

jan  mas rovira's avatar
clean    
jan mas rovira committed
185
prodCommut :: forall a b. SNat a -> SNat b -> (a :*: b) :~: (b :*: a)
jan  mas rovira's avatar
jan mas rovira committed
186
prodCommut SZero b = sym (prodZeroR b)
jan  mas rovira's avatar
jan mas rovira committed
187
prodCommut (SSuc (n :: SNat n)) b = s2
jan  mas rovira's avatar
jan mas rovira committed
188
189
190
  where
    indh :: (n :*: b) :~: (b :*: n)
    indh = prodCommut n b
jan  mas rovira's avatar
jan mas rovira committed
191
192
193
194
    s1 :: (b :+: (n :*: b)) :~: b :+: (b :*: n)
    s1 = plusEqL b indh
    s2 :: (b :+: (n :*: b)) :~: (b :*: 'Suc n)
    s2 = s1 `trans` sym (prodSucR b n)
jan  mas rovira's avatar
jan mas rovira committed
195
196
197

prodEqL :: SNat k -> a :~: b -> k :*: a :~: k :*: b
prodEqL SZero Refl                = Refl
jan  mas rovira's avatar
clean    
jan mas rovira committed
198
prodEqL (SSuc (_ :: SNat n)) Refl = Refl
jan  mas rovira's avatar
jan mas rovira committed
199
200
201

prodEqR :: SNat k -> a :~: b -> a :*: k :~: b :*: k
prodEqR SZero Refl                = Refl
jan  mas rovira's avatar
clean    
jan mas rovira committed
202
prodEqR (SSuc (_ :: SNat n)) Refl = Refl
jan  mas rovira's avatar
jan mas rovira committed
203

jan  mas rovira's avatar
jan mas rovira committed
204
powerZero :: a :^: 'Zero :~: One
jan  mas rovira's avatar
jan mas rovira committed
205
powerZero = Refl
jan  mas rovira's avatar
jan mas rovira committed
206

jan  mas rovira's avatar
jan mas rovira committed
207
powerOne :: SNat a -> a :^: One :~: a
jan  mas rovira's avatar
jan mas rovira committed
208
209
210
powerOne SZero                = Refl
powerOne (SSuc (n :: SNat n)) = congSuc (prodOneR n)

jan  mas rovira's avatar
jan mas rovira committed
211
powerTransExp :: SNat a -> c :~: a :^: b -> b :~: b' -> c :~: a :^: b'
jan  mas rovira's avatar
jan mas rovira committed
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
powerTransExp _ Refl Refl = Refl

prodPower :: forall a b c. SNat a -> SNat b -> SNat c
  -> (a :^: b) :*: (a :^: c) :~: a :^: (b :+: c)
prodPower a SZero c = plusZeroR (a .^. c)
prodPower a (SSuc (n :: SNat n)) c = s2
  where
    indh :: ((a :^: n) :*: (a :^: c)) :~: (a :^: (n :+: c))
    indh = prodPower a n c
    s1 :: (a :*: ((a :^: n) :*: (a :^: c))) :~: (a :*: (a :^: (n :+: c)))
    s2 :: ((a :*: (a :^: n)) :*: (a :^: c)) :~: (a :*: (a :^: (n :+: c)))
    s1 = prodEqL a indh
    s2 = s1 `transL` sym (prodAssoc a (a .^. n) (a .^. c))

powerProd :: forall a b c. SNat a -> SNat b -> SNat c
  -> (a :^: c) :*: (b :^: c) :~: (a :*: b) :^: c
powerProd _ _ SZero = Refl
powerProd a b (SSuc (n :: SNat n)) = s6
  where
    an = a .^. n
    bn = b .^. n
    indh = powerProd a b n
    indh :: ((a :^: n) :*: (b :^: n)) :~: ((a :*: b) :^: n)
    s1 :: ((a :*: b) :*: ((a :^: n) :*: (b :^: n))) :~: ((a :*: b) :*: ((a :*: b) :^: n))
    s2 :: (a :*: (b :*: ((a :^: n) :*: (b :^: n)))) :~: ((a :*: b) :*: ((a :*: b) :^: n))
    s3 :: (a :*: ((b :*: (a :^: n)) :*: (b :^: n))) :~: ((a :*: b) :*: ((a :*: b) :^: n))
    s4 :: (a :*: (((a :^: n) :*: b) :*: (b :^: n))) :~: ((a :*: b) :*: ((a :*: b) :^: n))
    s5 :: (a :*: ((a :^: n) :*: (b :*: (b :^: n)))) :~: ((a :*: b) :*: ((a :*: b) :^: n))
    s6 :: ((a :*: (a :^: n)) :*: (b :*: (b :^: n))) :~: ((a :*: b) :*: ((a :*: b) :^: n))
    s1 = prodEqL (a .*. b) indh
    s2 = s1 `transL` prodAssoc a b (an .*. bn)
    s3 = sym (prodTransR a (sym s2) (sym (prodAssoc b an bn)))
    s4 = sym (prodTransR a (sym s3) (prodEqR bn (prodCommut b an)))
    s5 = sym (prodTransR a (sym s4) (prodAssoc an b bn))
    s6 = s5 `transL` sym (prodAssoc a an (b .*. bn))
jan  mas rovira's avatar
jan mas rovira committed
247
248
249
250
251
252
253
254
255
256
257
258
259
260

powerPower :: forall a b c. SNat a -> SNat b -> SNat c
  -> (a :^: b) :^: c :~: a :^: (b :*: c)
powerPower a b SZero = powerTransExp a (sym powerZero) (sym (prodZeroR b))
powerPower a b (SSuc (n :: SNat n)) = s3
  where
    indh = powerPower a b n
    indh :: ((a :^: b) :^: n) :~: (a :^: (b :*: n))
    s1 :: ((a :^: b) :*: ((a :^: b) :^: n)) :~: (a :^: b) :*: (a :^: (b :*: n))
    s2 :: ((a :^: b) :*: ((a :^: b) :^: n)) :~: (a :^: (b :+: (b :*: n)))
    s3 :: ((a :^: b) :*: ((a :^: b) :^: n)) :~: (a :^: (b :*: 'Suc n))
    s1 = prodEqL (a .^. b) indh
    s2 = s1 `trans` prodPower a b (b .*. n)
    s3 = powerTransExp a s2 (sym (prodSucR b n))