在 Welder 中使用 notI。矛盾证明示例

Question

我在 Welder 中使用 notI 构造时遇到了一些问题。以下面为例证明：

我的示例使用了关于环结构的常用引理和派生引理 (zeroDivisorLemma)，它表示对于环中的所有 'a' a0 = 0 = 0a。

我证明如果两个元素不为零，则它们的乘积不为零。如下

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 solver could not prove the property: false

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

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

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

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

在 Welder 中使用 notI。矛盾证明示例

Using notI in Welder. Example contradiction proof

leon