Attributes for the basify tactic

This file declares the three attributes that drive basify, together with the two environment extensions backing them. They live in their own file because Lean cannot use an attribute in the file that declares it; Mathlib/Tactic/Basify.lean documents the tactic itself.

def Parser.Attr.basify_simp : Lean.ParserDescr

The simp set basify runs, after each case split and once at the end: the lemmas that clear away the degenerate branches, where some atom is ⊤ or ⊥, and those that translate a proposition down, such as ↑a ≤ ↑b ↔ a ≤ b. Lemmas tagged @[basify_op] are added here as well.

Equations

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

def Parser.Attr.basify_simp_proc : Lean.ParserDescr

Simplification procedure

Equations

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

The registries

structure Mathlib.Tactic.Basify.ElimEntry : Type

Information about an eliminator registered with @[basify_elim].

• elimName : Lean.Name

  The name of the eliminator, used as cases x using elimName.

• altBinders : Array (Array (Option Lean.Name))

  How to name what each minor premise introduces, one entry per premise and then one per binder, in order. none marks the binder carrying the value -- the one occurring in the alternative's pattern -- which takes the name of the atom being split; any other binder takes that name with its own appended. Splitting x : ℕ+ with an alternative ∀ (n : ℕ) (_pos : 0 < n), C n.toPNat' yields x and x_pos.

@[instance_reducible]

instance Mathlib.Tactic.Basify.instInhabitedElimEntry : Inhabited ElimEntry

Equations

• Mathlib.Tactic.Basify.instInhabitedElimEntry = { default := Mathlib.Tactic.Basify.instInhabitedElimEntry.default }

opaque Mathlib.Tactic.Basify.elimExt : Lean.SimpleScopedEnvExtension (Lean.Name × ElimEntry) (Lean.NameMap ElimEntry)

The eliminators registered with @[basify_elim], indexed by the head symbol of the type they destruct.

opaque Mathlib.Tactic.Basify.opExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.NameSet)

The operations registered with @[basify_op], indexed by the head symbol of the type they act on. These are the applications basify looks inside of when searching for atoms.

def Mathlib.Tactic.Basify.analyzeElim (elimName : Lean.Name) : Lean.MetaM (Lean.Name × ElimEntry)

Read off, from the type of the eliminator elimName, the head symbol of the type it destructs together with how to name what each of its alternatives introduces.

Equations

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

def Mathlib.Tactic.Basify.analyzeOp (opName : Lean.Name) : Lean.MetaM (Array (Lean.Name × Lean.Name))

The operations related by an @[basify_op] lemma ↑(f a₁ … aₙ) = g ↑a₁ … ↑aₙ, namely f and g, each paired with the type it operates on.

Equations

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

def Mathlib.Tactic.Basify.basifyElim : Lean.ParserDescr

@[basify_elim] registers an eliminator for basify to case split with. The declaration must be usable as cases x using foo: it takes a motive, some minor premises and a single target. The type it destructs and the shape of each of its cases are read off from its type.

A subtype is registered the same way, with an eliminator that has a single minor premise. It must present the value through a properly typed constructor rather than Subtype.mk: ℝ≥0 and ℕ+ are semireducible definitions, so a goal mentioning ⟨x, hx⟩ : ℝ≥0 is not type-correct at the transparency simp checks at. See NNReal.recToNNReal, which uses Real.toNNReal.

Equations

• Mathlib.Tactic.Basify.basifyElim = Lean.ParserDescr.node `Mathlib.Tactic.Basify.basifyElim 1024 (Lean.ParserDescr.nonReservedSymbol "basify_elim" false)

def Mathlib.Tactic.Basify.basifyOp : Lean.ParserDescr

@[basify_op] registers an operation of a registered type as one that basify knows how to see inside of, by tagging the lemma that relates it to the corresponding operation of the underlying type, such as ENNReal.coe_add : ↑(a + b) = ↑a + ↑b. Anything else of a registered type is an atom: basify generalizes it and case splits on it rather than descending into it.

The lemma is also added to basify_simp, reversed if ← is given, so that what basify looks inside of it can also rewrite through. That rules out a lemma unusable as a rewrite: ENNReal.coe_ofNat has a no_indexed right-hand side that would match everything when reversed, so Mathlib/Tactic/Basify/ENNReal.lean restates it.

Equations

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