blob: 1f3aca78ffd16837fb6acf0cc51e5ab1169fd1a2 (
plain)
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
|
-- https://www.codewars.com/kata/59db393bc1596bd2b700007f
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Kata.AdditionCommutes
( plusCommutes ) where
import Kata.AdditionCommutes.Definitions
( Z, S
, Natural(..), Equal(..)
, (:+:))
reflexive :: Natural n -> Equal n n
reflexive NumZ = EqlZ
reflexive (NumS n) = EqlS $ reflexive n
symmetric :: Equal a b -> Equal b a
symmetric EqlZ = EqlZ
symmetric (EqlS e) = EqlS $ symmetric e
transitive :: Equal a b -> Equal b c -> Equal a c
transitive EqlZ EqlZ = EqlZ
transitive (EqlS e1) (EqlS e2) = EqlS $ transitive e1 e2
-- lemma1 (a + s(b)) = s(a+b)
lemma1 :: Natural a -> Natural b -> Equal (a :+: S b) (S (a :+: b))
lemma1 NumZ NumZ = EqlS EqlZ
lemma1 NumZ (NumS b) = EqlS $ lemma1 NumZ b
lemma1 (NumS a) b = EqlS $ lemma1 a b
-- lemma2 (s(b) + a) = s(b+a)
lemma2 :: Natural a -> Natural b -> Equal (S b :+: a) (S (b :+: a))
lemma2 NumZ NumZ = EqlS EqlZ
lemma2 (NumS a) NumZ = EqlS $ lemma2 a NumZ
lemma2 a (NumS b) = EqlS $ lemma2 a b
plusCommutes :: Natural a -> Natural b -> Equal (a :+: b) (b :+: a)
plusCommutes NumZ NumZ = EqlZ
plusCommutes NumZ (NumS b) = EqlS $ plusCommutes NumZ b
plusCommutes (NumS a) NumZ = EqlS $ plusCommutes a NumZ
plusCommutes a (NumS b) = transitive (transitive eq1 known) eq2 where
known = EqlS $ plusCommutes a b
eq1 = lemma1 a b
eq2 = symmetric $ lemma2 a b
{-
data Z
data S n
data Natural :: Type -> Type where
NumZ :: Natural Z
NumS :: Natural n -> Natural (S n)
data Equal :: Type -> Type -> Type where
EqlZ :: Equal Z Z
EqlS :: Equal n m -> Equal (S n) (S m)
type family (:+:) (n :: Type) (m :: Type) :: Type
type instance Z :+: m = m
type instance S n :+: m = S (n :+: m)
-}
|
