mathlib3 documentation

tactic.tfae

The Following Are Equivalent (TFAE) #

This file provides the tactics tfae_have and tfae_finish for proving the pairwise equivalence of propositions in a set using various implications between them.

source
@[protected, instance]
def tactic.tfae.arrow.inhabited  :
inhabited tactic.tfae.arrow
source
@[protected, instance]
meta def tactic.tfae.arrow.has_reflect  :
has_reflect tactic.tfae.arrow
source
inductive tactic.tfae.arrow  :
Type
Instances for tactic.tfae.arrow
source
meta def tactic.tfae.mk_implication (re : tactic.tfae.arrow) (e₁ e₂ : expr) :
pexpr
source
meta def tactic.tfae.mk_name (re : tactic.tfae.arrow) (i₁ i₂ : ℕ) :
name
source
meta def tactic.interactive.parse_list  :
expr → option (list expr)
source
meta def tactic.interactive.tfae_have (h : interactive.parse (optional lean.parser.ident <* lean.parser.tk ":")) (i₁ : interactive.parse (interactive.with_desc ↑"i" lean.parser.small_nat)) (re : interactive.parse ((lean.parser.tk "→" <|> lean.parser.tk "->") *> return tactic.tfae.arrow.right <|> (lean.parser.tk "↔" <|> lean.parser.tk "<->") *> return tactic.tfae.arrow.left_right <|> (lean.parser.tk "←" <|> lean.parser.tk "<-") *> return tactic.tfae.arrow.left)) (i₂ : interactive.parse (interactive.with_desc ↑"j" lean.parser.small_nat)) :
tactic unit

In a goal of the form tfae [a₀, a₁, a₂], tfae_have : i → j creates the assertion aᵢ → aⱼ. The other possible notations are tfae_have : i ← j and tfae_have : i ↔ j. The user can also provide a label for the assertion, as with have: tfae_have h : i ↔ j.

source
meta def tactic.interactive.tfae_finish  :
tactic unit

Finds all implications and equivalences in the context to prove a goal of the form tfae [...].

source
def tactic_doc.tactic.tfae  :
tactic_doc_entry

The tfae tactic suite is a set of tactics that help with proving that certain propositions are equivalent. In data/list/basic.lean there is a section devoted to propositions of the form

tfae [p1, p2, ..., pn]

where p1, p2, through, pn are terms of type Prop. This proposition asserts that all the pi are pairwise equivalent. There are results that allow to extract the equivalence of two propositions pi and pj.

To prove a goal of the form tfae [p1, p2, ..., pn], there are two tactics. The first tactic is tfae_have. As an argument it takes an expression of the form i arrow j, where i and j are two positive natural numbers, and arrow is an arrow such as →, ->, ←, <-, ↔, or <->. The tactic tfae_have : i arrow j sets up a subgoal in which the user has to prove the equivalence (or implication) of pi and pj.

The remaining tactic, tfae_finish, is a finishing tactic. It collects all implications and equivalences from the local context and computes their transitive closure to close the main goal.

tfae_have and tfae_finish can be used together in a proof as follows:

example (a b c d : Prop) : tfae [a,b,c,d] :=
begin
  tfae_have : 3 → 1,
  { /- prove c → a -/ },
  tfae_have : 2 → 3,
  { /- prove b → c -/ },
  tfae_have : 2 ← 1,
  { /- prove a → b -/ },
  tfae_have : 4 ↔ 2,
  { /- prove d ↔ b -/ },
    -- a b c d : Prop,
    -- tfae_3_to_1 : c → a,
    -- tfae_2_to_3 : b → c,
    -- tfae_1_to_2 : a → b,
    -- tfae_4_iff_2 : d ↔ b
    -- ⊢ tfae [a, b, c, d]
  tfae_finish,
end