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.

@[protected, instance]
@[protected, instance]
inductive tactic.tfae.arrow  :
Type
Instances for tactic.tfae.arrow
meta def tactic.tfae.mk_implication (re : tactic.tfae.arrow) (e₁ e₂ : expr) :
meta def tactic.tfae.mk_name (re : tactic.tfae.arrow) (i₁ i₂ : ) :

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.

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

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