porting leaneuclid to use lean auto

Stream: general

[Frederick Pu]

I'm trying to port lean euclid to use lean-auto. Namely, I'm making a tactic eauto that wraps lean auto by passing all lemmas tagged with the specified attribute tag. For example eauto euclid [*] would call auto with all of the lemmas tagged with @[euclid].

import Lean
import Qq
import Auto

import SystemE.Tactic.Attr

open Lean Elab Tactic Meta Simp

namespace Auto

syntax (name := eauto) "eauto" ident autoinstr hints (uord)* : tactic

#check InputHints
def collectAllLemmas'
  (inputHints : InputHints) (unfoldInfos : Array Prep.ConstUnfoldInfo) (defeqNames : Array Name) (ngoalAndBinders : Array FVarId) :
  -- The first `Array Lemma` are `Prop` lemmas
  -- The second `Array Lemma` are Inhabitation facts
  TacticM (Array Lemma × Array Lemma) := do
  let unfoldInfos ← Prep.topoSortUnfolds unfoldInfos
  let startTime ← IO.monoMsNow
  let lctxLemmas ← collectLctxLemmas inputHints.lctxhyps ngoalAndBinders
  let lctxLemmas ← lctxLemmas.mapM (m:=MetaM) (unfoldConstAndPreprocessLemma unfoldInfos)
  traceLemmas `auto.printLemmas "Lemmas collected from local context:" lctxLemmas
  checkDuplicatedFact inputHints.terms
  checkDuplicatedLemmaDB inputHints.lemdbs
  let userLemmas := (← collectUserLemmas inputHints.terms) ++ (← collectHintDBLemmas inputHints.lemdbs)
  let userLemmas ← userLemmas.mapM (m:=MetaM) (unfoldConstAndPreprocessLemma unfoldInfos)
  traceLemmas `auto.printLemmas "Lemmas collected from user-provided terms:" userLemmas
  let defeqLemmas ← collectDefeqLemmas defeqNames
  let defeqLemmas ← defeqLemmas.mapM (m:=MetaM) (unfoldConstAndprepReduceDefeq unfoldInfos)
  traceLemmas `auto.printLemmas "Lemmas collected from user-provided defeq hints:" defeqLemmas
  trace[auto.tactic] "Preprocessing took {(← IO.monoMsNow) - startTime}ms"
  let inhFacts ← Inhabitation.getInhFactsFromLCtx
  let inhFacts ← inhFacts.mapM (m:=MetaM) (unfoldConstAndPreprocessLemma unfoldInfos)
  traceLemmas `auto.printLemmas "Inhabitation lemmas :" inhFacts
  return (lctxLemmas ++ userLemmas ++ defeqLemmas, inhFacts)

@[tactic eauto]
def evalEAuto : Tactic
| `(eauto | eauto $attr $instr $hints $[$uords]*) => withMainContext do
  -- Suppose the goal is `∀ (x₁ x₂ ⋯ xₙ), G`
  -- First, apply `intros` to put `x₁ x₂ ⋯ xₙ` into the local context,
  --   now the goal is just `G`
  let (goalBinders, newGoal) ← (← getMainGoal).intros
  let [nngoal] ← newGoal.apply (.const ``Classical.byContradiction [])
    | throwError "{decl_name%} :: Unexpected result after applying Classical.byContradiction"
  let (ngoal, absurd) ← MVarId.intro1 nngoal
  replaceMainGoal [absurd]
  withMainContext do
    let instr ← parseInstr instr
    match instr with
    | .none =>
      let ext :=
        match attr.getId with
        | `euclid => euclidExtension
        | `diag => diagExtension
        | `metric => metricExtension
        | `super => superExtension
        | `transfer => transferExtension
        | _ => euclidExtension
      let axioms := ext.getState (← getEnv)
      let mut inputHints ← parseHints hints
      for x in axioms do
        inputHints := { inputHints with terms := inputHints.terms.push (mkIdent x)}
      let (unfoldInfos, defeqNames) ← parseUOrDs uords
      let (lemmas, inhFacts) ← collectAllLemmas' inputHints unfoldInfos defeqNames (goalBinders.push ngoal)
      let declName? ← Elab.Term.getDeclName?
      let proof ← runAuto declName? lemmas inhFacts
      absurd.assign proof
    | .useSorry =>
      let proof ← Meta.mkAppM ``sorryAx #[Expr.const ``False [], Expr.const ``false []]
      absurd.assign proof
| _ => throwUnsupportedSyntax

However, I'm getting significantly worse performance than the original LeanEuclid smt solver command. Is it possible that Point is defined as multiple different sorts in the generated cvc5 smt query?

[Frederick Pu]

for reference this is what some of my queries look like:

 query:
    (set-logic ALL)
    (declare-sort _exTy_0 0)
    (declare-sort _exTy_1 0)
    (declare-fun e!_15 (_exTy_0 _exTy_0 _exTy_1) Bool)
    (declare-fun e!_14 (_exTy_0 _exTy_0 _exTy_0) Bool)
    (declare-sort _exTy_3 0)
    (declare-fun e!_6 (_exTy_0 _exTy_0) _exTy_3)
    (declare-sort _exTy_2 0)
    (declare-fun e!_5 (_exTy_3) _exTy_2)
    (declare-sort _exTy_5 0)
    (declare-fun e!_21 (_exTy_5) _exTy_2)
    (declare-fun e!_0 (_exTy_0 _exTy_1)
...

It seems like the constants such as Point and Circle are showing up as their metavariable id's instead of their actual names. Does lean-smt have issues with handling constants?

[Frederick Pu]

actually it seems that lean auto is unable to infer stuff about real numbers. You need to use the smt command for it to actually understand that the mathlib version of Real corresponds to the smt version

import SystemE
import Smt
import Smt.Real
import Smt.Auto
import Book.Prop02


set_option maxHeartbeats 0
set_option auto.mono.mode "fol"
set_option trace.smt true
set_option auto.mono.ciInstDefEq.mode "reducible"
set_option auto.mono.termLikeDefEq.mode "reducible"

set_option auto.native true

attribute [rebind Auto.Native.solverFunc] Smt.smtSolverFunc

theorem womp (x : ℝ) : x + x = 2 * x := by
  /-
    [smt] goal: False

[smt]
    query:
    (set-logic ALL)
    (declare-sort _exTy_0 0)
    (declare-const e!_3 _exTy_0)
    (declare-fun e!_0 (_exTy_0 _exTy_0) _exTy_0)
    (declare-const e!_1 _exTy_0)
    (declare-fun e!_2 (_exTy_0 _exTy_0) _exTy_0)
    (assert (distinct (e!_0 e!_1 e!_1) (e!_2 e!_3 e!_1)))
    (assert (not false))
    (check-sat)

[smt]
    error reason:
    cvc5.Error.error "Expected unsat, got sat"
  -/
  auto

[Frederick Pu]

is there anyway to include axioms and other constants as hints for the smt tactic?

[Josh Clune]

Currently, lean-smt has special support for the reals but lean-auto doesn't. Because of this, running smt on its own can yield a translation that involves smt reals, but running auto with lean-smt as a backend won't (because lean-auto's preprocessing procedure will get rid of reals before lean-smt has a chance to see them).

[Frederick Pu]

Here's my attempt to get lean-smt command to support axioms tagged with @[euclid]:

import Lean

import Smt.Tactic.Smt
import SystemE.Tactic.Attr

namespace Smt

open Lean hiding Command
open Elab Tactic Qq
open Smt Translate Query Reconstruct Util

namespace Tactic

syntax (name := esmt) "esmt" smtHints smtTimeout : tactic

@[tactic esmt]
def evalESmt : Tactic := fun stx => withMainContext do
  let axioms := euclidExtension.getState (← getEnv)
  let hintExprs : List Expr := (← axioms.toList.mapM (fun x => do
    let decl ← getConstInfo x
    return decl.type
  )) ++ (← parseHints ⟨stx[1]⟩)
  let mvs ← Smt.smt (← Tactic.getMainGoal) (hintExprs) (← parseTimeout ⟨stx[2]⟩)
  Tactic.replaceMainGoal mvs

But I still get the following error when I try to run the tactic:

/-
  trying to define _uniq✝⁸⁴⁵⁻⁰ but it has no equational definition and is not a let-decl
-/

[Frederick Pu]

any ideas what's going wrong?

[Josh Clune]

I'm not able to sit down properly and fully debug this at the moment, but off the cuff, it looks like in hintExprs, you're concatenating the list of decl types with the output of parseHints? But parseHints elaborates terms which are supposed to be proofs of relevant facts (not the fact itself). So I'm wondering if your current code is doing something analogous to creating a call like by smt [1 + 1 = 2]