Posted: Apr 07, 2012 7:55 am
So here's mine:mizvekov wrote:I am curious though about how much our proofs differ.
- Code: Select all
-- ⊢ P → P
truth :: Theorem String
truth = let step1 = instL [p, p :=>: p] axiom1
step2 = instL [p, p :=>: p, p] axiom2
step3 = head $ mp step2 step1
step4 = instL [p, p] axiom1 in
head $ mp step3 step4
-- ⊢ ¬P → P → ⊥
lemma1 :: Theorem String
lemma1 = let step1 = UseTheorem (instL [Not p, Not f] axiom1)
step2 = Assume (Not p)
step3 = MP step1 step2
step4 = matchMP axiom3 step3
in verify step4
-- ⊢ (¬P → Q) -> (¬P → ¬Q) → P
-- This is Mendelson's axiom3.
mendelson :: Theorem String
mendelson = let step1 = Assume (Not p :=>: Not q)
step2 = Assume (Not p :=>: q)
step3 = Assume (Not p)
step4 = MP step1 step3
step5 = MP step2 step3
step6 = matchMP lemma1 step4
step7 = MP step6 step5
step8 = discharge (Not p) step7
step9 = matchMP axiom3 step8
step10 = UseTheorem (instL [q] truth)
step11 = MP step9 step10
step12 = discharge (concl step2) step11
in verify step12
My lemma isn't quite the same as yours. I basically introduced the notion of false (⊥ or f) as the negation of the tautology "P → P". But I can then easily use this to derive an arbitrary proposition.
It's definitely going on my reading list if I ever land a C++ job. I'm thinking I'll go through Scott Meyers again, and then probably Sutter and Coplien too.Oh, it's a shame I haven' t yet read that book, I definitely should have and there are no excuses.