Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Functions on finite domains

Main result : for functions f:A→A with finite A, f injective <-> f bijective <-> f surjective.

Require Import List Compare_dec EqNat Decidable ListDec. Require Fin.
Set Implicit Arguments.

General definitions

Definition Injective {A B} (f : A->B) :=
 forall x y, f x = f y -> x = y.

Definition Surjective {A B} (f : A->B) :=
 forall y, exists x, f x = y.

Definition Bijective {A B} (f : A->B) :=
 exists g:B->A, (forall x, g (f x) = x) /\ (forall y, f (g y) = y).

Finiteness is defined here via exhaustive list enumeration

Definition Full {A:Type} (l:list A) := forall a:A, In a l.
Definition Finite (A:Type) := exists (l:list A), Full l.

In many following proofs, it will be convenient to have list enumerations without duplicates. As soon as we have decidability of equality (in Prop), this is equivalent to the previous notion.

Definition Listing {A:Type} (l:list A) := NoDup l /\ Full l.
Definition Finite' (A:Type) := exists (l:list A), Listing l.

Lemma Finite_alt A (d:decidable_eq A) : Finite A <-> Finite' A.A:Type
d:decidable_eq A
Finite A <-> Finite' A
Proof.A:Type
d:decidable_eq A
Finite A <-> Finite' A
 split.A:Type
d:decidable_eq A
Finite A -> Finite' A
A:Type
d:decidable_eq A
Finite' A -> Finite A
 -A:Type
d:decidable_eq A
Finite A -> Finite' A intros (l,F).A:Type
d:decidable_eq A
l:list A
F:Full l
Finite' A destruct (uniquify d l) as (l' & N & I).A:Type
d:decidable_eq A
l:list A
F:Full l
l':list A
N:NoDup l'
I:incl l l'
Finite' A
   exists l'.A:Type
d:decidable_eq A
l:list A
F:Full l
l':list A
N:NoDup l'
I:incl l l'
Listing l' split; trivial.A:Type
d:decidable_eq A
l:list A
F:Full l
l':list A
N:NoDup l'
I:incl l l'
Full l'
   intros x.A:Type
d:decidable_eq A
l:list A
F:Full l
l':list A
N:NoDup l'
I:incl l l'
x:A
In x l' apply I, F.
 -A:Type
d:decidable_eq A
Finite' A -> Finite A intros (l & _ & F).A:Type
d:decidable_eq A
l:list A
F:Full l
Finite A now exists l.
Qed.

Injections characterized in term of lists

Lemma Injective_map_NoDup A B (f:A->B) (l:list A) :
 Injective f -> NoDup l -> NoDup (map f l).A, B:Type
f:A -> B
l:list A
Injective f -> NoDup l -> NoDup (map f l)
Proof.A, B:Type
f:A -> B
l:list A
Injective f -> NoDup l -> NoDup (map f l)
 intros Ij.A, B:Type
f:A -> B
l:list A
Ij:Injective f
NoDup l -> NoDup (map f l) induction 1 as [|x l X N IH]; simpl; constructor; trivial.A, B:Type
f:A -> B
Ij:Injective f
x:A
l:list A
X:~ In x l
N:NoDup l
IH:NoDup (map f l)
~ In (f x) (map f l)
 rewrite in_map_iff.A, B:Type
f:A -> B
Ij:Injective f
x:A
l:list A
X:~ In x l
N:NoDup l
IH:NoDup (map f l)
~ (exists x0 : A, f x0 = f x /\ In x0 l) intros (y & E & Y).A, B:Type
f:A -> B
Ij:Injective f
x:A
l:list A
X:~ In x l
N:NoDup l
IH:NoDup (map f l)
y:A
E:f y = f x
Y:In y l
False apply Ij in E.A, B:Type
f:A -> B
Ij:Injective f
x:A
l:list A
X:~ In x l
N:NoDup l
IH:NoDup (map f l)
y:A
E:y = x
Y:In y l
False now subst.
Qed.

Lemma Injective_list_carac A B (d:decidable_eq A)(f:A->B) :
  Injective f <-> (forall l, NoDup l -> NoDup (map f l)).A, B:Type
d:decidable_eq A
f:A -> B
Injective f <->
(forall l : list A, NoDup l -> NoDup (map f l))
Proof.A, B:Type
d:decidable_eq A
f:A -> B
Injective f <->
(forall l : list A, NoDup l -> NoDup (map f l))
 split.A, B:Type
d:decidable_eq A
f:A -> B
Injective f ->
forall l : list A, NoDup l -> NoDup (map f l)
A, B:Type
d:decidable_eq A
f:A -> B
(forall l : list A, NoDup l -> NoDup (map f l)) ->
Injective f
 -A, B:Type
d:decidable_eq A
f:A -> B
Injective f ->
forall l : list A, NoDup l -> NoDup (map f l) intros.A, B:Type
d:decidable_eq A
f:A -> B
H:Injective f
l:list A
H0:NoDup l
NoDup (map f l) now apply Injective_map_NoDup.
 -A, B:Type
d:decidable_eq A
f:A -> B
(forall l : list A, NoDup l -> NoDup (map f l)) ->
Injective f intros H x y E.A, B:Type
d:decidable_eq A
f:A -> B
H:forall l : list A, NoDup l -> NoDup (map f l)
x, y:A
E:f x = f y
x = y
   destruct (d x y); trivial.A, B:Type
d:decidable_eq A
f:A -> B
H:forall l : list A, NoDup l -> NoDup (map f l)
x, y:A
E:f x = f y
H0:x <> y
x = y
   assert (N : NoDup (x::y::nil)).A, B:Type
d:decidable_eq A
f:A -> B
H:forall l : list A, NoDup l -> NoDup (map f l)
x, y:A
E:f x = f y
H0:x <> y
NoDup (x :: y :: nil)
A, B:Type
d:decidable_eq A
f:A -> B
H:forall l : list A, NoDup l -> NoDup (map f l)
x, y:A
E:f x = f y
H0:x <> y
N:NoDup (x :: y :: nil)
x = y
   {A, B:Type
d:decidable_eq A
f:A -> B
H:forall l : list A, NoDup l -> NoDup (map f l)
x, y:A
E:f x = f y
H0:x <> y
NoDup (x :: y :: nil) repeat constructor; simpl; intuition. }A, B:Type
d:decidable_eq A
f:A -> B
H:forall l : list A, NoDup l -> NoDup (map f l)
x, y:A
E:f x = f y
H0:x <> y
N:NoDup (x :: y :: nil)
x = y
   specialize (H _ N).A, B:Type
d:decidable_eq A
f:A -> B
x, y:A
H:NoDup (map f (x :: y :: nil))
E:f x = f y
H0:x <> y
N:NoDup (x :: y :: nil)
x = y simpl in H.A, B:Type
d:decidable_eq A
f:A -> B
x, y:A
H:NoDup (f x :: f y :: nil)
E:f x = f y
H0:x <> y
N:NoDup (x :: y :: nil)
x = y rewrite E in H.A, B:Type
d:decidable_eq A
f:A -> B
x, y:A
H:NoDup (f y :: f y :: nil)
E:f x = f y
H0:x <> y
N:NoDup (x :: y :: nil)
x = y
   inversion_clear H; simpl in *; intuition.
Qed.

Lemma Injective_carac A B (l:list A) : Listing l ->
   forall (f:A->B), Injective f <-> NoDup (map f l).A, B:Type
l:list A
Listing l ->
forall f : A -> B, Injective f <-> NoDup (map f l)
Proof.A, B:Type
l:list A
Listing l ->
forall f : A -> B, Injective f <-> NoDup (map f l)
 intros L f.A, B:Type
l:list A
L:Listing l
f:A -> B
Injective f <-> NoDup (map f l) split.A, B:Type
l:list A
L:Listing l
f:A -> B
Injective f -> NoDup (map f l)
A, B:Type
l:list A
L:Listing l
f:A -> B
NoDup (map f l) -> Injective f
 -A, B:Type
l:list A
L:Listing l
f:A -> B
Injective f -> NoDup (map f l) intros Ij.A, B:Type
l:list A
L:Listing l
f:A -> B
Ij:Injective f
NoDup (map f l) apply Injective_map_NoDup; trivial.A, B:Type
l:list A
L:Listing l
f:A -> B
Ij:Injective f
NoDup l apply L.
 -A, B:Type
l:list A
L:Listing l
f:A -> B
NoDup (map f l) -> Injective f intros N x y E.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
x = y
   assert (X : In x l) by apply L.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
X:In x l
x = y
   assert (Y : In y l) by apply L.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
X:In x l
Y:In y l
x = y
   apply In_nth_error in X.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
X:exists n : nat, nth_error l n = Some x
Y:In y l
x = y destruct X as (i,X).A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
Y:In y l
x = y
   apply In_nth_error in Y.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
Y:exists n : nat, nth_error l n = Some y
x = y destruct Y as (j,Y).A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
x = y
   assert (X' := map_nth_error f _ _ X).A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
x = y
   assert (Y' := map_nth_error f _ _ Y).A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
x = y
   assert (i = j).A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
i = j
A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
H:i = j
x = y
   {A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
i = j rewrite NoDup_nth_error in N.A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
i = j apply N.A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
i < length (map f l)
A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
nth_error (map f l) i = nth_error (map f l) j
     -A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
i < length (map f l) rewrite <- nth_error_Some.A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
nth_error (map f l) i <> None now rewrite X'.
     -A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
nth_error (map f l) i = nth_error (map f l) j rewrite X', Y'.A, B:Type
l:list A
L:Listing l
f:A -> B
N:forall i0 j0 : nat,
i0 < length (map f l) ->
nth_error (map f l) i0 = nth_error (map f l) j0 ->
i0 = j0
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
Some (f x) = Some (f y) now f_equal. }A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
j:nat
Y:nth_error l j = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) j = Some (f y)
H:i = j
x = y
   subst j.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:nth_error l i = Some x
Y:nth_error l i = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) i = Some (f y)
x = y rewrite Y in X.A, B:Type
l:list A
L:Listing l
f:A -> B
N:NoDup (map f l)
x, y:A
E:f x = f y
i:nat
X:Some y = Some x
Y:nth_error l i = Some y
X':nth_error (map f l) i = Some (f x)
Y':nth_error (map f l) i = Some (f y)
x = y now injection X.
Qed.

Surjection characterized in term of lists

Lemma Surjective_list_carac A B (f:A->B):
  Surjective f <-> (forall lB, exists lA, incl lB (map f lA)).A, B:Type
f:A -> B
Surjective f <->
(forall lB : list B,
 exists lA : list A, incl lB (map f lA))
Proof.A, B:Type
f:A -> B
Surjective f <->
(forall lB : list B,
 exists lA : list A, incl lB (map f lA))
 split.A, B:Type
f:A -> B
Surjective f ->
forall lB : list B,
exists lA : list A, incl lB (map f lA)
A, B:Type
f:A -> B
(forall lB : list B,
 exists lA : list A, incl lB (map f lA)) ->
Surjective f
 -A, B:Type
f:A -> B
Surjective f ->
forall lB : list B,
exists lA : list A, incl lB (map f lA) intros Su.A, B:Type
f:A -> B
Su:Surjective f
forall lB : list B,
exists lA : list A, incl lB (map f lA)
   induction lB as [|b lB IH].A, B:Type
f:A -> B
Su:Surjective f
exists lA : list A, incl nil (map f lA)
A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
IH:exists lA : list A, incl lB (map f lA)
exists lA : list A, incl (b :: lB) (map f lA)
   +A, B:Type
f:A -> B
Su:Surjective f
exists lA : list A, incl nil (map f lA) now exists nil.
   +A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
IH:exists lA : list A, incl lB (map f lA)
exists lA : list A, incl (b :: lB) (map f lA) destruct (Su b) as (a,E).A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
IH:exists lA : list A, incl lB (map f lA)
a:A
E:f a = b
exists lA : list A, incl (b :: lB) (map f lA)
     destruct IH as (lA,IC).A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
lA:list A
IC:incl lB (map f lA)
a:A
E:f a = b
exists lA0 : list A, incl (b :: lB) (map f lA0)
     exists (a::lA).A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
lA:list A
IC:incl lB (map f lA)
a:A
E:f a = b
incl (b :: lB) (map f (a :: lA)) simpl.A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
lA:list A
IC:incl lB (map f lA)
a:A
E:f a = b
incl (b :: lB) (f a :: map f lA) rewrite E.A, B:Type
f:A -> B
Su:Surjective f
b:B
lB:list B
lA:list A
IC:incl lB (map f lA)
a:A
E:f a = b
incl (b :: lB) (b :: map f lA)
     intros x [X|X]; simpl; intuition.
 -A, B:Type
f:A -> B
(forall lB : list B,
 exists lA : list A, incl lB (map f lA)) ->
Surjective f intros H y.A, B:Type
f:A -> B
H:forall lB : list B,
exists lA : list A, incl lB (map f lA)
y:B
exists x : A, f x = y
   destruct (H (y::nil)) as (lA,IC).A, B:Type
f:A -> B
H:forall lB : list B,
exists lA0 : list A, incl lB (map f lA0)
y:B
lA:list A
IC:incl (y :: nil) (map f lA)
exists x : A, f x = y
   assert (IN : In y (map f lA)) by (apply (IC y); now left).A, B:Type
f:A -> B
H:forall lB : list B,
exists lA0 : list A, incl lB (map f lA0)
y:B
lA:list A
IC:incl (y :: nil) (map f lA)
IN:In y (map f lA)
exists x : A, f x = y
   rewrite in_map_iff in IN.A, B:Type
f:A -> B
H:forall lB : list B,
exists lA0 : list A, incl lB (map f lA0)
y:B
lA:list A
IC:incl (y :: nil) (map f lA)
IN:exists x : A, f x = y /\ In x lA
exists x : A, f x = y destruct IN as (x & E & _).A, B:Type
f:A -> B
H:forall lB : list B,
exists lA0 : list A, incl lB (map f lA0)
y:B
lA:list A
IC:incl (y :: nil) (map f lA)
x:A
E:f x = y
exists x0 : A, f x0 = y
   now exists x.
Qed.

Lemma Surjective_carac A B : Finite B -> decidable_eq B ->
  forall f:A->B, Surjective f <-> (exists lA, Listing (map f lA)).A, B:Type
Finite B ->
decidable_eq B ->
forall f : A -> B,
Surjective f <->
(exists lA : list A, Listing (map f lA))
Proof.A, B:Type
Finite B ->
decidable_eq B ->
forall f : A -> B,
Surjective f <->
(exists lA : list A, Listing (map f lA))
 intros (lB,FB) d.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
forall f : A -> B,
Surjective f <->
(exists lA : list A, Listing (map f lA)) split.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Surjective f -> exists lA : list A, Listing (map f lA)
A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
(exists lA : list A, Listing (map f lA)) ->
Surjective f
 -A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Surjective f -> exists lA : list A, Listing (map f lA) rewrite Surjective_list_carac.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
(forall lB0 : list B,
 exists lA : list A, incl lB0 (map f lA)) ->
exists lA : list A, Listing (map f lA)
   intros Su.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Su:forall lB0 : list B,
exists lA : list A, incl lB0 (map f lA)
exists lA : list A, Listing (map f lA) destruct (Su lB) as (lA,IC).A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Su:forall lB0 : list B,
exists lA0 : list A, incl lB0 (map f lA0)
lA:list A
IC:incl lB (map f lA)
exists lA0 : list A, Listing (map f lA0)
   destruct (uniquify_map d f lA) as (lA' & N & IC').A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Su:forall lB0 : list B,
exists lA0 : list A, incl lB0 (map f lA0)
lA:list A
IC:incl lB (map f lA)
lA':list A
N:NoDup (map f lA')
IC':incl (map f lA) (map f lA')
exists lA0 : list A, Listing (map f lA0)
   exists lA'.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Su:forall lB0 : list B,
exists lA0 : list A, incl lB0 (map f lA0)
lA:list A
IC:incl lB (map f lA)
lA':list A
N:NoDup (map f lA')
IC':incl (map f lA) (map f lA')
Listing (map f lA') split; trivial.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Su:forall lB0 : list B,
exists lA0 : list A, incl lB0 (map f lA0)
lA:list A
IC:incl lB (map f lA)
lA':list A
N:NoDup (map f lA')
IC':incl (map f lA) (map f lA')
Full (map f lA')
   intro x.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
Su:forall lB0 : list B,
exists lA0 : list A, incl lB0 (map f lA0)
lA:list A
IC:incl lB (map f lA)
lA':list A
N:NoDup (map f lA')
IC':incl (map f lA) (map f lA')
x:B
In x (map f lA') apply IC', IC, FB.
 -A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
(exists lA : list A, Listing (map f lA)) ->
Surjective f intros (lA & N & FA) y.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
lA:list A
N:NoDup (map f lA)
FA:Full (map f lA)
y:B
exists x : A, f x = y
   generalize (FA y).A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
lA:list A
N:NoDup (map f lA)
FA:Full (map f lA)
y:B
In y (map f lA) -> exists x : A, f x = y rewrite in_map_iff.A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
lA:list A
N:NoDup (map f lA)
FA:Full (map f lA)
y:B
(exists x : A, f x = y /\ In x lA) ->
exists x : A, f x = y intros (x & E & _).A, B:Type
lB:list B
FB:Full lB
d:decidable_eq B
f:A -> B
lA:list A
N:NoDup (map f lA)
FA:Full (map f lA)
y:B
x:A
E:f x = y
exists x0 : A, f x0 = y
   now exists x.
Qed.

Main result :

Lemma Endo_Injective_Surjective :
 forall A, Finite A -> decidable_eq A ->
  forall f:A->A, Injective f <-> Surjective f.forall A : Type,
Finite A ->
decidable_eq A ->
forall f : A -> A, Injective f <-> Surjective f
Proof.forall A : Type,
Finite A ->
decidable_eq A ->
forall f : A -> A, Injective f <-> Surjective f
 intros A F d f.A:Type
F:Finite A
d:decidable_eq A
f:A -> A
Injective f <-> Surjective f rewrite (Surjective_carac F d).A:Type
F:Finite A
d:decidable_eq A
f:A -> A
Injective f <->
(exists lA : list A, Listing (map f lA)) split.A:Type
F:Finite A
d:decidable_eq A
f:A -> A
Injective f -> exists lA : list A, Listing (map f lA)
A:Type
F:Finite A
d:decidable_eq A
f:A -> A
(exists lA : list A, Listing (map f lA)) ->
Injective f
 -A:Type
F:Finite A
d:decidable_eq A
f:A -> A
Injective f -> exists lA : list A, Listing (map f lA) apply (Finite_alt d) in F.A:Type
F:Finite' A
d:decidable_eq A
f:A -> A
Injective f -> exists lA : list A, Listing (map f lA) destruct F as (l,L).A:Type
l:list A
L:Listing l
d:decidable_eq A
f:A -> A
Injective f -> exists lA : list A, Listing (map f lA)
   rewrite (Injective_carac L); intros.A:Type
l:list A
L:Listing l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
exists lA : list A, Listing (map f lA)
   exists l; split; trivial.A:Type
l:list A
L:Listing l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
Full (map f l)
   destruct L as (N,F).A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
Full (map f l)
   assert (I : incl l (map f l)).A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
incl l (map f l)
A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
I:incl l (map f l)
Full (map f l)
   {A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
incl l (map f l) apply NoDup_length_incl; trivial.A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
length l <= length (map f l)
A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
incl (map f l) l
     -A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
length l <= length (map f l) now rewrite map_length.
     -A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
incl (map f l) l intros x _.A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
x:A
In x l apply F. }A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
I:incl l (map f l)
Full (map f l)
   intros x.A:Type
l:list A
N:NoDup l
F:Full l
d:decidable_eq A
f:A -> A
H:NoDup (map f l)
I:incl l (map f l)
x:A
In x (map f l) apply I, F.
 -A:Type
F:Finite A
d:decidable_eq A
f:A -> A
(exists lA : list A, Listing (map f lA)) ->
Injective f clear F d.A:Type
f:A -> A
(exists lA : list A, Listing (map f lA)) ->
Injective f intros (l,L).A:Type
f:A -> A
l:list A
L:Listing (map f l)
Injective f
   assert (N : NoDup l).A:Type
f:A -> A
l:list A
L:Listing (map f l)
NoDup l
A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
Injective f {A:Type
f:A -> A
l:list A
L:Listing (map f l)
NoDup l apply (NoDup_map_inv f), L. }A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
Injective f
   assert (I : incl (map f l) l).A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
incl (map f l) l
A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
Injective f
   {A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
incl (map f l) l apply NoDup_length_incl; trivial.A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
length (map f l) <= length l
A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
incl l (map f l)
     -A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
length (map f l) <= length l now rewrite map_length.
     -A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
incl l (map f l) intros x _.A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
x:A
In x (map f l) apply L. }A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
Injective f
   assert (L' : Listing l).A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
Listing l
A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
L':Listing l
Injective f
   {A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
Listing l split; trivial.A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
Full l
     intro x.A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
x:A
In x l apply I, L. }A:Type
f:A -> A
l:list A
L:Listing (map f l)
N:NoDup l
I:incl (map f l) l
L':Listing l
Injective f
   apply (Injective_carac L'), L.
Qed.

An injective and surjective function is bijective. We need here stronger hypothesis : decidability of equality in Type.

Definition EqDec (A:Type) := forall x y:A, {x=y}+{x<>y}.

First, we show that a surjective f has an inverse function g such that f.g = id.

(* NB: instead of (Finite A), we could ask for (RecEnum A) with:
Definition RecEnum A := exists h:nat->A, surjective h.
*)

Lemma Finite_Empty_or_not A :
  Finite A -> (A->False) \/ exists a:A,True.A:Type
Finite A -> (A -> False) \/ (exists _ : A, True)
Proof.A:Type
Finite A -> (A -> False) \/ (exists _ : A, True)
 intros (l,F).A:Type
l:list A
F:Full l
(A -> False) \/ (exists _ : A, True)
 destruct l.A:Type
F:Full nil
(A -> False) \/ (exists _ : A, True)
A:Type
a:A
l:list A
F:Full (a :: l)
(A -> False) \/ (exists _ : A, True)
 -A:Type
F:Full nil
(A -> False) \/ (exists _ : A, True) left; exact F.
 -A:Type
a:A
l:list A
F:Full (a :: l)
(A -> False) \/ (exists _ : A, True) right; now exists a.
Qed.

Lemma Surjective_inverse :
  forall A B, Finite A -> EqDec B ->
   forall f:A->B, Surjective f ->
    exists g:B->A, forall x, f (g x) = x.forall A B : Type,
Finite A ->
EqDec B ->
forall f : A -> B,
Surjective f ->
exists g : B -> A, forall x : B, f (g x) = x
Proof.forall A B : Type,
Finite A ->
EqDec B ->
forall f : A -> B,
Surjective f ->
exists g : B -> A, forall x : B, f (g x) = x
 intros A B F d f Su.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
exists g : B -> A, forall x : B, f (g x) = x
 destruct (Finite_Empty_or_not F) as [noA | (a,_)].A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
exists g : B -> A, forall x : B, f (g x) = x
A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
a:A
exists g : B -> A, forall x : B, f (g x) = x
 - (* A is empty : g is obtained via False_rect *)A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
exists g : B -> A, forall x : B, f (g x) = x
   assert (noB : B -> False).A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
B -> False
A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
noB:B -> False
exists g : B -> A, forall x : B, f (g x) = x {A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
B -> False intros y.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
y:B
False now destruct (Su y). }A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
noB:B -> False
exists g : B -> A, forall x : B, f (g x) = x
   exists (fun y => False_rect _ (noB y)).A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
noB:B -> False
forall x : B, f (False_rect A (noB x)) = x
   intro y.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
noA:A -> False
noB:B -> False
y:B
f (False_rect A (noB y)) = y destruct (noB y).
 - (* A is inhabited by a : we use it in Option.get *)A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Su:Surjective f
a:A
exists g : B -> A, forall x : B, f (g x) = x
   destruct F as (l,F).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
exists g : B -> A, forall x : B, f (g x) = x
   set (h := fun x k => if d (f k) x then true else false).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x : B) (k : A) =>
if d (f k) x then true else false:B -> A -> bool
exists g : B -> A, forall x : B, f (g x) = x
   set (get := fun o => match o with Some y => y | None => a end).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x : B) (k : A) =>
if d (f k) x then true else false:B -> A -> bool
get:=fun o : option A =>
match o with
| Some y => y
| None => a
end:option A -> A
exists g : B -> A, forall x : B, f (g x) = x
   exists (fun x => get (List.find (h x) l)).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x : B) (k : A) =>
if d (f k) x then true else false:B -> A -> bool
get:=fun o : option A =>
match o with
| Some y => y
| None => a
end:option A -> A
forall x : B, f (get (find (h x) l)) = x
   intros x.A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
get:=fun o : option A =>
match o with
| Some y => y
| None => a
end:option A -> A
x:B
f (get (find (h x) l)) = x
   case_eq (find (h x) l); simpl; clear get; [intros y H|intros H].A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
y:A
H:find (h x) l = Some y
f y = x
A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
H:find (h x) l = None
f a = x
   *A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
y:A
H:find (h x) l = Some y
f y = x apply find_some in H.A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
y:A
H:In y l /\ h x y = true
f y = x destruct H as (_,H).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
y:A
H:h x y = true
f y = x unfold h in H.A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
y:A
H:(if d (f y) x then true else false) = true
f y = x
     now destruct (d (f y) x) in H.
   *A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
H:find (h x) l = None
f a = x exfalso.A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
H:find (h x) l = None
False
     destruct (Su x) as (y & Y).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
H:find (h x) l = None
y:A
Y:f y = x
False
     generalize (find_none _ l H y (F y)).A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
H:find (h x) l = None
y:A
Y:f y = x
h x y = false -> False
     unfold h.A, B:Type
l:list A
F:Full l
d:EqDec B
f:A -> B
Su:Surjective f
a:A
h:=fun (x0 : B) (k : A) =>
if d (f k) x0 then true else false:B -> A -> bool
x:B
H:find (h x) l = None
y:A
Y:f y = x
(if d (f y) x then true else false) = false -> False now destruct (d (f y) x).
Qed.

Same, with more knowledge on the inverse function: g.f = f.g = id

Lemma Injective_Surjective_Bijective :
 forall A B, Finite A -> EqDec B ->
  forall f:A->B, Injective f -> Surjective f -> Bijective f.forall A B : Type,
Finite A ->
EqDec B ->
forall f : A -> B,
Injective f -> Surjective f -> Bijective f
Proof.forall A B : Type,
Finite A ->
EqDec B ->
forall f : A -> B,
Injective f -> Surjective f -> Bijective f
 intros A B F d f Ij Su.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Ij:Injective f
Su:Surjective f
Bijective f
 destruct (Surjective_inverse F d Su) as (g, E).A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Ij:Injective f
Su:Surjective f
g:B -> A
E:forall x : B, f (g x) = x
Bijective f
 exists g.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Ij:Injective f
Su:Surjective f
g:B -> A
E:forall x : B, f (g x) = x
(forall x : A, g (f x) = x) /\
(forall y : B, f (g y) = y) split; trivial.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Ij:Injective f
Su:Surjective f
g:B -> A
E:forall x : B, f (g x) = x
forall x : A, g (f x) = x
 intros y.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Ij:Injective f
Su:Surjective f
g:B -> A
E:forall x : B, f (g x) = x
y:A
g (f y) = y apply Ij.A, B:Type
F:Finite A
d:EqDec B
f:A -> B
Ij:Injective f
Su:Surjective f
g:B -> A
E:forall x : B, f (g x) = x
y:A
f (g (f y)) = f y now rewrite E.
Qed.

An example of finite type : Fin.t

Lemma Fin_Finite n : Finite (Fin.t n).n:nat
Finite (Fin.t n)
Proof.n:nat
Finite (Fin.t n)
 induction n.Finite (Fin.t 0)
n:nat
IHn:Finite (Fin.t n)
Finite (Fin.t (S n))
 -Finite (Fin.t 0) exists nil.Full nil
   red;inversion a.
 -n:nat
IHn:Finite (Fin.t n)
Finite (Fin.t (S n)) destruct IHn as (l,Hl).n:nat
l:list (Fin.t n)
Hl:Full l
Finite (Fin.t (S n))
   exists (Fin.F1 :: map Fin.FS l).n:nat
l:list (Fin.t n)
Hl:Full l
Full (Fin.F1 :: map Fin.FS l)
   intros a.n:nat
l:list (Fin.t n)
Hl:Full l
a:Fin.t (S n)
In a (Fin.F1 :: map Fin.FS l) revert n a l Hl.forall (n : nat) (a : Fin.t (S n))
  (l : list (Fin.t n)),
Full l -> In a (Fin.F1 :: map Fin.FS l)
   refine (@Fin.caseS _ _ _); intros.n:nat
l:list (Fin.t n)
Hl:Full l
In Fin.F1 (Fin.F1 :: map Fin.FS l)
n:nat
p:Fin.t n
l:list (Fin.t n)
Hl:Full l
In (Fin.FS p) (Fin.F1 :: map Fin.FS l)
   +n:nat
l:list (Fin.t n)
Hl:Full l
In Fin.F1 (Fin.F1 :: map Fin.FS l) now left.
   +n:nat
p:Fin.t n
l:list (Fin.t n)
Hl:Full l
In (Fin.FS p) (Fin.F1 :: map Fin.FS l) right.n:nat
p:Fin.t n
l:list (Fin.t n)
Hl:Full l
In (Fin.FS p) (map Fin.FS l) now apply in_map.
Qed.

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 (Lt.le_not_lt _ _ H' H)
  |try rewrite (n2f_ext H' H) in *; try clear H'].

Lemma extend_ok n f : bFun n (@extend n f).n:nat
f:Fin.t n -> Fin.t n
bFun n (extend f)
Proof.n:nat
f:Fin.t n -> Fin.t n
bFun n (extend f)
 intros x h.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
extend f x < n unfold extend.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
match le_lt_dec n x with
| left _ => 0
| right h0 => f2n (f (n2f h0))
end < n break_dec h.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
f2n (f (n2f h)) < n apply f2n_ok.
Qed.

Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x).n:nat
f:Fin.t n -> Fin.t n
x:Fin.t n
extend f (f2n x) = f2n (f x)
Proof.n:nat
f:Fin.t n -> Fin.t n
x:Fin.t n
extend f (f2n x) = f2n (f x)
 generalize (n2f_f2n x).n:nat
f:Fin.t n -> Fin.t n
x:Fin.t n
n2f (f2n_ok x) = x -> extend f (f2n x) = f2n (f x) unfold extend, f2n, f2n_ok.n:nat
f:Fin.t n -> Fin.t n
x:Fin.t n
n2f (proj2_sig (Fin.to_nat x)) = x ->
match le_lt_dec n (proj1_sig (Fin.to_nat x)) with
| left _ => 0
| right h => proj1_sig (Fin.to_nat (f (n2f h)))
end = proj1_sig (Fin.to_nat (f x))
 destruct (Fin.to_nat x) as (x',h); simpl.n:nat
f:Fin.t n -> Fin.t n
x:Fin.t n
x':nat
h:x' < n
n2f h = x ->
match le_lt_dec n x' with
| left _ => 0
| right h0 => proj1_sig (Fin.to_nat (f (n2f h0)))
end = proj1_sig (Fin.to_nat (f x))
 break_dec h.n:nat
f:Fin.t n -> Fin.t n
x:Fin.t n
x':nat
h:x' < n
n2f h = x ->
proj1_sig (Fin.to_nat (f (n2f h))) =
proj1_sig (Fin.to_nat (f x))
 now intros ->.
Qed.

Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h).n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
n2f (extend_ok f h) = f (n2f h)
Proof.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
n2f (extend_ok f h) = f (n2f h)
 generalize (extend_ok f h).n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
forall l : extend f x < n, n2f l = f (n2f h) unfold extend in *.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
forall
  l : match le_lt_dec n x with
      | left _ => 0
      | right h0 => f2n (f (n2f h0))
      end < n, n2f l = f (n2f h) break_dec h.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
forall l : f2n (f (n2f h)) < n, n2f l = f (n2f h) intros h'.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
h':f2n (f (n2f h)) < n
n2f h' = f (n2f h)
 rewrite <- n2f_f2n.n:nat
f:Fin.t n -> Fin.t n
x:nat
h:x < n
h':f2n (f (n2f h)) < n
n2f h' = n2f (f2n_ok (f (n2f h))) now apply n2f_ext.
Qed.

Lemma restrict_f2n n f hf (x:Fin.t n) :
 f2n (@restrict n f hf x) = f (f2n x).n:nat
f:nat -> nat
hf:bFun n f
x:Fin.t n
f2n (restrict hf x) = f (f2n x)
Proof.n:nat
f:nat -> nat
hf:bFun n f
x:Fin.t n
f2n (restrict hf x) = f (f2n x)
 unfold restrict, f2n.n:nat
f:nat -> nat
hf:bFun n f
x:Fin.t n
proj1_sig
  (Fin.to_nat
     (let (x', h) := Fin.to_nat x in n2f (hf x' h))) =
f (proj1_sig (Fin.to_nat x)) destruct (Fin.to_nat x) as (x',h); simpl.n:nat
f:nat -> nat
hf:bFun n f
x:Fin.t n
x':nat
h:x' < n
proj1_sig (Fin.to_nat (n2f (hf x' h))) = f x'
 apply f2n_n2f.
Qed.

Lemma restrict_n2f n f hf x (h:x<n) :
 @restrict n f hf (n2f h) = n2f (hf _ h).n:nat
f:nat -> nat
hf:bFun n f
x:nat
h:x < n
restrict hf (n2f h) = n2f (hf x h)
Proof.n:nat
f:nat -> nat
hf:bFun n f
x:nat
h:x < n
restrict hf (n2f h) = n2f (hf x h)
 unfold restrict.n:nat
f:nat -> nat
hf:bFun n f
x:nat
h:x < n
(let (x', h0) := Fin.to_nat (n2f h) in n2f (hf x' h0)) =
n2f (hf x h) generalize (f2n_n2f h).n:nat
f:nat -> nat
hf:bFun n f
x:nat
h:x < n
f2n (n2f h) = x ->
(let (x', h0) := Fin.to_nat (n2f h) in n2f (hf x' h0)) =
n2f (hf x h) unfold f2n.n:nat
f:nat -> nat
hf:bFun n f
x:nat
h:x < n
proj1_sig (Fin.to_nat (n2f h)) = x ->
(let (x', h0) := Fin.to_nat (n2f h) in n2f (hf x' h0)) =
n2f (hf x h)
 destruct (Fin.to_nat (n2f h)) as (x',h'); simpl.n:nat
f:nat -> nat
hf:bFun n f
x:nat
h:x < n
x':nat
h':x' < n
x' = x -> n2f (hf x' h') = n2f (hf x h) intros ->.n:nat
f:nat -> nat
hf:bFun n f
x:nat
h, h':x < n
n2f (hf x h') = n2f (hf x h)
 now apply n2f_ext.
Qed.

Lemma extend_surjective n f :
  bSurjective n (@extend n f) <-> Surjective f.n:nat
f:Fin.t n -> Fin.t n
bSurjective n (extend f) <-> Surjective f
Proof.n:nat
f:Fin.t n -> Fin.t n
bSurjective n (extend f) <-> Surjective f
 split.n:nat
f:Fin.t n -> Fin.t n
bSurjective n (extend f) -> Surjective f
n:nat
f:Fin.t n -> Fin.t n
Surjective f -> bSurjective n (extend f)
 -n:nat
f:Fin.t n -> Fin.t n
bSurjective n (extend f) -> Surjective f intros hf y.n:nat
f:Fin.t n -> Fin.t n
hf:bSurjective n (extend f)
y:Fin.t n
exists x : Fin.t n, f x = y
   destruct (hf _ (f2n_ok y)) as (x & h & Eq).n:nat
f:Fin.t n -> Fin.t n
hf:bSurjective n (extend f)
y:Fin.t n
x:nat
h:x < n
Eq:extend f x = f2n y
exists x0 : Fin.t n, f x0 = y
   exists (n2f h).n:nat
f:Fin.t n -> Fin.t n
hf:bSurjective n (extend f)
y:Fin.t n
x:nat
h:x < n
Eq:extend f x = f2n y
f (n2f h) = y
   apply f2n_inj.n:nat
f:Fin.t n -> Fin.t n
hf:bSurjective n (extend f)
y:Fin.t n
x:nat
h:x < n
Eq:extend f x = f2n y
f2n (f (n2f h)) = f2n y now rewrite <- Eq, <- extend_f2n, f2n_n2f.
 -n:nat
f:Fin.t n -> Fin.t n
Surjective f -> bSurjective n (extend f) intros hf y hy.n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
exists x : nat, x < n /\ extend f x = y
   destruct (hf (n2f hy)) as (x,Eq).n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
exists x0 : nat, x0 < n /\ extend f x0 = y
   exists (f2n x).n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
f2n x < n /\ extend f (f2n x) = y
   split.n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
f2n x < n
n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
extend f (f2n x) = y
   +n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
f2n x < n apply f2n_ok.
   +n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
extend f (f2n x) = y rewrite extend_f2n, Eq.n:nat
f:Fin.t n -> Fin.t n
hf:Surjective f
y:nat
hy:y < n
x:Fin.t n
Eq:f x = n2f hy
f2n (n2f hy) = y apply f2n_n2f.
Qed.

Lemma extend_injective n f :
  bInjective n (@extend n f) <-> Injective f.n:nat
f:Fin.t n -> Fin.t n
bInjective n (extend f) <-> Injective f
Proof.n:nat
f:Fin.t n -> Fin.t n
bInjective n (extend f) <-> Injective f
 split.n:nat
f:Fin.t n -> Fin.t n
bInjective n (extend f) -> Injective f
n:nat
f:Fin.t n -> Fin.t n
Injective f -> bInjective n (extend f)
 -n:nat
f:Fin.t n -> Fin.t n
bInjective n (extend f) -> Injective f intros hf x y Eq.n:nat
f:Fin.t n -> Fin.t n
hf:bInjective n (extend f)
x, y:Fin.t n
Eq:f x = f y
x = y
   apply f2n_inj.n:nat
f:Fin.t n -> Fin.t n
hf:bInjective n (extend f)
x, y:Fin.t n
Eq:f x = f y
f2n x = f2n y apply hf; try apply f2n_ok.n:nat
f:Fin.t n -> Fin.t n
hf:bInjective n (extend f)
x, y:Fin.t n
Eq:f x = f y
extend f (f2n x) = extend f (f2n y)
   now rewrite 2 extend_f2n, Eq.
 -n:nat
f:Fin.t n -> Fin.t n
Injective f -> bInjective n (extend f) intros hf x y hx hy Eq.n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
x = y
   rewrite <- (f2n_n2f hx), <- (f2n_n2f hy).n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
f2n (n2f hx) = f2n (n2f hy) f_equal.n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
n2f hx = n2f hy
   apply hf.n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
f (n2f hx) = f (n2f hy)
   rewrite <- 2 extend_n2f.n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
n2f (extend_ok f hx) = n2f (extend_ok f hy)
   generalize (extend_ok f hx) (extend_ok f hy).n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
forall (l : extend f x < n) (l0 : extend f y < n),
n2f l = n2f l0
   rewrite Eq.n:nat
f:Fin.t n -> Fin.t n
hf:Injective f
x, y:nat
hx:x < n
hy:y < n
Eq:extend f x = extend f y
forall l l0 : extend f y < n, n2f l = n2f l0 apply n2f_ext.
Qed.

Lemma restrict_surjective n f h :
  Surjective (@restrict n f h) <-> bSurjective n f.n:nat
f:nat -> nat
h:bFun n f
Surjective (restrict h) <-> bSurjective n f
Proof.n:nat
f:nat -> nat
h:bFun n f
Surjective (restrict h) <-> bSurjective n f
 split.n:nat
f:nat -> nat
h:bFun n f
Surjective (restrict h) -> bSurjective n f
n:nat
f:nat -> nat
h:bFun n f
bSurjective n f -> Surjective (restrict h)
 -n:nat
f:nat -> nat
h:bFun n f
Surjective (restrict h) -> bSurjective n f intros hf y hy.n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
exists x : nat, x < n /\ f x = y
   destruct (hf (n2f hy)) as (x,Eq).n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
exists x0 : nat, x0 < n /\ f x0 = y
   exists (f2n x).n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
f2n x < n /\ f (f2n x) = y
   split.n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
f2n x < n
n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
f (f2n x) = y
   +n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
f2n x < n apply f2n_ok.
   +n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
f (f2n x) = y rewrite <- (restrict_f2n h), Eq.n:nat
f:nat -> nat
h:bFun n f
hf:Surjective (restrict h)
y:nat
hy:y < n
x:Fin.t n
Eq:restrict h x = n2f hy
f2n (n2f hy) = y apply f2n_n2f.
 -n:nat
f:nat -> nat
h:bFun n f
bSurjective n f -> Surjective (restrict h) intros hf y.n:nat
f:nat -> nat
h:bFun n f
hf:bSurjective n f
y:Fin.t n
exists x : Fin.t n, restrict h x = y
   destruct (hf _ (f2n_ok y)) as (x & hx & Eq).n:nat
f:nat -> nat
h:bFun n f
hf:bSurjective n f
y:Fin.t n
x:nat
hx:x < n
Eq:f x = f2n y
exists x0 : Fin.t n, restrict h x0 = y
   exists (n2f hx).n:nat
f:nat -> nat
h:bFun n f
hf:bSurjective n f
y:Fin.t n
x:nat
hx:x < n
Eq:f x = f2n y
restrict h (n2f hx) = y
   apply f2n_inj.n:nat
f:nat -> nat
h:bFun n f
hf:bSurjective n f
y:Fin.t n
x:nat
hx:x < n
Eq:f x = f2n y
f2n (restrict h (n2f hx)) = f2n y now rewrite restrict_f2n, f2n_n2f.
Qed.

Lemma restrict_injective n f h :
  Injective (@restrict n f h) <-> bInjective n f.n:nat
f:nat -> nat
h:bFun n f
Injective (restrict h) <-> bInjective n f
Proof.n:nat
f:nat -> nat
h:bFun n f
Injective (restrict h) <-> bInjective n f
 split.n:nat
f:nat -> nat
h:bFun n f
Injective (restrict h) -> bInjective n f
n:nat
f:nat -> nat
h:bFun n f
bInjective n f -> Injective (restrict h)
 -n:nat
f:nat -> nat
h:bFun n f
Injective (restrict h) -> bInjective n f intros hf x y hx hy Eq.n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
x = y
   rewrite <- (f2n_n2f hx), <- (f2n_n2f hy).n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
f2n (n2f hx) = f2n (n2f hy) f_equal.n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
n2f hx = n2f hy
   apply hf.n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
restrict h (n2f hx) = restrict h (n2f hy)
   rewrite 2 restrict_n2f.n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
n2f (h x hx) = n2f (h y hy)
   generalize (h x hx) (h y hy).n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
forall (l : f x < n) (l0 : f y < n), n2f l = n2f l0
   rewrite Eq.n:nat
f:nat -> nat
h:bFun n f
hf:Injective (restrict h)
x, y:nat
hx:x < n
hy:y < n
Eq:f x = f y
forall l l0 : f y < n, n2f l = n2f l0 apply n2f_ext.
 -n:nat
f:nat -> nat
h:bFun n f
bInjective n f -> Injective (restrict h) intros hf x y Eq.n:nat
f:nat -> nat
h:bFun n f
hf:bInjective n f
x, y:Fin.t n
Eq:restrict h x = restrict h y
x = y
   apply f2n_inj.n:nat
f:nat -> nat
h:bFun n f
hf:bInjective n f
x, y:Fin.t n
Eq:restrict h x = restrict h y
f2n x = f2n y apply hf; try apply f2n_ok.n:nat
f:nat -> nat
h:bFun n f
hf:bInjective n f
x, y:Fin.t n
Eq:restrict h x = restrict h y
f (f2n x) = f (f2n y)
   now rewrite <- 2 (restrict_f2n h), Eq.
Qed.

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).n:nat
f:nat -> nat
bFun n f -> bInjective n f <-> bSurjective n f
Proof.n:nat
f:nat -> nat
bFun n f -> bInjective n f <-> bSurjective n f
 intros h.n:nat
f:nat -> nat
h:bFun n f
bInjective n f <-> bSurjective n f
 rewrite <- (restrict_injective h), <- (restrict_surjective h).n:nat
f:nat -> nat
h:bFun n f
Injective (restrict h) <-> Surjective (restrict h)
 apply Endo_Injective_Surjective.n:nat
f:nat -> nat
h:bFun n f
Finite (Fin.t n)
n:nat
f:nat -> nat
h:bFun n f
decidable_eq (Fin.t n)
 -n:nat
f:nat -> nat
h:bFun n f
Finite (Fin.t n) apply Fin_Finite.
 -n:nat
f:nat -> nat
h:bFun n f
decidable_eq (Fin.t n) intros x y.n:nat
f:nat -> nat
h:bFun n f
x, y:Fin.t n
decidable (x = y) destruct (Fin.eq_dec x y); [left|right]; trivial.
Qed.

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.n:nat
f:nat -> nat
bFun n f ->
bSurjective n f ->
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
Proof.n:nat
f:nat -> nat
bFun n f ->
bSurjective n f ->
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 intro hf.n:nat
f:nat -> nat
hf:bFun n f
bSurjective n f ->
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 rewrite <- (restrict_surjective hf).n:nat
f:nat -> nat
hf:bFun n f
Surjective (restrict hf) ->
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x) intros Su.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 assert (Ij : Injective (restrict hf)).n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Injective (restrict hf)
n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 {n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Injective (restrict hf) apply Endo_Injective_Surjective; trivial.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Finite (Fin.t n)
n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
decidable_eq (Fin.t n)
   -n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Finite (Fin.t n) apply Fin_Finite.
   -n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
decidable_eq (Fin.t n) intros x y.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
x, y:Fin.t n
decidable (x = y) destruct (Fin.eq_dec x y); [left|right]; trivial. }n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 assert (Bi : Bijective (restrict hf)).n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
Bijective (restrict hf)
n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
Bi:Bijective (restrict hf)
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 {n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
Bijective (restrict hf) apply Injective_Surjective_Bijective; trivial.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
Finite (Fin.t n)
n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
EqDec (Fin.t n)
   -n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
Finite (Fin.t n) apply Fin_Finite.
   -n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
EqDec (Fin.t n) exact Fin.eq_dec. }n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
Bi:Bijective (restrict hf)
exists g : nat -> nat,
  bFun n g /\
  (forall x : nat, x < n -> g (f x) = x /\ f (g x) = x)
 destruct Bi as (g & Hg & Hg').n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x : Fin.t n, g (restrict hf x) = x
Hg':forall y : Fin.t n, restrict hf (g y) = y
exists g0 : nat -> nat,
  bFun n g0 /\
  (forall x : nat,
   x < n -> g0 (f x) = x /\ f (g0 x) = x)
 exists (extend g).n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x : Fin.t n, g (restrict hf x) = x
Hg':forall y : Fin.t n, restrict hf (g y) = y
bFun n (extend g) /\
(forall x : nat,
 x < n -> extend g (f x) = x /\ f (extend g x) = x)
 split.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x : Fin.t n, g (restrict hf x) = x
Hg':forall y : Fin.t n, restrict hf (g y) = y
bFun n (extend g)
n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x : Fin.t n, g (restrict hf x) = x
Hg':forall y : Fin.t n, restrict hf (g y) = y
forall x : nat,
x < n -> extend g (f x) = x /\ f (extend g x) = x
 -n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x : Fin.t n, g (restrict hf x) = x
Hg':forall y : Fin.t n, restrict hf (g y) = y
bFun n (extend g) apply extend_ok.
 -n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x : Fin.t n, g (restrict hf x) = x
Hg':forall y : Fin.t n, restrict hf (g y) = y
forall x : nat,
x < n -> extend g (f x) = x /\ f (extend g x) = x intros x Hx.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x0 : Fin.t n, g (restrict hf x0) = x0
Hg':forall y : Fin.t n, restrict hf (g y) = y
x:nat
Hx:x < n
extend g (f x) = x /\ f (extend g x) = x split.n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x0 : Fin.t n, g (restrict hf x0) = x0
Hg':forall y : Fin.t n, restrict hf (g y) = y
x:nat
Hx:x < n
extend g (f x) = x
n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x0 : Fin.t n, g (restrict hf x0) = x0
Hg':forall y : Fin.t n, restrict hf (g y) = y
x:nat
Hx:x < n
f (extend g x) = x
   +n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x0 : Fin.t n, g (restrict hf x0) = x0
Hg':forall y : Fin.t n, restrict hf (g y) = y
x:nat
Hx:x < n
extend g (f x) = x now rewrite <- (f2n_n2f Hx), <- (restrict_f2n hf), extend_f2n, Hg.
   +n:nat
f:nat -> nat
hf:bFun n f
Su:Surjective (restrict hf)
Ij:Injective (restrict hf)
g:Fin.t n -> Fin.t n
Hg:forall x0 : Fin.t n, g (restrict hf x0) = x0
Hg':forall y : Fin.t n, restrict hf (g y) = y
x:nat
Hx:x < n
f (extend g x) = x now rewrite <- (f2n_n2f Hx), extend_f2n, <- (restrict_f2n hf), Hg'.
Qed.