Documentation

Batteries.Tactic.Trans

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 br b cr a c

Compose using transitivity, homogeneous case.

Equations
Instances For

    solving e ← mkAppM' f #[x]

    Equations
    Instances For

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

      Equations
      Instances For

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

        Equations
        Instances For

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

          Instances For

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

            Equations
            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

                Synonym for trans tactic.

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