trans tactic

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

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

Compose using transitivity, homogeneous case.

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

Environment extension storing transitivity lemmas

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

solving e ← mkAppM' f #[x]

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

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

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

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

inductive Batteries.Tactic.TransRelation : Type

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

• app (rel : Lean.Expr) : TransRelation

  Expression for transitive relation.

• implies (name : Lean.Name) (bi : Lean.BinderInfo) : TransRelation

  Constant name for transitive relation.

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

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

def Batteries.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.

def Batteries.Tactic.tacticTransitivity___ : Lean.ParserDescr

Synonym for trans tactic.