Posted: Apr 05, 2012 4:53 pm
by mizvekov
VazScep wrote:
mizvekov wrote:Still working on that goddamn example! :grin:
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 ==> q
lemma1 = let
   step1  = Assume $ Not p
   step2  = instL [p, Not q] axiom1
   step3  = matchMP step2 step1
   step4  = matchMP axiom3 step3
   in verify step4

-- |- ~~p ==> p
lemma2 = 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 ==> ~~p
lemma3 = let
   step1  = instL [Not p] lemma2
   step2  = instL [Not $ Not p, p] axiom3
   step3  = mp step2 step1
   in head $ step3

-- |- (p ==> q) ==> ~q ==> ~p
lemma4 = 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 ==> p
lemma5 = 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 N
dx = 2 m
E  = 4 J