lean-auto

Stream: general

[Alessandro Pinto]

I am trying to use lean-auto. I have the following line in lakefile.lean:

require auto from git "https://github.com/leanprover-community/lean-auto.git" @ "v4.11.0"

I am trying this simple example https://github.com/leanprover-community/lean-auto/blob/main/Test/SmtTranslation/BoolNatInt.lean

I get several errors:

error: .\.\.lake/packages\auto\.\.\Auto\Lib\Pos.lean:108:13: tactic 'rfl' failed, the left-hand side
  ofNat'WF xH.toNat'
is not definitionally equal to the right-hand side
  xH
⊢ ofNat'WF xH.toNat' = xH
error: .\.\.lake/packages\auto\.\.\Auto\Lib\Pos.lean:121:25: tactic 'rfl' failed, the left-hand side
  (ofNat'WF 1).toNat'
is not definitionally equal to the right-hand side
  1
a✝ : 1 ≠ 0
⊢ (ofNat'WF 1).toNat' = 1
error: .\.\.lake/packages\auto\.\.\Auto\Lib\Pos.lean:166:16: tactic 'rfl' failed, the left-hand side
  ofNat'WF 0
is not definitionally equal to the right-hand side
  ofNat'RD 0 0
n : Nat
H : 0 ≥ n
hzero : n = 0
⊢ ofNat'WF 0 = ofNat'RD 0 0
error: Lean exited with code 1

error: .\.\.lake/packages\auto\.\.\Auto\Lib\ExprExtra.lean:395:37: unknown constant 'Lean.MetaEval'
error: .\.\.lake/packages\auto\.\.\Auto\Lib\ExprExtra.lean:396:33: unknown constant 'Lean.runMetaEval'
error: .\.\.lake/packages\auto\.\.\Auto\Lib\ExprExtra.lean:402:35: unknown constant 'Lean.Eval'
error: .\.\.lake/packages\auto\.\.\Auto\Lib\ExprExtra.lean:403:40: unknown constant 'Lean.runEval'
error: .\.\.lake/packages\auto\.\.\Auto\Lib\ExprExtra.lean:459:29: unknown constant 'Lean.MetaEval'
error: Lean exited with code 1

error: .\.\.lake/packages\auto\.\.\Auto\Parser\NDFA.lean:468:82: invalid field 'val', the environment does not contain 'Nat.val'
  idx
has type
  Nat
error: Lean exited with code 1

Any suggestion on how to fix them? I am using leanprover/lean4:v4.15.0-rc1

Thanks
Alessandro

[Kevin Buzzard]

Try using the version of lean which lean-auto uses?

[Alessandro Pinto]

I tried using leanprover/lean4:v4.13.0 (which is the toolchain used by lean-auto)
but I now get the following error:

error: .\.\.lake/packages\proofwidgets\lakefile.lean:20:20: error: invalid argument name 'text' for function 'Lake.buildFileAfterDep'
error: .\.\.lake/packages\proofwidgets\lakefile.lean: package configuration has errors
Invalid Lake configuration.  Please restart the server after fixing the Lake configuration file.

[Mauricio Collares]

Your first line fetches a v4.11.0 tag, what happens if you use leanprover/lean4:v4.11.0?

[Mauricio Collares]

(you might have to delete the .lake directory inside your project)

[Alessandro Pinto]

Thank you for the suggestions. I tried different versions of the toolchain, and I also tried deleting the .lake directory, but I still see the same issues regarding proofwidgets. I'll keep trying.

[Yicheng Qian]

Does the proofwidgets you're using use the same lean version?

[Mauricio Collares]

That's a good point. Why is proofwidgets being imported in the first place? Are you using both lean-auto and mathlib? If so, you must require matching tags. Using mathlib master will cause trouble.

[Mauricio Collares]

If that's not the problem, please post your lakefile.lean file in full

[Max Nowak 🐉]

Lean-auto is a little sensitive to the exact version of Lean and other dependencies used. One data point: I am using Lean 4.12 with lean-auto at commit 680d6d58ce2bb65d15e5711d93111b2e5b22cb1a and those work together.

[Alessandro Pinto]

Max Nowak 🐉 said:

Lean-auto is a little sensitive to the exact version of Lean and other dependencies used. One data point: I am using Lean 4.12 with lean-auto at commit 680d6d58ce2bb65d15e5711d93111b2e5b22cb1a and those work together.

I removed the mathlib dependency, and I am using Lean 4.13. It seems that auto is correctly setup. I am not sure about the output that I am seeing though. For the following Lean program:

import Auto.Tactic
set_option auto.redMode "reducible"
set_option trace.auto.smt.printCommands true
set_option trace.auto.smt.result true
set_option auto.smt.solver.name "z3"

set_option auto.smt true


 -- In `Checker Statistics`, check that the `assertions` field is `4`
  set_option auto.optimizeCheckerProof true in
  set_option trace.auto.buildChecker true in
  example (h₁ : a = b) (h₂ : b = c) (h₃ : c = d) : a = c := by
    auto [h₁, h₂, h₃]

I see the following output:

Tactic state
1 goal
case h
α✝ : Sort u_1
a b c d : α✝
h₁ : a = b
h₂ : b = c
h₃ : c = d
a✝ : ¬a = c
⊢ False

Messages (2)
auto_example.lean:14:4
5
auto_example.lean:14:4
[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-sort |_α.71_| 0)

[auto.smt.printCommands] (declare-fun _d () |_α.71_|)

[auto.smt.printCommands] (assert (! (not (= _d _d)) :named valid_fact_0))

The by auto tactic is marked with a red squiggle.

Any insight?