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

def Mathlib.Tactic.Propose.discrTreeConfig : Lean.Meta.WhnfCoreConfig

Configuration for DiscrTree.

Equations

• Mathlib.Tactic.Propose.discrTreeConfig = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }

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 : Array Lean.Expr) (required : Array Lean.Expr) (depth : Nat) : Lean.MetaM PUnit

Shortcut for calling solveByElim.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Propose.propose (lemmas : Lean.Meta.DiscrTree Lean.Name) (type : Lean.Expr) (required : Array Lean.Expr) (solveByElimDepth : optParam 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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.