0

在 Welder 中使用 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) 
      }
    }
  }

代码可以编译，但 Welder 说：

SMT求解器无法证明属性：false

从假设： (mult(a, b) == zero()) == false。

我会说我没有将正确的函数传递给构造。有人可以解释我应该写什么才能成功吗？是否与类型有关，即 (Theorem, Goal) => Attempt[Witness]？我是否需要提供一个定理来证明目标？

我还能证明什么是假的？我应该使用某种暗示介绍吗？

4

1 回答 1

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)
      }
    }
  }
于 2017-04-19T08:26:26.693 回答