Using notI in Welder. Example contradiction proof

Question

I have some problems while using the notI construct in Welder. Take the following as an example proof:

My example uses usual lemmas about the structure of rings and a derived lemma (zeroDivisorLemma) that says that for all 'a' in the ring a0 = 0 = 0a.

I proof that if two elements are not zero, their product is not zero. As follows.

val theorem: Theorem = 
  forallI("a"::F,"b"::F){ case (a,b) => 
    implI(and(a !== z, b !== z,multInverseElement,multNeutralElement,multAssociative,
              addOppositeElement,addNeutralElement,addAssociative,isDistributive)){ axioms => 
      val Seq(aNotZero,bNotZero,multInverseElement,multNeutralElement,multAssociative,
              addOppositeElement,addNeutralElement,addAssociative,isDistributive) = andE(axioms) : Seq[Theorem]
      notI((a ^* b) === z) { case (hyp,_) => 
        ((a ^* b) === z)                         ==| andI(bNotZero,hyp)                                    |
        (((a ^* b) ^* inv(b)) === (z ^* inv(b))) ==| forallE(multAssociative)(a,b,inv(b))                  |
        ((a ^* (b ^* inv(b))) === (z ^* inv(b))) ==| andI(forallE(multInverseElement)(b),bNotZero)         |
        ((a ^* one) === (z ^* inv(b)))           ==| forallE(multNeutralElement)(a)                        |
        (a === (z ^* inv(b)))                    ==| forallE(implE(zeroDivisorLemma)(g => axioms))(inv(b)) |
        (a === z)                                ==| aNotZero     |
        ((a !== z) && (a === z))                 ==| trivial |
        (a !== a)                                ==| trivial |
        BooleanLiteral(false) 
      }
    }
  }

The code compiles but Welder says:

SMT solver could not prove the property: false

from hypotheses: (mult(a, b) == zero()) == false.

I'd say I'm not passing the right function to the construct. Could someone explain what should I write to succeed? Does it have to do with the type, i.e., (Theorem, Goal) => Attempt[Witness]? Do I need to provide a theorem and that proves the goal?

What else can I proof to get false? Should I use some sort of implication introduction?

score 1 · Accepted Answer · answered Apr 19 '17 at 08:26

What the error says is that it could not deduce a contradiction from what you shown. Indeed, you have not shown a contradiction in body of the notI. The derivation to prove that (mult(a, b) == zero()) == false is correct, but you still have to explicitly show the contradiction by taking the conjunction with hyp.

Would something like this work ?

    val theorem: Theorem = 
  forallI("a"::F,"b"::F){ case (a,b) => 
    implI(and(a !== z, b !== z,multInverseElement,multNeutralElement,multAssociative,
              addOppositeElement,addNeutralElement,addAssociative,isDistributive)){ axioms => 
      val Seq(aNotZero,bNotZero,multInverseElement,multNeutralElement,multAssociative,
              addOppositeElement,addNeutralElement,addAssociative,isDistributive) = andE(axioms) : Seq[Theorem]
      notI((a ^* b) === z) { case (hyp,_) => 
        val deriv = ((a ^* b) === z)               ==| andI(bNotZero,hyp)                                    |
          (((a ^* b) ^* inv(b)) === (z ^* inv(b))) ==| forallE(multAssociative)(a,b,inv(b))                  |
          ((a ^* (b ^* inv(b))) === (z ^* inv(b))) ==| andI(forallE(multInverseElement)(b),bNotZero)         |
          ((a ^* one) === (z ^* inv(b)))           ==| forallE(multNeutralElement)(a)                        |
          (a === (z ^* inv(b)))                    ==| forallE(implE(zeroDivisorLemma)(g => axioms))(inv(b)) |
          (a === z)                                ==| aNotZero     |
          ((a !== z) && (a === z))                 ==| trivial |
          (a !== a)                                ==| trivial |
          BooleanLiteral(false) 

        andI(deriv, hyp)
      }
    }
  }

Using notI in Welder. Example contradiction proof

1 Answers1