Is it possible to prove this defined function is an involution in z3?

Question

I'm trying to understand how to define an assertion in such a way that it proves certain mathematical qualities of an already defined function. As discussed in this post SMT solvers are not well-suited for induction, which is often needed to prove a mathematical quality.

In my case, I have a recursive function definition for the identity function f(x) = x (just as a simple example):

(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 suggests that such characteristics cannot be proven out-of-the-box. However, I am interested to know how general mathematical properties are proven in z3. I tried with all-quantifiers to prove the involution of the function but z3 does not terminate:

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

My Question: What assertion can we use to prove that such a recursive function is an involution with z3?

alias alias · Accepted Answer · 2021-01-29T20:04:29

There isn't really much you can do here. Ideally, the strategy would be to define and prove the base case and the inductive-step separately, and then argue (at the meta-level) that the property is true for all strings.

For the base-case things are easy enough. I'd define:

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

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

And then:

(assert (not base_case))

If you do this, z3 will happily say unsat, i.e., base case is true. For the induction step, I'd define:

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

And hope to prove:

(assert (not inductive_step))

Alas, you'll find that z3 will choke on this query, i.e., won't terminate. Assuming for a second it did, you'd then conclude (at the meta-level) that identity is indeed an involution. But this has to be done at one-level above z3; either by a human, or some other proof tool that uses z3 as a sub-engine.

So, the natural question is to ask what are the hopes for getting z3 to prove the inductive_step? It will definitely not do it out-of-the-box. But perhaps you can use patterns to coax it into doing so, see https://rise4fun.com/z3/tutorialcontent/guide#h28 for details. Be warned, however, that even if you can get this proof go with very clever pattern instantiations, the proof will be so very brittle: Even minor changes to your theorem or the actual implementation of z3 can affect the result, as you'll be at the mercy of a myriad of heuristics.

Long story short: You're using the wrong tool if your goal is to prove properties of recursive functions. Use ACL2, HOL, Isabelle, etc.; which are purposefully designed and built to deal with such theorems. An SMT solver just doesn't fit the bill here.

Is it possible to prove this defined function is an involution in z3?

1 Answers