# mk_iff_of_inductive_prop #

This file defines a command `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'

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

source
partial def Mathlib.Tactic.MkIff.compactRelation :
List Lean.Expr → List (Lean.Expr × Lean.Expr) → List (Option Lean.Expr) × List (Lean.Expr × Lean.Expr) × (Lean.Expr → Lean.Expr)

`compactRelation bs as_ps`: Produce a relation of the form:

    R := fun as ↦ ∃ 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`.

source
def Mathlib.Tactic.MkIff.mkExistsList (args : List Lean.Expr) (inner : Lean.Expr) :
Lean.MetaM Lean.Expr

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

Equations

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

Instances For

source
def Mathlib.Tactic.MkIff.mkOpList (op empty : Lean.Expr) :
List Lean.Expr → Lean.Expr

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

Instances For

source
def Mathlib.Tactic.MkIff.mkAndList :
List Lean.Expr → Lean.Expr

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

Equations

- Mathlib.Tactic.MkIff.mkAndList = Mathlib.Tactic.MkIff.mkOpList (Lean.mkConst `And) (Lean.mkConst `True)

Instances For

source
def Mathlib.Tactic.MkIff.mkOrList :
List Lean.Expr → Lean.Expr

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

Equations

- Mathlib.Tactic.MkIff.mkOrList = Mathlib.Tactic.MkIff.mkOpList (Lean.mkConst `Or) (Lean.mkConst `False)

Instances For

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

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

Instances For

source
structure Mathlib.Tactic.MkIff.Shape :
Type

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

- variablesKept : List Bool

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

  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)

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

- neqs : Option Nat

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

Instances For

source
def Mathlib.Tactic.MkIff.constrToProp (univs : List Lean.Level) (params idxs : List Lean.Expr) (c : Lean.Name) :
Lean.MetaM (Shape × Lean.Expr)

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.

Instances For

source
def Mathlib.Tactic.MkIff.splitThenConstructor (mvar : Lean.MVarId) (n : Nat) :
Lean.MetaM Unit

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.

Instances For

source
def Mathlib.Tactic.MkIff.toCases (mvar : Lean.MVarId) (shape : List Shape) :
Lean.MetaM Unit

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.

Instances For

source
def Mathlib.Tactic.MkIff.nCasesSum (n : Nat) (mvar : Lean.MVarId) (h : Lean.FVarId) :
Lean.MetaM (List (Lean.FVarId × Lean.MVarId))

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

Instances For

source
def Mathlib.Tactic.MkIff.nCasesProd (n : Nat) (mvar : Lean.MVarId) (h : Lean.FVarId) :
Lean.MetaM (Lean.MVarId × List Lean.FVarId)

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

Instances For

source
def Mathlib.Tactic.MkIff.listBoolMerge {α : Type u_1} :
List Bool → List α → List (Option α)

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) [] = []

Instances For

source
def Mathlib.Tactic.MkIff.toInductive (mvar : Lean.MVarId) (cs : List Lean.Name) (gs : List Lean.Expr) (s : List Shape) (h : Lean.FVarId) :
Lean.MetaM Unit

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

Equations

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

Instances For

source
def Mathlib.Tactic.MkIff.mkIffOfInductivePropImpl (ind rel : Lean.Name) (relStx : Lean.Syntax) :
Lean.MetaM Unit

Implementation for both `mk_iff` and `mk_iff_of_inductive_prop`.

Equations

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

Instances For

source
def Mathlib.Tactic.MkIff.mkIff :
Lean.ParserDescr

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

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

See also the user command `mk_iff_of_inductive_prop`.

Equations

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

Instances For

source
def Mathlib.Tactic.MkIff.mkIffOfInductiveProp :
Lean.ParserDescr

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

See also the `mk_iff` user attribute.

Equations

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

Instances For