是否可以证明这个定义的函数是 z3 的对合？

问题描述

我试图了解如何定义断言，以证明已定义函数的某些数学特性。如 this post 中所述，SMT 求解器不太适合用于证明数学质量的归纳法。

在我的例子中，我有一个用于身份函数 f(x) = x 的递归函数定义（只是一个简单的例子）：

(define-fun-rec identity-rec ((l String)) String
   (ite (= 0 (str.len l))
      ""
      (str.++ (str.at l 0) (identity-rec (str.substr l 1 (seq.len l))))))



(define-fun identity ((l String)) String
   (ite (= 0 (str.len l))
      ""
      (identity-rec l)))

The same post 表明这些特性不能开箱即用。但是，我很想知道如何在 z3 中证明一般的数学属性。我尝试使用全量词来证明函数的对合，但 z3 不会终止：

(assert
(forall ((a String))
    (=
        a
        (indentity (identity a))
    )
)

我的问题： 我们可以用什么断言来证明这样的递归函数是与 z3 的对合？

解决方法

在这里你真的无能为力。理想情况下，策略是分别定义和证明基本情况和归纳步骤，然后（在元级别）论证该属性对所有字符串都为真。

对于基本情况，事情很简单。我会定义：

(define-fun check-inv ((x String)) Bool (= (identity (identity x)) x))

(define-fun base_case () Bool (check-inv ""))

然后：

(assert (not base_case))

如果你这样做，z3 会很高兴地说 unsat，即基本情况是真的。对于归纳步骤，我会定义：

(define-fun inductive_step () Bool
   (forall ((x String) (c String))
        (implies (and (= 1 (str.len c)) (check-inv x))
                 (check-inv (str.++ c x)))))

并希望证明：

(assert (not inductive_step))

唉，你会发现 z3 会阻塞这个查询，即不会终止。假设它确实有那么一秒钟，然后您会得出结论（在元级别）identity 确实是对合。但这必须在 z3 之上的一级完成；由人类或其他一些使用 z3 作为子引擎的证明工具。

那么，自然的问题是要问让 z3 证明 inductive_step 的希望是什么？它绝对不会开箱即用。但也许您可以使用模式来诱使它这样做，有关详细信息，请参阅 https://rise4fun.com/z3/tutorialcontent/guide#h28。但是，请注意，即使您可以通过非常聪明的模式实例化来获得此证明，该证明也将非常脆弱：即使对定理或 z3 的实际实现进行微小更改也会影响结果，因为您将受无数启发式方法的支配。

长话短说：如果您的目标是证明递归函数的属性，那么您使用了错误的工具。使用ACL2、HOL、Isabelle等；有目的地设计和构建来处理这些定理。 SMT 求解器不适合这里的要求。

smt z3