Propose

This file defines a tactic have? using a, b, c that tries to find a lemma which makes use of each of the local hypotheses a, b, c.

The variant have? : t using a, b, c restricts to lemmas with type t (which may contain _).

Note that in either variant have? does not look at the current goal at all. It is a relative of apply? but for forward reasoning (i.e. looking at the hypotheses) rather than backward reasoning.

import Batteries.Data.List.Basic
import Mathlib.Tactic.Propose

example (K L M : List α) (w : L.Disjoint M) (m : K ⊆ L) : True := by
  have? using w, m -- Try this: `List.disjoint_of_subset_left m w`
  trivial

opaque Mathlib.Tactic.Propose.proposeLemmas : Batteries.Tactic.DeclCache (Lean.Meta.DiscrTree Lean.Name)

def Mathlib.Tactic.Propose.solveByElim (orig : Lean.MVarId) (goals : Array Lean.MVarId) (use required : Array Lean.Expr) (depth : Nat) : Lean.MetaM PUnit

Shortcut for calling solveByElim.

def Mathlib.Tactic.Propose.propose (lemmas : Lean.Meta.DiscrTree Lean.Name) (type : Lean.Expr) (required : Array Lean.Expr) (solveByElimDepth : Nat := 15) : Lean.MetaM (Array (Lean.Name × Lean.Expr))

Attempts to find lemmas which use all of the required expressions as arguments, and can be unified with the given type (which may contain metavariables, which we avoid assigning). We look up candidate lemmas from a discrimination tree using the first such expression.

Returns an array of pairs, containing the names of found lemmas and the resulting application.

def Mathlib.Tactic.Propose.propose' : Lean.ParserDescr

• have? 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.
• have? : h using a, b, c only returns lemmas whose type matches h (which may contain _).
• have?! using a, b, c will also call have to add results to the local goal state.

Note that have? (unlike apply?) does not inspect the goal at all, only the types of the lemmas in the using clause.

have? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as have := f a b c.

def Mathlib.Tactic.Propose.«tacticHave?!:_Using__» : Lean.ParserDescr

• have? 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.
• have? : h using a, b, c only returns lemmas whose type matches h (which may contain _).
• have?! using a, b, c will also call have to add results to the local goal state.

Note that have? (unlike apply?) does not inspect the goal at all, only the types of the lemmas in the using clause.

have? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as have := f a b c.

def Mathlib.Tactic.Propose.«tacticHave!?:_Using__» : Lean.ParserDescr

• have? 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.
• have? : h using a, b, c only returns lemmas whose type matches h (which may contain _).
• have?! using a, b, c will also call have to add results to the local goal state.

Note that have? (unlike apply?) does not inspect the goal at all, only the types of the lemmas in the using clause.

have? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as have := f a b c.