Library Stdlib.Vectors.FinFun
An example of finite type : Fin.t
#[local] Set Warnings "-stdlib-vector".
Set Implicit Arguments.
From Stdlib Require Import PeanoNat Compare_dec List Finite Fin Permutation.
Export Finite.
Lemma Fin_Finite n : Finite (Fin.t n).
Set Implicit Arguments.
From Stdlib Require Import PeanoNat Compare_dec List Finite Fin Permutation.
Export Finite.
Lemma Fin_Finite n : Finite (Fin.t n).
Instead of working on a finite subset of nat, another
solution is to use restricted nat->nat functions, and
to consider them only below a certain bound n.
Definition bFun n (f:nat->nat) := forall x, x < n -> f x < n.
Definition bInjective n (f:nat->nat) :=
forall x y, x < n -> y < n -> f x = f y -> x = y.
Definition bSurjective n (f:nat->nat) :=
forall y, y < n -> exists x, x < n /\ f x = y.
We show that this is equivalent to the use of Fin.t n.
Module Fin2Restrict.
Notation n2f := Fin.of_nat_lt.
Definition f2n {n} (x:Fin.t n) := proj1_sig (Fin.to_nat x).
Definition f2n_ok n (x:Fin.t n) : f2n x < n := proj2_sig (Fin.to_nat x).
Definition n2f_f2n : forall n x, n2f (f2n_ok x) = x := @Fin.of_nat_to_nat_inv.
Definition f2n_n2f x n h : f2n (n2f h) = x := f_equal (@proj1_sig _ _) (@Fin.to_nat_of_nat x n h).
Definition n2f_ext : forall x n h h', n2f h = n2f h' := @Fin.of_nat_ext.
Definition f2n_inj : forall n x y, f2n x = f2n y -> x = y := @Fin.to_nat_inj.
Definition extend n (f:Fin.t n -> Fin.t n) : (nat->nat) :=
fun x =>
match le_lt_dec n x with
| left _ => 0
| right h => f2n (f (n2f h))
end.
Definition restrict n (f:nat->nat)(hf : bFun n f) : (Fin.t n -> Fin.t n) :=
fun x => let (x',h) := Fin.to_nat x in n2f (hf _ h).
Ltac break_dec H :=
let H' := fresh "H" in
destruct le_lt_dec as [H'|H'];
[elim (proj1 (Nat.le_ngt _ _) H' H)
|try rewrite (n2f_ext H' H) in *; try clear H'].
Lemma extend_ok n f : bFun n (@extend n f).
Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x).
Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h).
Lemma restrict_f2n n f hf (x:Fin.t n) :
f2n (@restrict n f hf x) = f (f2n x).
Lemma restrict_n2f n f hf x (h:x<n) :
@restrict n f hf (n2f h) = n2f (hf _ h).
Lemma extend_surjective n f :
bSurjective n (@extend n f) <-> Surjective f.
Lemma extend_injective n f :
bInjective n (@extend n f) <-> Injective f.
Lemma restrict_surjective n f h :
Surjective (@restrict n f h) <-> bSurjective n f.
Lemma restrict_injective n f h :
Injective (@restrict n f h) <-> bInjective n f.
End Fin2Restrict.
Import Fin2Restrict.
We can now use Proof via the equivalence ...
Lemma bInjective_bSurjective n (f:nat->nat) :
bFun n f -> (bInjective n f <-> bSurjective n f).
Lemma bSurjective_bBijective n (f:nat->nat) :
bFun n f -> bSurjective n f ->
exists g, bFun n g /\ forall x, x < n -> g (f x) = x /\ f (g x) = x.
Section Permutation_alt.
Variable A:Type.
Implicit Type a : A.
Implicit Type l : list A.
Lemma Permutation_nth_error_bis l l' :
Permutation l l' <->
exists f:nat->nat,
Injective f /\
bFun (length l) f /\
(forall n, nth_error l' n = nth_error l (f n)).
Lemma Permutation_nth l l' d :
Permutation l l' <->
(let n := length l in
length l' = n /\
exists f:nat->nat,
bFun n f /\
bInjective n f /\
(forall x, x < n -> nth x l' d = nth (f x) l d)).
End Permutation_alt.