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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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).

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Mathlib.Tactic.TFAE.tfaeFinish = Lean.ParserDescr.node `Mathlib.Tactic.TFAE.tfaeFinish 1024 (Lean.ParserDescr.nonReservedSymbol "tfae_finish" false)

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.

Equations

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

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.

Equations

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

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₂, ...].

Equations

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

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.

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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