Anonymous user
Proof: Difference between revisions
update Haskell example
mNo edit summary |
(update Haskell example) |
||
Line 251:
<lang haskell>{-# LANGUAGE TypeOperators, TypeFamilies, GADTs #-}
module
-- 1.1. Natural numbers.
data Z = Z
data S
-- 2.1. Addition.
Line 263:
type family x :+ y
type instance Z :+ n = n
type instance
-- 1.2. Even natural numbers.
Line 269:
data En :: * -> * where
Ez :: En Z
Es :: En
-- 1.3. Odd natural numbers.
data On :: * -> * where
Oo :: On (S Z)
Os :: On m -> On (S (S m))
-- 3.1. Sum of any two even numbers is even.
Line 280 ⟶ 286:
infix 4 :=
data (:=)
Refl ::
sym :: m := n -> n := m
sym Refl = Refl
trans :: m := n -> n := p -> m := p
trans Refl np = np
cong :: m := n -> S m := S n
Line 296 ⟶ 308:
instance AssocAdd m => AssocAdd (S m) where
proof (S m) n p = cong $ proof m n p
</lang>▼
-- Induction, associativity of addition by induction, equational reasoning and
-- commutativity of addition is too tricky.
-- Uninhabited type.
data Bot
-- 4.1.
sum_of_even_is_not_odd :: En m -> En n -> On (m :+ n) -> Bot
sum_of_even_is_not_odd Ez (Es n) (Os mn) = sum_of_even_is_not_odd Ez n mn
sum_of_even_is_not_odd (Es m) n (Os mn) = sum_of_even_is_not_odd m n mn
sum_of_even_is_not_odd Ez Ez _ =
error "impossible happened in sum_of_even_is_not_odd!"
-- ^
-- partial, however, we know that Ez :: En Z, Z + Z = Z and On Z is
-- uninhabited, so that this clause is unreachable.
--
-- Also, GHC complains:
--
-- Warning: Pattern match(es) are non-exhaustive
-- In an equation for `sum_of_even_is_not_odd':
-- Patterns not matched:
-- Ez (Es _) Oo
-- (Es _) _ Oo
--
-- and can't find that this clauses is unreachable too, since this isn't type check:
--
-- sum_of_even_is_not_odd Ez (Es _) Oo = undefined
-- sum_of_even_is_not_odd (Es _) _ Oo = undefined
▲-- </lang>
See also [[Proof/Haskell]] for implementation of a small theorem prover.
| |||