mathlib documentation

tactic.mk_iff_of_inductive_prop

meta def tactic.mk_iff  :
exprexprexpr

meta def tactic.select  :
tactic unit

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, where ps are the type parameters, is are the indices, j ranges over all possible constructors, the cs are the parameters for each constructors, 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'
meta def mk_iff_of_inductive_prop_cmd  :
interactive.parse (lean.parser.tk "mk_iff_of_inductive_prop")lean.parser unit

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, where ps are the type parameters, is are the indices, j ranges over all possible constructors, the cs are the parameters for each constructors, 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'