coercions and constructions #
order #
last #
addition, numerals, and coercion from Nat #
succ and casts into larger Fin types #
Version of succ_one_eq_two
to be used by dsimp
pred #
Recursion and induction principles #
An induction principle for Fin
that considers a given i : Fin n
as given by a sequence of i
applications of Fin.succ
.
The cases in the induction are:
zero
demonstrates the motive for(0 : Fin (n + 1))
for all boundsn
succ
demonstrates the motive forFin.succ
applied to an arbitraryFin
for an arbitrary boundn
Unlike Fin.induction
, the motive quantifies over the bound, and the bound varies at each inductive
step. Fin.succRecOn
is a version of this induction principle that takes the Fin
argument first.
Equations
Instances For
An induction principle for Fin
that considers a given i : Fin n
as given by a sequence of i
applications of Fin.succ
.
The cases in the induction are:
zero
demonstrates the motive for(0 : Fin (n + 1))
for all boundsn
succ
demonstrates the motive forFin.succ
applied to an arbitraryFin
for an arbitrary boundn
Unlike Fin.induction
, the motive quantifies over the bound, and the bound varies at each inductive
step. Fin.succRec
is a version of this induction principle that takes the Fin
argument last.
Equations
Instances For
Proves a statement by induction on the underlying Nat
value in a Fin (n + 1)
.
For the induction:
zero
is the base case, demonstratingmotive 0
.succ
is the inductive step, assuming the motive fori : Fin n
(lifted toFin (n + 1)
withFin.castSucc
) and demonstrating it fori.succ
.
Fin.inductionOn
is a version of this induction principle that takes the Fin
as its first
parameter, Fin.cases
is the corresponding case analysis operator, and Fin.reverseInduction
is a
version that starts at the greatest value instead of 0
.
Equations
Instances For
Proves a statement by induction on the underlying Nat
value in a Fin (n + 1)
.
For the induction:
zero
is the base case, demonstratingmotive 0
.succ
is the inductive step, assuming the motive fori : Fin n
(lifted toFin (n + 1)
withFin.castSucc
) and demonstrating it fori.succ
.
Fin.induction
is a version of this induction principle that takes the Fin
as its last
parameter.
Equations
Instances For
Proves a statement by cases on the underlying Nat
value in a Fin (n + 1)
.
The two cases are:
zero
, used when the value is of the form(0 : Fin (n + 1))
succ
, used when the value is of the form(j : Fin n).succ
The corresponding induction principle is Fin.induction
.
Equations
Instances For
Proves a statement by reverse induction on the underlying Nat
value in a Fin (n + 1)
.
For the induction:
last
is the base case, demonstratingmotive (Fin.last n)
.cast
is the inductive step, assuming the motive for(j : Fin n).succ
and demonstrating it for the predecessorj.castSucc
.
Fin.induction
is the non-reverse induction principle.
Equations
Instances For
Proves a statement by cases on the underlying Nat
value in a Fin (n + 1)
, checking whether the
value is the greatest representable or a predecessor of some other.
The two cases are:
The corresponding induction principle is Fin.reverseInduction
.
Equations
Instances For
A case analysis operator for i : Fin (m + n)
that separately handles the cases where i < m
and
where m ≤ i < m + n
.
The first case, where i < m
, is handled by left
. In this case, i
can be represented as
Fin.castAdd n (j : Fin m)
.
The second case, where m ≤ i < m + n
, is handled by right
. In this case, i
can be represented
as Fin.natAdd m (j : Fin n)
.