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, 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.
Yeah, I still have to try that conversions language you posted though.

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

Well, so here it is, finally
Code: Select all
`-- |- (~p ==> q) ==> (~p ==> ~q) ==> pmain = 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.