在焊機中使用notI。示例矛盾證明

Question

在焊機中使用notI構造時存在一些問題。以下列爲例證：

我的例子使用了有關環的結構和導出的引理（zeroDivisorLemma）的一般引理，它說環a0 = 0 = 0a中的所有'a'。

我證明如果兩個元素不爲零，他們的產品不是零。如下。

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) 
     } 
    } 
    } 

的代碼編譯，但焊工說：

SMT求解器不能證明財產：假

從假設： （多重（A，B）==零（）） ==假。

我想說我沒有把正確的功能傳遞給構造。有人能解釋我應該寫什麼才能成功嗎？它是否與這個類型有關，即（定理，目標）=>嘗試[見證]？我需要提供一個定理並證明目標嗎？

還有什麼我可以證明爲假？我應該使用某種暗示介紹嗎？

Answer 1

錯誤說的是它不能推斷出你所顯示的矛盾。事實上，你在notI的主體中沒有表現出矛盾。推導證明(mult(a, b) == zero()) == false是正確的，但你仍然必須明確地通過與hyp結合顯示矛盾。

會這樣的工作？

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) 
     } 
    } 
    }