Posted: Apr 06, 2012 7:33 pm
by mizvekov
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 :thumbup:
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.