Documentation

Mathlib.Tactic.TFAE

The Following Are Equivalent (TFAE) #

This file provides the tactics tfae_have and tfae_finish for proving goals of the form TFAE [P₁, P₂, ...].

An arrow of the form , , or .

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

    tfae_have introduces hypotheses for proving goals of the form TFAE [P₁, P₂, ...]. Specifically, tfae_have i arrow j introduces a hypothesis of type Pᵢ arrow Pⱼ to the local context, where arrow can be , , or . Note that i and j are natural number indices (beginning at 1) used to specify the propositions P₁, P₂, ... that appear in the TFAE goal list. A proof is required afterward, typically via a tactic block.

    example (h : P → R) : TFAE [P, Q, R] := by
      tfae_have 1 → 3
      · exact h
      ...
    

    The resulting context now includes tfae_1_to_3 : P → R.

    The introduced hypothesis can be given a custom name, in analogy to have syntax:

    tfae_have h : 2 ↔ 3
    

    Once sufficient hypotheses have been introduced by tfae_have, tfae_finish can be used to close the goal.

    example : TFAE [P, Q, R] := by
      tfae_have 1 → 2
      · /- proof of P → Q -/
      tfae_have 2 → 1
      · /- proof of Q → P -/
      tfae_have 2 ↔ 3
      · /- proof of Q ↔ R -/
      tfae_finish
    
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      tfae_finish is used to close goals of the form TFAE [P₁, P₂, ...] once a sufficient collection of hypotheses of the form Pᵢ → Pⱼ or Pᵢ ↔ Pⱼ have been introduced to the local context.

      tfae_have can be used to conveniently introduce these hypotheses; see tfae_have.

      Example:

      example : TFAE [P, Q, R] := by
        tfae_have 1 → 2
        · /- proof of P → Q -/
        tfae_have 2 → 1
        · /- proof of Q → P -/
        tfae_have 2 ↔ 3
        · /- proof of Q ↔ R -/
        tfae_finish
      
      Equations
      Instances For

        Setup #

        Extract a list of Prop expressions from an expression of the form TFAE [P₁, P₂, ...] as long as [P₁, P₂, ...] is an explicit list.

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

          Convert an expression representing an explicit list into a list of expressions.

          Proof construction #

          partial def Mathlib.Tactic.TFAE.dfs (hyps : Array ( × × Lean.Expr)) (atoms : Array Q(Prop)) (i : ) (j : ) (P : Q(Prop)) (P' : Q(Prop)) (hP : Q(«$P»)) :

          Uses depth-first search to find a path from P to P'.

          def Mathlib.Tactic.TFAE.proveImpl (hyps : Array ( × × Lean.Expr)) (atoms : Array Q(Prop)) (i : ) (j : ) (P : Q(Prop)) (P' : Q(Prop)) :
          Lean.MetaM Q(«$P»«$P'»)

          Prove an implication via depth-first traversal.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            partial def Mathlib.Tactic.TFAE.proveChain (hyps : Array ( × × Lean.Expr)) (atoms : Array Q(Prop)) (i : ) (is : List ) (P : Q(Prop)) (l : Q(List Prop)) :
            Lean.MetaM Q(List.Chain (fun (x x_1 : Prop) => xx_1) «$P» «$l»)

            Generate a proof of Chain (· → ·) P l. We assume P : Prop and l : List Prop, and that l is an explicit list.

            partial def Mathlib.Tactic.TFAE.proveGetLastDImpl (hyps : Array ( × × Lean.Expr)) (atoms : Array Q(Prop)) (i : ) (i' : ) (is : List ) (P : Q(Prop)) (P' : Q(Prop)) (l : Q(List Prop)) :
            Lean.MetaM Q(List.getLastD «$l» «$P'»«$P»)

            Attempt to prove getLastD l P' → P given an explicit list l.

            def Mathlib.Tactic.TFAE.proveTFAE (hyps : Array ( × × Lean.Expr)) (atoms : Array Q(Prop)) (is : List ) (l : Q(List Prop)) :

            Attempt to prove a statement of the form TFAE [P₁, P₂, ...].

            Instances For

              tfae_have components #

              def Mathlib.Tactic.TFAE.mkTFAEHypName (i : Lean.TSyntax `num) (j : Lean.TSyntax `num) (arr : Lean.TSyntax `Mathlib.Tactic.TFAE.impArrow) :

              Construct a name for a hypothesis introduced by tfae_have.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                def Mathlib.Tactic.TFAE.tfaeHaveCore (goal : Lean.MVarId) (name : Option (Lean.TSyntax `ident)) (i : Lean.TSyntax `num) (j : Lean.TSyntax `num) (arrow : Lean.TSyntax `Mathlib.Tactic.TFAE.impArrow) (t : Lean.Expr) :

                The core of tfae_have, which behaves like haveLetCore in Mathlib.Tactic.Have.

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

                  Turn syntax for a given index into a natural number, as long as it lies between 1 and maxIndex.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Mathlib.Tactic.TFAE.mkImplType (Pi : Q(Prop)) (arr : Lean.TSyntax `Mathlib.Tactic.TFAE.impArrow) (Pj : Q(Prop)) :

                    Construct an expression for the type Pj → Pi, Pi → Pj, or Pi ↔ Pj given expressions Pi Pj : Q(Prop) and impArrow syntax arr, depending on whether arr is , , or respectively.

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

                      Tactic implementation #