lean-auto with structure

Stream: lean4

[Kaushik Raghavan]

Hi everyone,

I was trying this simple example to use lean-auto to find sat/unsat for a trivial case:

set_option auto.smt true
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true
set_option trace.auto.smt.unsatCore.leanExprs true

structure st where
  x : Int

def unfoldedTestRec (p: Int) (a b : st) : st :=
  if p = a.x then a else if p = b.x then b else { x := -1 }

example {a b : st} (h : (unfoldedTestRec 1 a b).x = 1) : False := by
  simp [unfoldedTestRec] at h
  auto

which gives the following error _private.Auto.Translation.LamFOL2SMT.0.Auto.SMT.lamTerm2STermAux :: Unexpected head term Auto.Embedding.Lam.LamTerm.lam (.atom 1) (.bvar 2). I was expecting the auto tactic to return Sat.

Could someone please help me understand what is causing this error for cases like this?

[Abdalrhman M Mohamed]

It appears that in Lean-auto's quest to identify definitional equalities between constants, it ends up unfolding Auto.Bool.ite' (auto's own version of ite). That unfolding introduces a higher-order lambda term, which cannot be translated to SMT-LIB. (Higher-order constructs were recently added in SMT-LIB 2.7, which no solver fully supports yet.)

I see three possible ways to work around this:

1. Mark Auto.Bool.ite' as @[irreducible]. Lean-auto does not unfold irreducible constants by default, so this avoids introducing the higher-order lambda. This would require a small change on Lean-auto's side (ping @Yicheng Qian).

2. Restrict Lean-auto's transparency mode to unfold only reducible constants. This prevents unfolding Auto.Bool.ite', but may cause Lean-auto to miss some otherwise obvious equalities. If you use this approach, you may also want to set auto.mono.termLikeDefEq.mode to "reducible":

set_option auto.mono.ciInstDefEq.mode "reducible"

example {a b : st} (h : (unfoldedTestRec 1 a b).x = 1) : False := by
  auto u[unfoldedTestRec]

example {a b : st} : (unfoldedTestRec (-1) a b).x = -1 := by
  auto u[unfoldedTestRec]

3. Keep the default transparency mode but force Lean-auto to reduce the goal to FOL. By default Lean-auto supports higher-order reasoning with duper; switching to FOL mode can avoid the problematic lambda term. Since this reduction may fail (and does fail here), you should also tell Lean-auto to ignore hints it cannot reduce to FOL:

set_option auto.mono.mode "fol"
set_option auto.mono.ignoreNonQuasiHigherOrder true

example {a b : st} (h : (unfoldedTestRec 1 a b).x = 1) : False := by
  auto u[unfoldedTestRec]

example {a b : st} : (unfoldedTestRec (-1) a b).x = -1 := by
  auto u[unfoldedTestRec]

[Yicheng Qian]

@Abdalrhman M Mohamed Thanks for looking into the issue! I have marked Auto.Bool.ite' and Auto.Bool.ofProp as irreducible.

[Kaushik Raghavan]

Thanks a lot for the detailed response and the quick fix @Abdalrhman M Mohamed and @Yicheng Qian !