溶接機でnotIを使用する。例矛盾の証明

Question

WelderでnotI構造を使用しているときにいくつか問題があります。

私の例では、リングの構造と、リングa0 = 0 = 0aのすべての 'a'についての派生した補題（zeroDivisorLemma）について通常の補題を使用しています。

2つの要素がゼロでない場合、その積はゼロではないことを証明します。次のように。

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ソルバーは、プロパティを証明することができませんでした：偽

仮説から： （MULT（a、b）は==ゼロ（）） == false。

私は、正しい関数を構造体に渡していないと思います。誰かが成功するために何を書くべきか説明することができますか？タイプ（すなわち、（定理、目標）=>試み[証人]）と関係がありますか？私は定理を提供する必要があり、それは目標を証明しますか？

偽証を得るために他に何が証明できますか？私は暗黙の導入のいくつかの並べ替えを使用する必要がありますか？

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