Posted:

**Apr 06, 2012 7:33 pm**VazScep wrote::grin: I'm seriously happy about this! I've no idea whether my solution is optimal, but you seem to have picked the same strategy, so that's cool. Basically, we want the fact that contradictions imply *anything*. If you have p and you have its negation, then you have arbitrary q.

Yeah, I have no idea if it's optimal either. Frankly it's the first move I could make, I can't even think of another way.

Yeah, I still have to try that conversions language you posted though.Yeah, you're damn close at this point. And you don't want these as mere lemmas. These two give you the double-negation elimination conversion.

Easily. Cheers for getting into this stuff. I'm seriously impressed.

Well, so here it is, finally

- Code: Select all
`-- |- (~p ==> q) ==> (~p ==> ~q) ==> p`

main = let

step1 = Assume $ Not p :=>: q

step2 = matchMP lemma5 step1

step3 = Assume $ Not p :=>: Not q

step4 = hyp_sylo step3 step2

step5 = let

step5_1 = instL [p, Not (q :=>: p)] lemma1

step5_2 = instL [Not p, p, Not (q :=>: p)] axiom2

in head $ mp step5_2 step5_1

step6 = matchMP step5 step4

step7 = instL [p, q :=>: p] axiom3

step8 = matchMP step7 step6

step9 = matchMP axiom3 step3

step10 = MP step8 step9

step11 = discharge (Not p :=>: Not q) step10

in print $ printThm $ verify $ step11

Now, damn it, that took a while.

I am curious though about how much our proofs differ.

I *believe* a templated dimensional analysis system is one of the case-studies in Alexandrescu's "Modern C++ Design". A friend of mine who worked in the physics department for a major game developer said they used the pattern a lot, but he said he also found it so verbose as to be almost useless. The big sell of the F# solution is in the fact that you write virtually no unit annotations and you get polymorphism. However, it's not going to be a serious shock to me to hear that the Boost folk figured that out too.

Oh, it's a shame I haven' t yet read that book, I definitely should have and there are no excuses.

I have no idea how complicated the boost library is if you need to create custom base units, but it seems simple enough if all you need are the common ones. Guess I' ll have to try it.