The finite type with n
elements #
Fin n
is the type whose elements are natural numbers smaller than n
.
This file expands on the development in the core library.
Main definitions #
Induction principles #
finZeroElim
: Elimination principle for the empty setFin 0
, generalizesFin.elim0
.Fin.succRec
: DefineC n i
by induction oni : Fin n
interpreted as(0 : Fin (n - i)).succ.succ…
. This function has two arguments:H0 n
defines0
-th elementC (n+1) 0
of an(n+1)
-tuple, andHs n i
defines(i+1)
-st element of(n+1)
-tuple based onn
,i
, andi
-th element ofn
-tuple.Fin.succRecOn
: same asFin.succRec
buti : Fin n
is the first argument;Fin.induction
: DefineC i
by induction oni : Fin (n + 1)
, separating into theNat
-like base cases ofC 0
andC (i.succ)
.Fin.inductionOn
: same asFin.induction
but withi : Fin (n + 1)
as the first argument.Fin.cases
: definef : Π i : Fin n.succ, C i
by separately handling the casesi = 0
andi = Fin.succ j
,j : Fin n
, defined usingFin.induction
.Fin.reverseInduction
: reverse induction oni : Fin (n + 1)
; givenC (Fin.last n)
and∀ i : Fin n, C (Fin.succ i) → C (Fin.castSucc i)
, constructs all valuesC i
by going down;Fin.lastCases
: definef : Π i, Fin (n + 1), C i
by separately handling the casesi = Fin.last n
andi = Fin.castSucc j
, a special case ofFin.reverseInduction
;Fin.addCases
: define a function onFin (m + n)
by separately handling the casesFin.castAdd n i
andFin.natAdd m i
;Fin.succAbove_cases
: giveni : Fin (n + 1)
, define a function onFin (n + 1)
by separately handling the casesj = i
andj = Fin.succAbove i k
, same asFin.insertNth
but marked as eliminator and works forSort*
. -- Porting note: this is in another file
Order embeddings and an order isomorphism #
Fin.orderIsoSubtype
: coercion to{ i // i < n }
as anOrderIso
;Fin.valEmbedding
: coercion to natural numbers as anEmbedding
;Fin.valOrderEmbedding
: coercion to natural numbers as anOrderEmbedding
;Fin.succEmbedding
:Fin.succ
as anOrderEmbedding
;Fin.castLe h
: embedFin n
intoFin m
,h : n ≤ m
;Fin.cast
: order isomorphism betweenFin n
andFin m
provided thatn = m
, see alsoEquiv.finCongr
;Fin.castAdd m
: embedFin n
intoFin (n+m)
;Fin.castSucc
: embedFin n
intoFin (n+1)
;Fin.succAbove p
: embedFin n
intoFin (n + 1)
with a hole aroundp
;Fin.addNat m i
: addm
oni
on the right, generalizesFin.succ
;Fin.natAdd n i
addsn
oni
on the left;
Other casts #
Fin.ofNat'
: given a positive numbern
(deduced from[NeZero n]
),Fin.ofNat' i
isi % n
interpreted as an element ofFin n
;Fin.castLt i h
: embedi
into aFin
whereh
proves it belongs into;Fin.predAbove (p : Fin n) i
: embedi : Fin (n+1)
intoFin n
by subtracting one ifp < i
;Fin.castPred
: embedFin (n + 2)
intoFin (n + 1)
by mappingFin.last (n + 1)
toFin.last n
;Fin.subNat i h
: subtractm
fromi ≥ m
, generalizesFin.pred
;Fin.clamp n m
:min n m
as an element ofFin (m + 1)
;Fin.divNat i
: dividesi : Fin (m * n)
byn
;Fin.modNat i
: takes the mod ofi : Fin (m * n)
byn
;
Misc definitions #
Elimination principle for the empty set Fin 0
, dependent version.
Equations
- finZeroElim x = Fin.elim0 x
A non-dependent variant of elim0
.
Equations
- Fin.elim0' x = Fin.elim0 x
coercions and constructions #
order #
Equations
- One or more equations did not get rendered due to their size.
Equations
- Fin.instPartialOrderFin = inferInstance
The inclusion map Fin n → ℕ
is an embedding.
Equations
- Fin.valEmbedding = { toFun := Fin.val, inj' := (_ : Function.Injective Fin.val) }
The inclusion map Fin n → ℕ
is an order embedding.
The ordering on Fin n
is a well order.
Use the ordering on Fin n
for checking recursive definitions.
For example, the following definition is not accepted by the termination checker,
unless we declare the WellFoundedRelation
instance:
def factorial {n : ℕ} : Fin n → ℕ
| ⟨0, _⟩ := 1
| ⟨i + 1, hi⟩ := (i + 1) * factorial ⟨i, i.lt_succ_self.trans hi⟩
Given a positive n
, Fin.ofNat' i
is i % n
as an element of Fin n
.
Equations
- Fin.ofNat'' i = { val := i % n, isLt := (_ : i % n < n) }
Equations
- Fin.instZeroFin = { zero := Fin.ofNat'' 0 }
Equations
- Fin.instOneFin = { one := Fin.ofNat'' 1 }
Equations
- Fin.instBoundedOrderFinHAddNatInstHAddInstAddNatOfNatInstLEFin = BoundedOrder.mk
Two strictly monotone functions from Fin n
are equal provided that their ranges
are equal.
addition, numerals, and coercion from Nat #
Equations
Equations
- Fin.instAddCommSemigroupFin n = AddCommSemigroup.mk (_ : ∀ (a a_1 : Fin n), a + a_1 = a_1 + a)
Equations
- Fin.addCommMonoid n = AddCommMonoid.mk (_ : ∀ (a a_1 : Fin n), a + a_1 = a_1 + a)
Equations
- Fin.instAddMonoidWithOneFin n = let src := inferInstanceAs (AddCommMonoid (Fin n)); AddMonoidWithOne.mk
succ and casts into larger Fin types #
Fin.succ
as an OrderEmbedding
Equations
- Fin.succEmbedding n = OrderEmbedding.ofStrictMono Fin.succ (_ : ∀ (x x_1 : Fin n), x < x_1 → Nat.succ ↑x < Nat.succ ↑x_1)
Version of succ_zero_eq_one
to be used by dsimp
Version of succ_one_eq_two
to be used by dsimp
castLe h i
embeds i
into a larger Fin
type.
Equations
- Fin.castLe h = OrderEmbedding.ofStrictMono (fun a => Fin.castLt a (_ : ↑a < m)) (_ : ∀ (x x_1 : Fin n), x < x_1 → x < x_1)
While in many cases Fin.cast
is better than Equiv.cast
/cast
, sometimes we want to apply
a generic theorem about cast
.
castAdd m i
embeds i : Fin n
in Fin (n+m)
. See also Fin.natAdd
and Fin.addNat
.
Equations
- Fin.castAdd m = Fin.castLe (_ : n ≤ n + m)
For rewriting in the reverse direction, see Fin.cast_castAdd_left
.
The cast of the successor is the succesor of the cast. See Fin.succ_cast_eq
for rewriting in
the reverse direction.
For rewriting in the reverse direction, see Fin.cast_addNat_left
.
For rewriting in the reverse direction, see Fin.cast_natAdd_right
.
pred #
recursion and induction principles #
Define C n i
by induction on i : Fin n
interpreted as (0 : Fin (n - i)).succ.succ…
.
This function has two arguments: H0 n
defines 0
-th element C (n+1) 0
of an (n+1)
-tuple,
and Hs n i
defines (i+1)
-st element of (n+1)
-tuple based on n
, i
, and i
-th element
of n
-tuple.
Equations
- Fin.succRec H0 Hs i = Fin.elim0 i
- Fin.succRec H0 Hs { val := 0, isLt := isLt } = Eq.mpr (_ : C (Nat.succ n) { val := 0, isLt := isLt } = C (Nat.succ n) 0) (H0 n)
- Fin.succRec H0 Hs { val := Nat.succ i, isLt := h } = Hs n { val := i, isLt := (_ : i < n) } (Fin.succRec H0 Hs { val := i, isLt := (_ : i < n) })
Define C n i
by induction on i : Fin n
interpreted as (0 : Fin (n - i)).succ.succ…
.
This function has two arguments: H0 n
defines 0
-th element C (n+1) 0
of an (n+1)
-tuple,
and Hs n i
defines (i+1)
-st element of (n+1)
-tuple based on n
, i
, and i
-th element
of n
-tuple.
A version of Fin.succRec
taking i : Fin n
as the first argument.
Equations
- Fin.succRecOn i H0 Hs = Fin.succRec H0 Hs i
Define C i
by induction on i : Fin (n + 1)
via induction on the underlying Nat
value.
This function has two arguments: h0
handles the base case on C 0
,
and hs
defines the inductive step using C i.castSucc
.
Equations
- One or more equations did not get rendered due to their size.
Define C i
by induction on i : Fin (n + 1)
via induction on the underlying Nat
value.
This function has two arguments: h0
handles the base case on C 0
,
and hs
defines the inductive step using C i.castSucc
.
A version of Fin.induction
taking i : Fin (n + 1)
as the first argument.
Equations
- Fin.inductionOn i h0 hs = Fin.induction h0 hs i
Define C i
by reverse induction on i : Fin (n + 1)
via induction on the underlying Nat
value.
This function has two arguments: hlast
handles the base case on C (Fin.last n)
,
and hs
defines the inductive step using C i.succ
, inducting downwards.
Equations
- One or more equations did not get rendered due to their size.
Define f : Π i : Fin n.succ, C i
by separately handling the cases i = Fin.last n
and
i = j.castSucc
, j : Fin n
.
Equations
- Fin.lastCases hlast hcast i = Fin.reverseInduction hlast (fun i x => hcast i) i
Define f : Π i : Fin (m + n), C i
by separately handling the cases i = castAdd n i
,
j : Fin m
and i = natAdd m j
, j : Fin n
.
Equations
- One or more equations did not get rendered due to their size.
Abelian group structure on Fin n
.
Equations
- Fin.addCommGroup n = let src := Fin.addCommMonoid n; let src_1 := Fin.neg n; AddCommGroup.mk (_ : ∀ (a b : Fin n), a + b = b + a)
Given a fixed pivot x : Fin (n + 1)
, x.succAbove
is injective
Given a fixed pivot x : Fin (n + 1)
, x.succAbove
is injective
succAbove
is injective at the pivot
succAbove
is injective at the pivot
By moving succ
to the outside of this expression, we create opportunities for further
simplification using succAbove_zero
or succ_succAbove_zero
.
Sending Fin (n+1)
to Fin n
by subtracting one from anything above p
then back to Fin (n+1)
with a gap around p
is the identity away from p
.
Sending Fin n
into Fin (n + 1)
with a gap at p
then back to Fin n
by subtracting one from anything above p
is the identity.
succ
commutes with predAbove
.