# Documentation

Mathlib.Tactic.MkIffOfInductiveProp

# mk_iff_of_inductive_prop #

This file defines a tactic tactic.mk_iff_of_inductive_prop that generates iff rules for inductive Props. For example, when applied to List.Chain, it creates a declaration with the following type:

∀ {α : Type _} (R : α → α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∀ {α : Type _} (R : α → α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
→ α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
→ Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∧ Chain R b l ∧ l = b :: l'
∧ l = b :: l'


This tactic can be called using either the mk_iff_of_inductive_prop user command or the mk_iff attribute.

compactRelation bs as_ps: Produce a relation of the form:

R := λ as ∃ bs, Λ_i a_i = p_i[bs]
∃ bs, Λ_i a_i = p_i[bs]


This relation is user-visible, so we compact it by removing each b_j where a p_i = b_j, and hence a_i = b_j. We need to take care when there are p_i and p_j with p_i = p_j = b_k.

Generates an expression of the form ∃(args), inner∃(args), inner. args is assumed to be a list of fvars. When possible, p ∧ q∧ q is used instead of ∃(_ : p), q∃(_ : p), q.

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

mkOpList op empty [x1, x2, ...] is defined as op x1 (op x2 ...). Returns empty if the list is empty.

Equations

mkAndList [x1, x2, ...] is defined as x1 ∧ (x2 ∧ ...)∧ (x2 ∧ ...)∧ ...), or True if the list is empty.

Equations

mkOrList [x1, x2, ...] is defined as x1 ∨ (x2 ∨ ...)∨ (x2 ∨ ...)∨ ...), or False if the list is empty.

Equations
def Mathlib.Tactic.MkIff.List.init {α : Type u_1} :
List αList α

Drops the final element of a list.

Equations
• = []
• For each forall-bound variable in the type of the constructor, minus the "params" that apply to the entire inductive type, this list contains true if that variable has been kept after compactRelation.

For example, List.Chain.nil has type

  ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []
∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []
→ α → Prop} {a : α}, List.Chain R a []
→ Prop} {a : α}, List.Chain R a []


and the first two variables α and R are "params", while the a : α gets eliminated in a compactRelation, so variablesKept = [false].

List.Chain.cons has type

  ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
R a b → List.Chain R b l → List.Chain R a (b :: l)
∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α},
R a b → List.Chain R b l → List.Chain R a (b :: l)
→ α → Prop} {a b : α} {l : List α},
R a b → List.Chain R b l → List.Chain R a (b :: l)
→ Prop} {a b : α} {l : List α},
R a b → List.Chain R b l → List.Chain R a (b :: l)
→ List.Chain R b l → List.Chain R a (b :: l)
→ List.Chain R a (b :: l)


and the a : α gets eliminated, so compactRelation = [false,true,true,true,true].

variablesKept :
• The number of equalities, or none in the case when we've reduced something of the form p ∧ True∧ True to just p.

neqs :

Auxiliary data associated with a single constructor of an inductive declaration.

Instances For
def Mathlib.Tactic.MkIff.constrToProp (univs : ) (params : ) (idxs : ) (c : Lean.Name) :

Converts an inductive constructor c into a Shape that will be used later in while proving the iff theorem, and a proposition representing the constructor.

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

Splits the goal n times via refine ⟨?_,?_⟩, and then applies constructor to close the resulting subgoals.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.MkIff.toCases (mvar : Lean.MVarId) (shape : ) :

Proves the left to right direction of a generated iff theorem. shape is the output of a call to constrToProp.

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

Calls cases on h (assumed to be a binary sum) n times, and returns the resulting subgoals and their corresponding new hypotheses.

Equations
• One or more equations did not get rendered due to their size.
• = pure [(h, mvar)]

Calls cases on h (assumed to be a binary product) n times, and returns the resulting subgoal and the new hypotheses.

Equations
• One or more equations did not get rendered due to their size.
• = pure (mvar, [h])
def Mathlib.Tactic.MkIff.listBoolMerge {α : Type u_1} :
List αList ()

Iterate over two lists, if the first element of the first list is false, insert none into the result and continue with the tail of first list. Otherwise, wrap the first element of the second list with some and continue with the tails of both lists. Return when either list is empty.

Example:

listBoolMerge [false, true, false, true] [0, 1, 2, 3, 4] = [none, (some 0), none, (some 1)]

Equations
def Mathlib.Tactic.MkIff.toInductive (mvar : Lean.MVarId) (cs : ) (gs : ) (h : Lean.FVarId) :

Proves the right to left direction of a generated iff theorem.

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

Implementation for both mk_iff and mk_iff_of_inductive_prop.y

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

Applying the mk_iff attribute to an inductively-defined proposition mk_iff makes an iff rule r with the shape ∀ps is, i as ↔ ⋁_j, ∃cs, is = cs∀ps is, i as ↔ ⋁_j, ∃cs, is = cs↔ ⋁_j, ∃cs, is = cs⋁_j, ∃cs, is = cs∃cs, is = cs, where ps are the type parameters, is are the indices, j ranges over all possible constructors, the cs are the parameters for each of the constructors, and the equalities is = cs are the instantiations for each constructor for each of the indices to the inductive type i.

In each case, we remove constructor parameters (i.e. cs) when the corresponding equality would be just c = i for some index i.

For example, if we try the following:

@[mk_iff]
structure Foo (m n : Nat) : Prop where
equal : m = n
sum_eq_two : m + n = 2


Then #check Foo_iff returns:

Foo_iff : ∀ (m n : Nat), Foo m n ↔ m = n ∧ m + n = 2
∀ (m n : Nat), Foo m n ↔ m = n ∧ m + n = 2
↔ m = n ∧ m + n = 2
∧ m + n = 2


You can add an optional string after mk_iff to change the name of the generated lemma. For example, if we try the following:

@[mk_iff bar]
structure Foo (m n : Nat) : Prop where
equal : m = n
sum_eq_two : m + n = 2


Then #check bar returns:

bar : ∀ (m n : ℕ), Foo m n ↔ m = n ∧ m + n = 2
∀ (m n : ℕ), Foo m n ↔ m = n ∧ m + n = 2
↔ m = n ∧ m + n = 2
∧ m + n = 2


See also the user command mk_iff_of_inductive_prop.

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

mk_iff_of_inductive_prop i r makes an iff rule for the inductively-defined proposition i. The new rule r has the shape ∀ps is, i as ↔ ⋁_j, ∃cs, is = cs∀ps is, i as ↔ ⋁_j, ∃cs, is = cs↔ ⋁_j, ∃cs, is = cs⋁_j, ∃cs, is = cs∃cs, is = cs, where ps are the type parameters, is are the indices, j ranges over all possible constructors, the cs are the parameters for each of the constructors, and the equalities is = cs are the instantiations for each constructor for each of the indices to the inductive type i.

In each case, we remove constructor parameters (i.e. cs) when the corresponding equality would be just c = i for some index i.

For example, mk_iff_of_inductive_prop on List.Chain produces:

∀ { α : Type _} (R : α → α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∀ { α : Type _} (R : α → α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
→ α → Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
→ Prop) (a : α) (l : List α),
Chain R a l ↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
↔ l = [] ∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∨ ∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∃(b : α) (l' : List α), R a b ∧ Chain R b l ∧ l = b :: l'
∧ Chain R b l ∧ l = b :: l'
∧ l = b :: l'


See also the mk_iff` user attribute.

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