The Following Are Equivalent (TFAE)

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

Parsing and syntax

We implement tfae_have in terms of a syntactic have. To support as much of the same syntax as possible, we recreate the parsers for have, except with the changes necessary for tfae_have.

def Mathlib.Tactic.TFAE.Parser.impTo : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.impFrom : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.impIff : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.impArrow : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.tfaeType : Lean.Parser.Parser

A tfae_have type specification, e.g. 1 ↔ 3 The numbers refer to the proposition at the corresponding position in the TFAE goal (starting at 1).

The following parsers are similar to those for have in Lean.Parser.Term, but instead of optType, we use tfaeType := num >> impArrow >> num (as a tfae_have invocation must always include this specification). Also, we disallow including extra binders, as that makes no sense in this context; we also include " : " after the binder to avoid breaking tfae_have 1 → 2 syntax (which, unlike have, omits " : ").

def Mathlib.Tactic.TFAE.Parser.binder : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.tfaeHaveIdLhs : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.tfaeHaveIdDecl : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.tfaeHaveEqnsDecl : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.tfaeHavePatDecl : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.Parser.tfaeHaveDecl : Lean.Parser.Parser

def Mathlib.Tactic.TFAE.tfaeHave : Lean.ParserDescr

tfae_have i → j := t, where the goal is TFAE [P₁, P₂, ...] introduces a hypothesis tfae_i_to_j : Pᵢ → Pⱼ and proof t to the local context. Note that i and j are natural number literals (beginning at 1) used as indices to specify the propositions P₁, P₂, ... that appear in the goal.

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

All features of have are supported by tfae_have, including naming, matching, destructuring, and goal creation.

• tfae_have i ← j := t adds a hypothesis in the reverse direction, of type Pⱼ → Pᵢ.
• tfae_have i ↔ j := t adds a hypothesis in the both directions, of type Pᵢ ↔ Pⱼ.
• tfae_have hij : i → j := t names the introduced hypothesis hij instead of tfae_i_to_j.
• tfae_have i j | p₁ => t₁ | ... matches on the assumption p : Pᵢ.
• tfae_have ⟨hij, hji⟩ : i ↔ j := t destructures the bi-implication into hij : Pᵢ → Pⱼ and hji : Pⱼ → Pⱼ.
• tfae_have i → j := t ?a creates a new goal for ?a.

Examples:

example (h : P → R) : TFAE [P, Q, R] := by
  tfae_have 1 → 3 := h
  -- The resulting context now includes `tfae_1_to_3 : P → R`.
  sorry

-- An example of `tfae_have` and `tfae_finish`:
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish

-- All features of `have` are supported by `tfae_have`:
example : TFAE [P, Q] := by
  -- assert `tfae_1_to_2 : P → Q`:
  tfae_have 1 → 2 := sorry

  -- assert `hpq : P → Q`:
  tfae_have hpq : 1 → 2 := sorry

  -- match on `p : P` and prove `Q` via `f p`:
  tfae_have 1 → 2
  | p => f p

  -- assert `pq : P → Q`, `qp : Q → P`:
  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry

  -- assert `h : P → Q`; `?a` is a new goal:
  tfae_have h : 1 → 2 := f ?a

  sorry

def Mathlib.Tactic.TFAE.tfaeFinish : Lean.ParserDescr

tfae_finish closes 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 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish

Setup

def Mathlib.Tactic.TFAE.getTFAEList (t : Lean.Expr) : Lean.MetaM (Q(List Prop) × List Q(Prop))

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

Proof construction

partial def Mathlib.Tactic.TFAE.dfs (hyps : Array (ℕ × ℕ × Lean.Expr)) (atoms : Array Q(Prop)) (i j : ℕ) (P P' : Q(Prop)) (hP : Q(«$P»)) : StateT (Std.HashSet ℕ) Lean.MetaM 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 P' : Q(Prop)) : Lean.MetaM Q(«$P» → «$P'»)

Prove an implication via depth-first traversal.

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.IsChain (fun (x1 x2 : Prop) => x1 → x2) («$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 P' : Q(Prop)) (l : Q(List Prop)) : Lean.MetaM Q(«$l».getLastD «$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)) : Lean.MetaM Q(«$l».TFAE)

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

tfae_have components

def Mathlib.Tactic.TFAE.mkTFAEId : Lean.TSyntax `Mathlib.Tactic.TFAE.Parser.tfaeType → Lean.MacroM Lean.Name

Construct a name for a hypothesis introduced by tfae_have.

def Mathlib.Tactic.TFAE.elabIndex (i : Lean.TSyntax `num) (maxIndex : ℕ) : Lean.MetaM ℕ

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

Tactic implementation

def Mathlib.Tactic.TFAE.elabTFAEType (tfaeList : List Q(Prop)) : Lean.TSyntax `Mathlib.Tactic.TFAE.Parser.tfaeType → Lean.Elab.TermElabM Lean.Expr

Accesses the propositions at indices i and j of tfaeList, and constructs the expression Pi <arr> Pj, which will be the type of our tfae_have hypothesis

Deprecated "Goal-style" tfae_have

This syntax and its implementation, which behaves like "Mathlib have" is deprecated; we preserve it here to provide graceful deprecation behavior.

opaque Mathlib.Tactic.TFAE.useDeprecated : Lean.Option Bool

Re-enables "goal-style" syntax for tfae_have when true.

def Mathlib.Tactic.TFAE.tfaeHave' : Lean.ParserDescr

tfae_have i → j := t, where the goal is TFAE [P₁, P₂, ...] introduces a hypothesis tfae_i_to_j : Pᵢ → Pⱼ and proof t to the local context. Note that i and j are natural number literals (beginning at 1) used as indices to specify the propositions P₁, P₂, ... that appear in the goal.

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

All features of have are supported by tfae_have, including naming, matching, destructuring, and goal creation.

• tfae_have i ← j := t adds a hypothesis in the reverse direction, of type Pⱼ → Pᵢ.
• tfae_have i ↔ j := t adds a hypothesis in the both directions, of type Pᵢ ↔ Pⱼ.
• tfae_have hij : i → j := t names the introduced hypothesis hij instead of tfae_i_to_j.
• tfae_have i j | p₁ => t₁ | ... matches on the assumption p : Pᵢ.
• tfae_have ⟨hij, hji⟩ : i ↔ j := t destructures the bi-implication into hij : Pᵢ → Pⱼ and hji : Pⱼ → Pⱼ.
• tfae_have i → j := t ?a creates a new goal for ?a.

Examples:

example (h : P → R) : TFAE [P, Q, R] := by
  tfae_have 1 → 3 := h
  -- The resulting context now includes `tfae_1_to_3 : P → R`.
  sorry

-- An example of `tfae_have` and `tfae_finish`:
example : TFAE [P, Q, R] := by
  tfae_have 1 → 2 := sorry /- proof of P → Q -/
  tfae_have 2 → 1 := sorry /- proof of Q → P -/
  tfae_have 2 ↔ 3 := sorry /- proof of Q ↔ R -/
  tfae_finish

-- All features of `have` are supported by `tfae_have`:
example : TFAE [P, Q] := by
  -- assert `tfae_1_to_2 : P → Q`:
  tfae_have 1 → 2 := sorry

  -- assert `hpq : P → Q`:
  tfae_have hpq : 1 → 2 := sorry

  -- match on `p : P` and prove `Q` via `f p`:
  tfae_have 1 → 2
  | p => f p

  -- assert `pq : P → Q`, `qp : Q → P`:
  tfae_have ⟨pq, qp⟩ : 1 ↔ 2 := sorry

  -- assert `h : P → Q`; `?a` is a new goal:
  tfae_have h : 1 → 2 := f ?a

  sorry