New `propose` tactic

Stream: mathlib4

[Scott Morrison]

An announcement for mathlib4 users who don't necessarily watch the RSS stream: we've just merged a new tactic propose, which is a forwards reasoning analogue of library_search.

• propose using a, b, c tries to find a lemma
  which makes use of each of the local hypotheses a, b, c,
  and reports any results via trace messages.

• propose : h using a, b, c only returns lemmas whose type matches h (which may contain _).

• propose! using a, b, c will also call have to add results to the local goal state.

propose should not be left in proofs; it is a search tool, like library_search.

Please try it out and see if it is useful to you! Bug reports, mysteriously missing results, complaints about speed, etc, all welcome. :-)

[Scott Morrison]

Example usage:

example (K L M : List α) (w : L.Disjoint M) (m : K ⊆ L) : True := by
  propose using w
  -- Prints:
  -- have : List.Disjoint K M := List.disjoint_of_subset_left m w
  -- have : List.Disjoint M L := List.disjoint_symm w
  trivial

[Scott Morrison]

Under the hood this just uses a discrimination tree indexed on the hypotheses of theorems (as opposed to the conclusions, for library_search).

[Johan Commelin]

@Scott Morrison So is propose : h similar to observe : h in mathlib3?

[Scott Morrison]

Oh, you mean without a using clause? That doesn't even parse. :-)

[Johan Commelin]

aha...

[Johan Commelin]

Does propose : h using * parse?

[Scott Morrison]

No, it doesn't, unfortunately.

[Scott Morrison]

Note that in propose : h using ... we only use h to filter results after we've found them. We do not use h for indexing!

[Scott Morrison]

We also have library_search using x, however, which looks up lemmas using the goal, but then only shows results that make use of x.

[Scott Morrison]

I'm not sure what propose : h using * would mean. Using at least one of the hypotheses?

[Johan Commelin]

Or even none.

[Johan Commelin]

propose : n! > 0 is my favorite example...

[Johan Commelin]

Should propose take an optional name? Like propose myFancyName : x^n + y^n = z^n using h1 h2 h3?

[Patrick Massot]

Is there any specific reason why this was renamed from suggest to propose? Is this meant to be very different from mathlib3's suggest?

[Johan Commelin]

I think that in ml4 library_search is already doing what suggest did (but with some rough edges)

[Johan Commelin]

propose is a more precise tactic, because you allow it to filter for specific forward steps.

[Scott Morrison]

Sorry for the confusion. This has nothing to do with mathlib's suggest.

[Scott Morrison]

This uses "forward reasoning", i.e. propose using x does not look at the goal at all.

[Scott Morrison]

Instead it looks up lemmas which could use x as a hypothesis.

[Scott Morrison]

propose : h using x then filters those results to only take those whose type matches h.

[Scott Morrison]

That does have overlap with library_search using x. The difference is that library_search is working by "backwards reasoning", i.e. using the type of the goal to look up the candidate lemmas.

[Scott Morrison]

mathlib's suggest is now just part of library_search. If library_search doesn't find a complete solution it prints that partial solutions (i.e. that still have subgoals). This mode of library_search could definitely use some love.

[Scott Morrison]

@Patrick Massot, if you're able to come up with a better phrase for explaining this than "forwards reasoning", please let me know! I appreciate that it is not immediately clear how propose and library_search operate differently,

[Patrick Massot]

Ok, I indeed completely misunderstood the topic of this discussion. I don't have a great naming idea but there is a very clear way to improve the description in the first message of this thread. The key point is "propose using x does not look at the goal at all."

[Mario Carneiro]

yeah, I don't think english usage helps to differentiate propose and suggest

[Siddhartha Gadgil]

This may be useless, but if propose does not look at the goal at all, should it be in a lower monad, TermElabM or even MetaM? There may be additional uses this way.

[Arthur Paulino]

Idea: helpme so helpme using x reads just fine

[Scott Morrison]

@Siddhartha Gadgil the plumbing tactic has signature:

def propose (lemmas : DiscrTree Name s) (type : Expr) (required : Array Expr)
    (solveByElimDepth := 15) : MetaM (Array (Name × Expr)) := ...

[Kyle Miller]

@Scott Morrison Today @Johan Commelin and I were looking at a hack to get n! to work. It's sort of similar to how dot notation works (at least in the Lean 3 model) where you try to resolve the full name, then you pop off the end and try to resolve that as dot notation, recursively. In this case, if n! fails to resolve, we can make a term elaborator that then tries n !.

import Lean
import Mathlib.Data.Nat.Factorial.Basic

namespace Factorial!
open Lean Elab Term Meta

def elabIdentFactorial : TermElab := fun stx expectedType? =>
  match stx with
  | `($name:ident) => do
    let name := name.getId
    if name.hasMacroScopes then
      -- I think this would mean the name appears from within a quote.
      -- I'm not sure how to properly deal with this, and it seems ok to just not.
      throwUnsupportedSyntax
    else
      try
        elabIdent stx expectedType?
      catch e =>
        match name with
        | .str n s =>
          if s.endsWith "!" then
            let name' := Name.str n (s.dropRight 1)
            try
              elabTerm (← `(Nat.factorial $(mkIdent name'))) expectedType?
            catch _ =>
              throw e
          else
            throw e
        | _ => throw e
  | _ => throwUnsupportedSyntax

attribute [scoped term_elab ident] elabIdentFactorial

end Factorial!

open scoped Nat Factorial!

variable (x : Nat)
#check x !
#check x!

def f (z : Nat) : Nat := z!

example : f 4 = 24 := rfl

def s := {n | n! ≤ 3}

example : s = {n | n ! ≤ 3} := rfl

instance : Coe Bool Nat where
  coe
    | true => 1
    | false => 0

example : true! = 1 := rfl

[Kyle Miller]

There's still a bug here with the unused variable linter, where n! doesn't seem to imply that n is being used.

[Scott Morrison]

https://github.com/leanprover-community/mathlib4/pull/3534 updates to documentation to reflect Patrick's suggestion above.