# trans tactic #

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

Discrimation tree settings for the trans extension.

Equations
Instances For

Environment extension storing transitivity lemmas

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

Composition using the Trans class in the homogeneous case.

Equations
• Trans.simple = trans
Instances For
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 bs b ct a c

Composition using the Trans class in the general case.

Equations
• Trans.het = trans
Instances For

solving e ← mkAppM' f #[x]

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

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

Equations
• One or more equations did not get rendered due to their size.
• = pure none
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
• = pure (rel, x)
Instances For

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

• app:
• implies:
Instances For

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

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

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.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For