Posted: Apr 05, 2012 4:53 pm
VazScep wrote:
mizvekov wrote:Still working on that goddamn example!
By the way, I found that having a theorem and a function like this helps a lot:
I think I can see that working.

Unfortunately, I don't have my code to hand at the moment. But I can throw a lemma your way if you want a hint.

Okay, these are the lemmas I have so far:
Code: Select all
`-- |- ~p ==> p ==> qlemma1 = let   step1  = Assume \$ Not p   step2  = instL [p, Not q] axiom1   step3  = matchMP step2 step1   step4  = matchMP axiom3 step3   in verify step4-- |- ~~p ==> plemma2 = let   step1  = Assume \$ Not \$ Not p   step2  = instL [p, Not \$ Not p] lemma1   step3  = matchMP step2 step1   step4  = instL [p, Not \$ Not p] axiom3   step5  = matchMP step4 step3   step6  = MP step5 step1   in verify \$ step6-- |- p ==> ~~plemma3 = let   step1  = instL [Not p] lemma2   step2  = instL [Not \$ Not p, p] axiom3   step3  = mp step2 step1   in head \$ step3-- |- (p ==> q) ==> ~q ==> ~plemma4 = let   step1  = Assume \$ p :=>: q   step2  = UseTheorem lemma2   step3  = hyp_sylo step2 step1   step4  = UseTheorem \$ instL [q] lemma3   step5  = hyp_sylo step3 step4   step6  = instL [Not p, Not q] axiom3   step7  = matchMP step6 step5   in verify \$ step7-- |- (~p ==> q) ==> ~q ==> plemma5 = let   step1  = Assume \$ Not p :=>: q   step2  = matchMP (instL [Not p, q] lemma4) step1   step3  = Assume \$ Not q   step4  = MP step2 step3   step5  = matchMP lemma2 step4   step6  = discharge (Not q) step5   in verify \$ step6`

I think I should be able to find a proof for it now. I will try to finish this off tomorrow.

epepke wrote:
This is reasonably easy to do in C++ by overloading the multiplication operator. I've done a units package based on this. A simple example:
...

By the way, I was curious and checked if boost already supported something like this, and yes indeed it does!
Based on an example in: http://www.boost.org/doc/libs/1_49_0/do ... Start.html
Code: Select all
`        quantity<force>     F(2.0 * newton);        quantity<length>    dx(2.0 * meter);        auto E = F * dx;        std::cout << "F  = " << F << std::endl;        std::cout << "dx = " << dx << std::endl;        std::cout << "E  = " << E << std::endl;`

Prints:
Code: Select all
`F  = 2 Ndx = 2 mE  = 4 J`