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.
compactRelation bs as_ps
: Produce a relation of the form:
R := λ 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
.
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
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
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
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 aftercompactRelation
.For example,
List.Chain.nil
has type∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []`
and the first two variables
α
andR
are "params", while thea : α
gets eliminated in acompactRelation
, sovariablesKept = [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, socompactRelation = [false,true,true,true,true]
.The number of equalities, or
none
in the case when we've reduced something of the formp ∧ True
to justp
.
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.
Instances For
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
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
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)]
Instances For
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])
Instances For
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
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
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.
Instances For
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
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.