Simp indexing failure

Stream: lean4

[Patrick Massot]

The following example was minimized by @Mario Carneiro from code in the rpow_simptactic.

def bla (_ _ : Nat) : Nat := default
theorem foo {a n : Nat} : bla a (no_index OfNat.ofNat n) = default := rfl

example : bla a 2 = default := by simp only [foo] -- simp made no progress

theorem bar {a n : Nat} : no_index (bla a (OfNat.ofNat n)) = default := rfl
example : bla a 2 = default := by simp only [bar]

[Patrick Massot]

Basically simp isn't able to use this lemma until we tell it to give up on any kind of discrimination. Is this a known issue?

[Eric Wieser]

lean4#2867?

[Timo Carlin-Burns]

You're missing parentheses around OfNat.ofNat n

def bla (_ _ : Nat) : Nat := default
theorem foo {a n : Nat} : bla a (no_index (OfNat.ofNat n)) = default := rfl

example : bla a 2 = default := by simp only [foo] -- success

[Timo Carlin-Burns]

It looks like no_index has no effect on the discrimination tree keys when applied to the head of a function application

-- DiscrTree keys:

-- [Eq, Nat, bla, *, OfNat.ofNat, Nat, *, *, Inhabited.default, Nat, *]
theorem foo {a n : Nat} : bla a (no_index OfNat.ofNat n) = default := rfl
-- [Eq, Nat, bla, *, OfNat.ofNat, Nat, *, *, Inhabited.default, Nat, *]
theorem foo' {a n : Nat} : bla a (OfNat.ofNat n) = default := rfl
-- [Eq, Nat, bla, *, *, Inhabited.default, Nat, *]
theorem foo'' {a n : Nat} : bla a (no_index (OfNat.ofNat n)) = default := rfl
-- [Eq, Nat, bla, *, 2, Inhabited.default, Nat, *]
theorem foo_two : bla a 2 = default := by simp only [foo'']
-- [Eq, Nat, *, Inhabited.default, Nat, *]
theorem bar {a n : Nat} : no_index (bla a (OfNat.ofNat n)) = default := rfl

[Patrick Massot]

How do you get access to those keys?

[Timo Carlin-Burns]

Here is my hacky tactic to get the discr tree keys since I don't know how else to run MetaM (reposted from "writing lemmas about ofNat")

import Mathlib.Tactic.LibrarySearch

def bla (_ _ : Nat) : Nat := default
theorem foo {a n : Nat} : bla a (no_index OfNat.ofNat n) = default := rfl

open Lean Meta Elab Tactic

def defnName : String := "foo"

elab "dbg_discr_key" : tactic => do
  let cinfo := ((←getEnv).find? defnName).get!
  let processed ← Mathlib.Tactic.LibrarySearch.processLemma defnName cinfo
  logInfo m!"{processed}"

example : True :=by
  dbg_discr_key
-- [Eq, Nat, bla, *, OfNat.ofNat, Nat, *, *, Inhabited.default, Nat, *]
  trivial

[Patrick Massot]

Thanks! It would be nice to have an official way of accessing this information.

[Tomas Skrivan]

Here is a simple command #discr_tree_key foo that prints out the key of a simp theorem.

import Lean

open Lean Meta

def discrKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
  let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
  let type ← whnfR type
  match type.eq? with
  | some (_, lhs, _) => DiscrTree.mkPath lhs simpDtConfig
  | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"

open Elab Term
elab "#discr_tree_key" t:term : command => do
  Command.liftTermElabM <| do
    let e ← elabTerm t none
    IO.println ((← discrKey e).map fun key => key.format)

open Elab Term
elab "#discr_tree_key" id:ident : command => do
  Command.liftTermElabM <| do
    let info ← getConstInfo id.getId
    IO.println ((← discrKey info.type).map fun key => key.format)


def bla (_ _ : Nat) : Nat := default
theorem foo {a n : Nat} : bla a (no_index OfNat.ofNat n) = default := rfl
theorem foo' {a n : Nat} : bla a (no_index (OfNat.ofNat n)) = default := rfl


-- #[bla, *, OfNat.ofNat, Nat, *, *]
#discr_tree_key (∀ {a n : Nat}, bla a (OfNat.ofNat n) = default)
-- #[bla, *, OfNat.ofNat, Nat, *, *]
#discr_tree_key (∀ {a n : Nat}, bla a (no_index OfNat.ofNat n) = default)
-- #[bla, *, *]
#discr_tree_key (∀ {a n : Nat}, bla a (no_index (OfNat.ofNat n)) = default)
-- #[bla, *, OfNat.ofNat, Nat, *, *]
#discr_tree_key foo
-- #[bla, *, *]
#discr_tree_key foo'

[Patrick Massot]

Thanks! Can you explain how the simplifier uses those arrays?

[Tomas Skrivan]

Timo Carlin-Burns said:

Here is my hacky tactic to get the discr tree keys since I don't know how else to run MetaM (reposted from "writing lemmas about ofNat")

You can write #eval show MetaM Unit from do ... as in

import Lean
open Lean Meta
#eval show MetaM Unit from do
  let id := Expr.const ``id [levelOne]
  IO.println (← ppExpr (← inferType id))

Just note that the mysterious show α from a is just a sugar for (a : α) i.e. telling elaborator that a should have the type α.

This way you can also eval monads IO, TermElabM, CommandElabM and CoreM.

[Tomas Skrivan]

Patrick Massot said:

Thanks! Can you explain how the simplifier uses those arrays?

It would be better if someone with better understanding of DiscrTree explains this. This array is just an implementation detail of DiscrTree and plays a similar role of a key as in a hash map. Just in discriminatory trees these keys allow for some form of fast pattern matching.

[Mario Carneiro]

I believe it is a preorder traversal of the expression tree, with * replacing subterms that are supposed to be ignored by the indexing

[Mario Carneiro]

the important part is that when you see a constant name, it will only match things with that constant at the head (after reducible whnf), and when you see * it will match anything

[Mario Carneiro]

This is used as a filter on matching lemmas: only lemmas which match in the discrimination tree will have unification attempted, so if you put no_index on the LHS head then the key is just #[*] which matches every expression and then simp will try to unify this lemma against every subterm, which is slow but avoids false negatives