Anonymous user
Proof: Difference between revisions
update haskell example
mNo edit summary |
(update haskell example) |
||
Line 342:
-- Induction, associativity of addition by induction, equational reasoning and
-- commutativity of addition is too tricky.
-- 3.4. Bad proof.
-- ^
-- Сan not be written totally:
--
sum_of_even_is_odd Ez Ez = undefined
-- ^
-- then, in GHCi:
--
-- *PeanoArithmetic> :t sum_of_even_is_odd Ez Ez
-- sum_of_even_is_odd Ez Ez :: On (Z :+ Z)
-- *PeanoArithmetic> :t undefined :: On (Z :+ Z)
-- undefined :: On (Z :+ Z) :: On Z
-- *PeanoArithmetic> :t sum_of_even_is_odd Ez Ez :: On Z
-- sum_of_even_is_odd Ez Ez :: On Z :: On Z
-- *PeanoArithmetic> :t Oo
-- Oo :: On (S Z)
-- *PeanoArithmetic> :t Os Oo
-- Os Oo :: On (S (S (S Z)))
-- *PeanoArithmetic> :t Os (Os Oo)
-- Os (Os Oo) :: On (S (S (S (S (S Z)))))
--
-- so that sum_of_even_is_odd Ez Ez :: On Z, but On Z is empty, it is impossible
-- to write such a proof.
--
-- Uninhabited type.
Line 347 ⟶ 374:
data Bot
--
type Not a = a -> Bot
▲sum_of_even_is_not_odd :: En m -> En n -> On (m :+ n) -> Bot
-- 4.1. Disproof.
sum_of_even_is_not_odd :: En m -> En n -> Not (On (m :+ n))
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
Line 370 ⟶ 401:
-- sum_of_even_is_not_odd Ez (Es _) Oo = undefined
-- sum_of_even_is_not_odd (Es _) _ Oo = undefined
--
-- 4.2. Bad disproof.
sum_of_even_is_not_even :: En m -> En n -> Not (En (m :+ n))
--
-- Starting from a partial definition:
--
sum_of_even_is_not_even Ez Ez _ = undefined
--
-- we can show that it can not be rewritten totally:
--
-- *PeanoArithmetic> :t sum_of_even_is_not_even Ez Ez
-- sum_of_even_is_not_even Ez Ez :: Not (En (Z :+ Z))
-- *PeanoArithmetic> :t sum_of_even_is_not_even Ez Ez :: Not (En Z)
-- sum_of_even_is_not_even Ez Ez :: Not (En Z) :: Not (En Z)
-- *PeanoArithmetic> :t sum_of_even_is_not_even Ez Ez :: En Z -> Bot
-- sum_of_even_is_not_even Ez Ez :: En Z -> Bot :: En Z -> Bot
-- *PeanoArithmetic> :t Ez
-- Ez :: En Z
-- *PeanoArithmetic> :t (sum_of_even_is_not_even Ez Ez :: En Z -> Bot) Ez
-- (sum_of_even_is_not_even Ez Ez :: En Z -> Bot) Ez :: Bot
--
-- since we have a "citizen" of an uninhabited type here (contradiction!).
-- </lang>
| |||