Correct use of lean-auto

Stream: new members

[Mike Whalen]

Hello,

I'm a new user of lean and I am trying out lean-auto on a simple model:

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

def Zone.MinArea2 : Zone → Area
  | .Z1    => 12000
  | .Z2    => 7000
  | .Z3     => 4000
  | .Z4     => 3000

example (x : Zone) : x.MinArea1 <= x.MinArea2 := by
  cases x <;> simp

example (x : Zone) : x.MinArea1 <= x.MinArea2 := by
  cases x <;> auto

Simp succeeds but auto fails here. Looking at the generated SMT it looks like MinArea1 and MinArea2 are treated as uninterpreted functions. How do I tell lean-auto to use these definitions?

[Mario Carneiro]

cc: @Yicheng Qian

[Yicheng Qian]

Currently lean-auto does not have good support for match expressions, but that might change in the near future.

[Yicheng Qian]

@Mario Carneiro Is there already code in Lean to generate/obtain equational theorems for aux constants like ?.match_1?

[Mario Carneiro]

I thought it did, but getEqnsFor? only seems to return some if the definition is recursive, and it returns it only for the main recursive definition, not the internal match splitters

[Mario Carneiro]

oh, there is a special function for matchers:

import Lean

def foo : Nat → Nat
  | 0 => 1
  | n+1 => 2

#eval Lean.Meta.Match.getEquationsFor ``foo.match_1

#print foo.match_1
#print foo.match_1.eq_1
#print foo.match_1.eq_2
#print foo.match_1.splitter

def foo.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive 0) → ((n : Nat) → motive (Nat.succ n)) → motive x :=
fun motive x h_1 h_2 ↦ Nat.casesOn x (h_1 ()) fun n ↦ h_2 n

private theorem foo.match_1.eq_1.{u_1} : ∀ (motive : Nat → Sort u_1) (h_1 : Unit → motive 0)
  (h_2 : (n : Nat) → motive (Nat.succ n)),
  (match 0 with
    | 0 => h_1 ()
    | Nat.succ n => h_2 n) =
    h_1 () :=
fun motive h_1 h_2 ↦ id (id (Eq.refl (h_1 ())))

private theorem foo.match_1.eq_2.{u_1} : ∀ (motive : Nat → Sort u_1) (n : Nat) (h_1 : Unit → motive 0)
  (h_2 : (n : Nat) → motive (Nat.succ n)),
  (match Nat.succ n with
    | 0 => h_1 ()
    | Nat.succ n => h_2 n) =
    h_2 n :=
fun motive n h_1 h_2 ↦ id (id (Eq.refl (h_2 n)))

private def foo.match_1.splitter.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → motive 0 → ((n : Nat) → motive (Nat.succ n)) → motive x :=
fun motive x h_1 h_2 ↦ Nat.casesOn x h_1 fun n ↦ h_2 n

[Mike Whalen]

(Hopefully I am replying correctly - still my first post) - I also tried using auto u[Zone.MinArea1, Zone.MinArea2] but got some errors, e.g. lamTerm2STerm :: Unexpected head term Auto.Embedding.Lam.LamTerm.lam (.atom 1) (.app (.base (.nat)) (.base (.icst (.iofNat))) (.base (.ncst (.natVal 10000))))

[Yicheng Qian]

Mario Carneiro said:

oh, there is a special function for matchers:

import Lean

def foo : Nat → Nat
  | 0 => 1
  | n+1 => 2

#eval Lean.Meta.Match.getEquationsFor ``foo.match_1

#print foo.match_1
#print foo.match_1.eq_1
#print foo.match_1.eq_2
#print foo.match_1.splitter

def foo.match_1.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → (Unit → motive 0) → ((n : Nat) → motive (Nat.succ n)) → motive x :=
fun motive x h_1 h_2 ↦ Nat.casesOn x (h_1 ()) fun n ↦ h_2 n

private theorem foo.match_1.eq_1.{u_1} : ∀ (motive : Nat → Sort u_1) (h_1 : Unit → motive 0)
  (h_2 : (n : Nat) → motive (Nat.succ n)),
  (match 0 with
    | 0 => h_1 ()
    | Nat.succ n => h_2 n) =
    h_1 () :=
fun motive h_1 h_2 ↦ id (id (Eq.refl (h_1 ())))

private theorem foo.match_1.eq_2.{u_1} : ∀ (motive : Nat → Sort u_1) (n : Nat) (h_1 : Unit → motive 0)
  (h_2 : (n : Nat) → motive (Nat.succ n)),
  (match Nat.succ n with
    | 0 => h_1 ()
    | Nat.succ n => h_2 n) =
    h_2 n :=
fun motive n h_1 h_2 ↦ id (id (Eq.refl (h_2 n)))

private def foo.match_1.splitter.{u_1} : (motive : Nat → Sort u_1) →
  (x : Nat) → motive 0 → ((n : Nat) → motive (Nat.succ n)) → motive x :=
fun motive x h_1 h_2 ↦ Nat.casesOn x h_1 fun n ↦ h_2 n

Ah, this seems to be what I've been missing! I was only calling getEqnsFor? before.

[Yicheng Qian]

Mike Whalen said:

(Hopefully I am replying correctly - still my first post) - I also tried using auto u[Zone.MinArea1, Zone.MinArea2] but got some errors, e.g. lamTerm2STerm :: Unexpected head term Auto.Embedding.Lam.LamTerm.lam (.atom 1) (.app (.base (.nat)) (.base (.icst (.iofNat))) (.base (.ncst (.natVal 10000))))

Yes, that's another issue in auto. If we unfold these match-expressions, there will be dependently typed terms that auto can't handle. The expected usage is auto d[Zone.MinArea1, Zone.MinArea2], but that doesn't work right now. The first issue is recorded in TODO.md, and the second issue is recorded in Test/SmtTranslation/Inductive.lean (I'll add it to TODO.md).

[Yicheng Qian]

So that's it. Lean-auto is only 4 months old and I'm the only developer of it, so it's pretty rudimentary. It do work on some mathlib examples when used together with duper.

[Mike Whalen]

Sure, no problem. Thank you for your quick response!

[Yicheng Qian]

@Mike Whalen p.s: Recently I've been busy with other stuff and have no time for lean-auto, but it will get better after January 7th next year. Sorry about this.
Issues on github are still welcome.