Iff is translated as an uninterpreted function, leading to wrong results

[dranov]

import Smt

set_option trace.smt true
set_option trace.smt.solve true

variable {node : Type} [Nonempty node]

theorem wrong (a : node → Prop)
: ∀ n, a n ↔ a n := by smt

The generated query is:

(set-logic ALL)
(declare-sort node 0)
(declare-fun a (node) Bool)
(declare-fun Iff (Bool Bool) Bool)
(assert (not (forall ((n node)) (Iff (a n) (a n)))))
(check-sat) 

which returns sat

[dranov]

The change in PR #122 seems sufficient.

[abdoo8080]

Hi @dranov! Thanks for filing the bug and working on a fix. While your PR is sound, the proof reconstruction part of the tactic is not aware of the change, which might cause Lean to reject the reconstructed proof. To avoid confusion, it's better to eliminate Iff in a pre-processing step. PR #123 addresses this for the most part, though there may still be some corner cases. We'll have a proper solution once we start integrating lean-smt with lean-auto.

[dranov]

That makes sense. Thank you for the quick fix!