lean-auto failure on simple model.

[mww-aws]

I have a trivial Lean spec:

import Auto
import Std.Data.BitVec
set_option auto.smt true
set_option auto.smt.trust true
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true

inductive Zone where
  | Z1 | Z2 | Z3 | Z4
  -- Ask Lean to automatically show that type is not empty, has a representation function, and
  -- equality is decidable
  deriving Inhabited, Repr, DecidableEq

abbrev Area : Type := Int

def Zone.MinArea1 : Zone → Area
  | .Z1    => 10000
  | .Z2    => 5000
  | .Z3     => 3500
  | .Z4     => 2500

example (x: Zone) : x.MinArea1 >= 2500 := by cases x <;> simp -- succeeds
example (x: Zone) : x.MinArea1 >= 2500 := by cases x <;> auto -- fails

I can't seem to prove it by auto because it is not expanding the definition of MinArea1:

[auto.smt.printCommands] (declare-sort |Empty| 0) 

[auto.smt.printCommands] (define-fun |nsub| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|>=| |x| |y|) (|-| |x| |y|) 0)) 

[auto.smt.printCommands] (define-fun |itdiv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|div| |x| |y|) (|-| (|div| (|-| |x|) |y|))))) 

[auto.smt.printCommands] (define-fun |itmod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|ite| (|>=| |x| 0) (|mod| |x| |y|) (|-| (|mod| (|-| |x|) |y|))))) 

[auto.smt.printCommands] (define-fun |iediv| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) 0 (|div| |x| |y|))) 

[auto.smt.printCommands] (define-fun |iemod| ((|x| |Int|) (|y| |Int|)) |Int| (|ite| (|=| |y| 0) |x| (|mod| |x| |y|))) 

[auto.smt.printCommands] (declare-datatypes ((smti_0 0)) (((|smti_1|) (|smti_2|) (|smti_3|) (|smti_4|)))) 

[auto.smt.printCommands] (declare-fun |smti_5| (|smti_0|) |Int|) 

[auto.smt.printCommands] (assert (! (|not| (|<=| 2500 (|smti_5| |smti_1|))) :named valid_fact_0)) 

[auto.smt.result] z3 says Sat, model:
    ((|define-fun| |valid_fact_0| () |Bool| (|not| (|<=| 2500 (|smti_5| |smti_1|)))) (|define-fun| |smti_5| ((|x!0| |smti_0|)) |Int| 0))
    stderr:

I have tried a couple of things like asking lean-auto to unfold Zone.MinArea1: auto u[Zone.MinArea1] but this leads to an error: lamTerm2STerm :: Unexpected head term Auto.Embedding.Lam.LamTerm.lam (.atom 1) (.app (.base (.nat)) (.base (.icst (.iofNat))) (.base (.ncst (.natVal 10000))))

Can you tell me how to complete this proof properly? Also, is it possible to get lean-auto to handle the cases part?

[PratherConid]

@mww-aws This is a very involved issue. At first glance, I believe to fully fix this we need to implement (1) Support for complicated dependent types (at least for recursors), or support for obtaining definitional equality for functions whose body contain match (2) Translation from higher-order logic to first-order logic.
At this point it's unclear to me how exactly I should implement support for these two features because there are a lot of design choices to make. I'll look more into this issue after Jan 7th next year.
If it's ok to you, you can manually prove the four definitional equalities related to Zone.MinArea1, and supply them to auto.

[mww-aws]

O.k., I can prove those. How would I submit them to auto? Could you give a concrete example, then I can generalize.

[PratherConid]

The cases x is indeed not necessary in these examples.

[PratherConid]

Okay, fixed. Now a more complex lemdb example is recorded in https://github.com/leanprover-community/lean-auto/blob/main/Test/LemDBTest.lean and the no-lemdb example is recorded in https://github.com/leanprover-community/lean-auto/blob/main/Test/SmtTranslation/MatchWorkaround.lean