# mk_iff_of_inductive_prop #

This file defines a tactic `tactic.mk_iff_of_inductive_prop`

that generates `iff`

rules for
inductive `Prop`

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

- Mathlib.Tactic.MkIff.mkOpList op empty [] = empty
- Mathlib.Tactic.MkIff.mkOpList op empty [e] = e
- Mathlib.Tactic.MkIff.mkOpList op empty (e :: es) = Lean.mkApp2 op e (Mathlib.Tactic.MkIff.mkOpList op empty es)

`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

Drops the final element of a list.

## Equations

- Mathlib.Tactic.MkIff.List.init [] = []
- Mathlib.Tactic.MkIff.List.init [head] = []
- Mathlib.Tactic.MkIff.List.init (a :: l) = a :: Mathlib.Tactic.MkIff.List.init l

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]`

.The number of equalities, or

`none`

in the case when we've reduced something of the form`p ∧ True∧ True`

to just`p`

.

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

## Instances For

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.

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.
- Mathlib.Tactic.MkIff.nCasesSum 0 mvar h = 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.
- Mathlib.Tactic.MkIff.nCasesProd 0 mvar h = pure (mvar, [h])

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

- Mathlib.Tactic.MkIff.listBoolMerge [] x = []
- Mathlib.Tactic.MkIff.listBoolMerge (false :: xs) x = none :: Mathlib.Tactic.MkIff.listBoolMerge xs x
- Mathlib.Tactic.MkIff.listBoolMerge (true :: xs) (y :: ys) = some y :: Mathlib.Tactic.MkIff.listBoolMerge xs ys
- Mathlib.Tactic.MkIff.listBoolMerge (true :: tail) [] = []

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.