trans tactic

This implements the trans tactic, which can apply transitivity theorems with an optional middle variable argument.

def Mathlib.Tactic.transExt.config : Lean.Meta.WhnfCoreConfig

Discrimation tree settings for the trans extension.

Equations

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

opaque Mathlib.Tactic.transExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)

Environment extension storing transitivity lemmas

def Trans.simple {α : Sort u} {r : α → α → Sort v} {a : α} {b : α} {c : α} [Trans r r r] : r a b → r b c → r a c

Composition using the Trans class in the homogeneous case.

Equations

• Trans.simple = trans

def Trans.het {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {a : α} {b : β} {c : γ} {r : α → β → Sort u} {s : β → γ → Sort v} {t : outParam (α → γ → Sort w)} [Trans r s t] : r a b → s b c → t a c

Composition using the Trans class in the general case.

Equations

• Trans.het = trans

def Mathlib.Tactic.getExplicitFuncArg? (e : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

solving e ← mkAppM' f #[x]

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.getExplicitFuncArg? e = pure none

def Mathlib.Tactic.getExplicitRelArg? (tgt : Lean.Expr) (f : Lean.Expr) (z : Lean.Expr) : Lean.MetaM (Option (Lean.Expr × Lean.Expr))

solving tgt ← mkAppM' rel #[x, z] given tgt = f z

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.getExplicitRelArg? tgt f z = pure none

def Mathlib.Tactic.getExplicitRelArgCore (tgt : Lean.Expr) (rel : Lean.Expr) (x : Lean.Expr) (z : Lean.Expr) : Lean.MetaM (Lean.Expr × Lean.Expr)

refining tgt ← mkAppM' rel #[x, z] dropping more arguments if possible

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.getExplicitRelArgCore tgt rel x z = pure (rel, x)

inductive Mathlib.Tactic.TransRelation : Type

Internal definition for trans tactic. Either a binary relation or a non-dependent arrow.

• app: Lean.Expr → Mathlib.Tactic.TransRelation
• implies: Lean.Name → Lean.BinderInfo → Mathlib.Tactic.TransRelation

def Mathlib.Tactic.getRel (tgt : Lean.Expr) : Lean.MetaM (Option (Mathlib.Tactic.TransRelation × Lean.Expr × Lean.Expr))

Finds an explicit binary relation in the argument, if possible.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.getRel (Lean.Expr.forallE name binderType body info) = pure (some (Mathlib.Tactic.TransRelation.implies name info, binderType, body))
• Mathlib.Tactic.getRel tgt = pure none

def Mathlib.Tactic.tacticTrans___ : Lean.ParserDescr

trans applies to a goal whose target has the form t ~ u where ~ is a transitive relation, that is, a relation which has a transitivity lemma tagged with the attribute [trans].

• trans s replaces the goal with the two subgoals t ~ s and s ~ u.
• If s is omitted, then a metavariable is used instead.

Additionally, trans also applies to a goal whose target has the form t → u, in which case it replaces the goal with t → s and s → u.

Equations

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

def Mathlib.Tactic.tacticTransitivity___ : Lean.ParserDescr

Equations

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