The @[cfc_pull] attribute

The cfc_pull attribute marks lemmas for use by the cfc_pull tactic and categorizes them according to their shape, and records other information used by the tactic.

inductive Mathlib.Tactic.CFCPull.Kind : Type

What a tagged lemma is for.

• pull : Kind

  ⟨algebraic expression⟩ = cfc f a, usable as a plain simp lemma.

• target : Kind

  Like pull, but the ring, the element or a type is not determined by the algebraic side, e.g. a = cfc (fun x : R ↦ x) a, so simp cannot use the lemma as it is. cfc_pull specializes these at the ring asked for and, if need be (Entry.elemFree), at its targets.

• compose : Kind

  cfc f ⟨structured element⟩ = cfc g a, e.g. cfc f (CFC.abs a) = cfc (f ‖·‖) a.

• conv : Kind

  cfc f a = cfc g a changing the scalar ring or the unitality.

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instInhabitedKind : Inhabited Kind

Equations

• Mathlib.Tactic.CFCPull.instInhabitedKind = { default := Mathlib.Tactic.CFCPull.instInhabitedKind.default }

def Mathlib.Tactic.CFCPull.instBEqKind.beq : Kind → Kind → Bool

Equations

• Mathlib.Tactic.CFCPull.instBEqKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instBEqKind : BEq Kind

Equations

• Mathlib.Tactic.CFCPull.instBEqKind = { beq := Mathlib.Tactic.CFCPull.instBEqKind.beq }

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instReprKind : Repr Kind

Equations

• Mathlib.Tactic.CFCPull.instReprKind = { reprPrec := Mathlib.Tactic.CFCPull.instReprKind.repr }

def Mathlib.Tactic.CFCPull.instReprKind.repr : Kind → ℕ → Std.Format

Equations

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

structure Mathlib.Tactic.CFCPull.Entry : Type

A tagged lemma, in one of the orientations cfc_pull may use it in.

• origin : Lean.Meta.Origin

  The lemma: a declaration, or, from the [..] list of cfc_pull, a local hypothesis (*) or a term.

• term? : Option (Array Lean.Name × Lean.Expr)

  The proof and its universe parameters, as simp elaborated them, when the lemma is a term from the [..] list of cfc_pull.

• inv : Bool

  Whether simp uses it right to left.

• kind : Kind

  Its CFCPUll.Kind: pull, target, compose or conv.

• prio : ℕ

  The attribute priority.

• ring : Option Lean.Name

  The head constant of the scalar ring of the right-hand side, if it is concrete.

• unital : Bool

  Whether the right-hand side is cfc rather than cfcₙ.

• srcRing : Option Lean.Name

  For conv lemmas: the ring of the left-hand side.

• srcUnital : Bool

  For conv lemmas: the unitality of the left-hand side.

• holes : Bool

  For pull and target lemmas: whether the algebraic side has applications of the calculus in it (holes). A lemma without holes is applied top-down, before its argument is simplified.

• freeType : Bool

  For target lemmas: whether some type appears in neither side of the equation, like the S of StarAlgHomClass.map_cfc. cfc_pull has to guess it, and tries the scalar rings it knows.

• elemFree : Bool

  For target lemmas: whether the element has to be supplied, because the algebraic side is the bare element (a = cfc (fun x ↦ x) a, which would match anything) or does not mention it (1 = cfc (fun _ ↦ 1) a). Otherwise simp finds the element by unification, and cfc_pull accepts the rewrite if it is a target.

• elemHead : Option Lean.Name

  For pull and target lemmas: the head constant of the element the calculus is applied to, if it is structured: DFunLike.coe for the φ a of φ (cfc f a) = cfc f (φ a).

• thms : Array Lean.Meta.SimpTheorem

  The lemma as simp uses it, in its orientation and at its priority, if simp can use it on its own, finding the ring and the element by unification: that is, unless it is a target lemma, which cfc_pull specializes when it is called.

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instInhabitedEntry : Inhabited Entry

Equations

• Mathlib.Tactic.CFCPull.instInhabitedEntry = { default := Mathlib.Tactic.CFCPull.instInhabitedEntry.default }

inductive Mathlib.Tactic.CFCPull.SetKind : Type

What the lemmas of a simp set of cfc_pull are for.

• pull : SetKind

  pull lemmas with holes: simp uses them itself.

• towards : SetKind

  pull lemmas with holes towards a structured element (φ (cfc f a) = cfc f (φ a)), used only if that element is a target.

• loose : SetKind

  pull lemmas without holes, at a concrete ring (CFC.sqrt a = cfc √· a): used top-down.

• looseTowards : SetKind

  pull lemmas without holes that are generic in their ring, which they find in a scalar (r • a = cfc (r * ·) a): used top-down, if r is in the ring asked for and a is a target.

• compose : SetKind

  compose lemmas.

• conv : SetKind

  conv lemmas, in one direction.

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instInhabitedSetKind : Inhabited SetKind

Equations

• Mathlib.Tactic.CFCPull.instInhabitedSetKind = { default := Mathlib.Tactic.CFCPull.instInhabitedSetKind.default }

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instBEqSetKind : BEq SetKind

Equations

• Mathlib.Tactic.CFCPull.instBEqSetKind = { beq := Mathlib.Tactic.CFCPull.instBEqSetKind.beq }

def Mathlib.Tactic.CFCPull.instBEqSetKind.beq : SetKind → SetKind → Bool

Equations

• Mathlib.Tactic.CFCPull.instBEqSetKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Mathlib.Tactic.CFCPull.instReprSetKind.repr : SetKind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instReprSetKind : Repr SetKind

Equations

• Mathlib.Tactic.CFCPull.instReprSetKind = { reprPrec := Mathlib.Tactic.CFCPull.instReprSetKind.repr }

structure Mathlib.Tactic.CFCPull.Key : Type

The lemmas of one simp set have the same use, ring and unitality. cfc_pull orders the sets for one use when it knows which ring and unitality are asked for: fewer scalar conversions first, then the requested unitality. Inside a set the priority decides, as always.

• set : SetKind

  The use.

• ring : Option Lean.Name

  The head constant of the scalar ring, if it is concrete.

• unital : Bool

  Whether the calculus is cfc rather than cfcₙ.

• srcRing : Option Lean.Name

  For conv lemmas: the ring converted from.

• srcUnital : Bool

  For conv lemmas: the unitality converted from.

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instInhabitedKey : Inhabited Key

Equations

• Mathlib.Tactic.CFCPull.instInhabitedKey = { default := Mathlib.Tactic.CFCPull.instInhabitedKey.default }

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instBEqKey : BEq Key

Equations

• Mathlib.Tactic.CFCPull.instBEqKey = { beq := Mathlib.Tactic.CFCPull.instBEqKey.beq }

def Mathlib.Tactic.CFCPull.instBEqKey.beq : Key → Key → Bool

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.CFCPull.instBEqKey.beq x✝¹ x✝ = false

def Mathlib.Tactic.CFCPull.Entry.key? (e : Entry) : Option Key

The simp set a lemma goes to when it is tagged, if it is not one cfc_pull specializes.

Equations

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

structure Mathlib.Tactic.CFCPull.State : Type

The @[cfc_pull] lemmas, and the simp sets of those simp can use on its own.

• entries : Array Entry

  The lemmas.

• sets : Array (Key × Lean.Meta.SimpTheorems)

  The simp sets.

@[instance_reducible]

instance Mathlib.Tactic.CFCPull.instInhabitedState : Inhabited State

Equations

• Mathlib.Tactic.CFCPull.instInhabitedState = { default := Mathlib.Tactic.CFCPull.instInhabitedState.default }

def Mathlib.Tactic.CFCPull.State.insert (s : State) (k : Key) (thms : Array Lean.Meta.SimpTheorem) : State

Add lemmas to a simp set.

Equations

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

def Mathlib.Tactic.CFCPull.State.add (s : State) (e : Entry) : State

Add a lemma, to its simp set too if it has one.

Equations

• s.add e = match e.key? with | some k => { entries := s.entries.push e, sets := s.sets }.insert k e.thms | none => { entries := s.entries.push e, sets := s.sets }

def Mathlib.Tactic.CFCPull.State.erase (s : State) (declName : Lean.Name) : State

Remove the lemmas of a declaration.

Equations

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

opaque Mathlib.Tactic.CFCPull.cfcPullExt : Lean.SimpleScopedEnvExtension Entry State

The environment extension holding the @[cfc_pull] lemmas.

def Mathlib.Tactic.CFCPull.matchCFC? (e : Lean.Expr) : Option (Lean.Expr × Bool × Lean.Expr × Lean.Expr)

Recognise cfc f a or cfcₙ f a: (ring, unital, fn, elem).

Equations

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

def Mathlib.Tactic.CFCPull.Entry.proof (e : Entry) : Lean.MetaM Lean.Expr

The lemma as a term, with fresh universe metavariables.

Equations

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

def Mathlib.Tactic.CFCPull.mkEntries? (origin : Lean.Meta.Origin) (type : Lean.Expr) (prio : ℕ) (term? : Option (Array Lean.Name × Lean.Expr) := none) : Lean.MetaM (Option (Array Entry))

Classify a lemma of type type: the entries recording how cfc_pull may use it, or none if it is not an equation with cfc or cfcₙ at the head of a side.

Equations

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

def Mathlib.Tactic.CFCPull.mkEntries (origin : Lean.Meta.Origin) (type : Lean.Expr) (prio : ℕ) : Lean.MetaM (Array Entry)

Classify a lemma of type type, which must be one cfc_pull can use.

Equations

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

def Mathlib.Tactic.CFCPull.cfcPullAttr : Lean.ParserDescr

The cfc_pull attribute marks lemmas for use by the cfc_pull tactic. Such a lemma is an equation with cfc or cfcₙ at the head of at least one side. The attribute sorts lemmas into the following categories and records other information used by the tactic, including the scalar ring, unitality, and whether the algebraic side contains applications of cfc (holes).

category	shape	example
pull	cfc f a = ⟨an expression in the algebra⟩	cfc_mul
target	a pull lemma whose algebraic side does not fix R	cfc_id'
conv	cfc (f : R → R) a = cfc (g : S → S) a, cfcₙ f a = cfc f a	cfcₙ_eq_cfc
compose	cfc (f ∘ g) a = cfc f ⟨an expression in a⟩	cfc_comp_pow

Equations

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