(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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. *)

#[local] Set Warnings "-stdlib-vector".
Require Import List PeanoNat 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 of the 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 (s. lemma Finite_dec). *)

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

Lemma Listing_decidable_eq {A:Type} (l:list A): Listing l -> decidable_eq A.
Proof.
  intros (Hnodup & Hfull) a a'.
  now apply (NoDup_list_decidable Hnodup).
Qed.

Lemma Finite_dec {A:Type}: Finite A /\ decidable_eq A <-> Finite' A.
Proof.
  split.
  - intros ((l, Hfull) & Hdec).
    destruct (uniquify Hdec l) as (l' & H_nodup & H_inc).
    exists l'. split; trivial.
    intros a. apply H_inc. apply Hfull.
  - intros (l & Hlist).
    apply Listing_decidable_eq in Hlist as Heqdec.
    destruct Hlist as (Hnodup & Hfull).
    split; [ exists l | ]; assumption.
Qed.

(* Finite_alt is a weaker version of Finite_dec and has been deprecated.  *)
Lemma Finite_alt_deprecated A (d:decidable_eq A) : Finite A <-> Finite' A.
Proof.
 split.
 - intros F. now apply Finite_dec.
 - intros (l & _ & F). now exists l.
Qed.
#[deprecated(since="8.17", note="Use Finite_dec instead.")]
Notation Finite_alt := Finite_alt_deprecated.

(** 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).
Proof.
 intros Ij. induction 1 as [|x l X N IH]; simpl; constructor; trivial.
 rewrite in_map_iff. intros (y & E & Y). apply Ij in E. 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)).
Proof.
 split.
 - intros. now apply Injective_map_NoDup.
 - intros H x y E.
   destruct (d x y); trivial.
   assert (N : NoDup (x::y::nil)).
   { repeat constructor; simpl; intuition. }
   specialize (H _ N). simpl in H. rewrite E in H.
   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).
Proof.
 intros L f. split.
 - intros Ij. apply Injective_map_NoDup; trivial. apply L.
 - intros N x y E.
   assert (X : In x l) by apply L.
   assert (Y : In y l) by apply L.
   apply In_nth_error in X. destruct X as (i,X).
   apply In_nth_error in Y. destruct Y as (j,Y).
   assert (X' := map_nth_error f _ _ X).
   assert (Y' := map_nth_error f _ _ Y).
   assert (i = j).
   { rewrite NoDup_nth_error in N. apply N.
     - rewrite <- nth_error_Some. now rewrite X'.
     - rewrite X', Y'. now f_equal. }
   subst j. rewrite Y in X. 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)).
Proof.
 split.
 - intros Su lB.
   induction lB as [|b lB IH].
   + now exists nil.
   + destruct (Su b) as (a,E).
     destruct IH as (lA,IC).
     exists (a::lA). simpl. rewrite E.
     intros x [X|X]; simpl; intuition.
 - intros H y.
   destruct (H (y::nil)) as (lA,IC).
   assert (IN : In y (map f lA)) by (apply (IC y); now left).
   rewrite in_map_iff in IN. destruct IN as (x & E & _).
   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)).
Proof.
 intros (lB,FB) d f. split.
 - rewrite Surjective_list_carac.
   intros Su. destruct (Su lB) as (lA,IC).
   destruct (uniquify_map d f lA) as (lA' & N & IC').
   exists lA'. split; trivial.
   intro x. apply IC', IC, FB.
 - intros (lA & N & FA) y.
   generalize (FA y). rewrite in_map_iff. intros (x & E & _).
   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.
Proof.
 intros A F d f. rewrite (Surjective_carac F d). split.
 - assert (Finite' A) as (l, L) by (now apply Finite_dec); clear F.
   rewrite (Injective_carac L); intros.
   exists l; split; trivial.
   destruct L as (N,F).
   assert (I : incl l (map f l)).
   { apply NoDup_length_incl; trivial.
     - now rewrite length_map.
     - intros x _. apply F. }
   intros x. apply I, F.
 - clear F d. intros (l,L).
   assert (N : NoDup l). { apply (NoDup_map_inv f), L. }
   assert (I : incl (map f l) l).
   { apply NoDup_length_incl; trivial.
     - now rewrite length_map.
     - intros x _. apply L. }
   assert (L' : Listing l).
   { split; trivial.
     intro x. apply I, L. }
   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.
Proof.
 intros (l,F).
 destruct l as [|a l].
 - left; exact F.
 - 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.
Proof.
 intros A B F d f Su.
 destruct (Finite_Empty_or_not F) as [noA | (a,_)].
 - (* A is empty : g is obtained via False_rect *)
   assert (noB : B -> False). { intros y. now destruct (Su y). }
   exists (fun y => False_rect _ (noB y)).
   intro y. destruct (noB y).
 - (* A is inhabited by a : we use it in Option.get *)
   destruct F as (l,F).
   set (h := fun x k => if d (f k) x then true else false).
   set (get := fun o => match o with Some y => y | None => a end).
   exists (fun x => get (List.find (h x) l)).
   intros x.
   case_eq (find (h x) l); simpl; clear get; [intros y H|intros H].
   * apply find_some in H. destruct H as (_,H). unfold h in H.
     now destruct (d (f y) x) in H.
   * exfalso.
     destruct (Su x) as (y & Y).
     generalize (find_none _ l H y (F y)).
     unfold h. 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.
Proof.
 intros A B F d f Ij Su.
 destruct (Surjective_inverse F d Su) as (g, E).
 exists g. split; trivial.
 intros y. apply Ij. now rewrite E.
Qed.


(** An example of finite type : [Fin.t] *)

Lemma Fin_Finite n : Finite (Fin.t n).
Proof.
 induction n as [|n IHn].
 - exists nil.
   red;inversion 1.
 - destruct IHn as (l,Hl).
   exists (Fin.F1 :: map Fin.FS l).
   intros a. revert n a l Hl.
   refine (@Fin.caseS _ _ _); intros.
   + now left.
   + right. 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 (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).
Proof.
 intros x h. unfold extend. break_dec h. apply f2n_ok.
Qed.

Lemma extend_f2n n f (x:Fin.t n) : extend f (f2n x) = f2n (f x).
Proof.
 generalize (n2f_f2n x). unfold extend, f2n, f2n_ok.
 destruct (Fin.to_nat x) as (x',h); simpl.
 break_dec h.
 now intros ->.
Qed.

Lemma extend_n2f n f x (h:x<n) : n2f (extend_ok f h) = f (n2f h).
Proof.
 generalize (extend_ok f h). unfold extend in *. break_dec h. intros h'.
 rewrite <- n2f_f2n. now apply n2f_ext.
Qed.

Lemma restrict_f2n n f hf (x:Fin.t n) :
 f2n (@restrict n f hf x) = f (f2n x).
Proof.
 unfold restrict, f2n. destruct (Fin.to_nat x) as (x',h); simpl.
 apply f2n_n2f.
Qed.

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

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

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

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

Lemma restrict_injective n f h :
  Injective (@restrict n f h) <-> bInjective n f.
Proof.
 split.
 - intros hf x y hx hy Eq.
   rewrite <- (f2n_n2f hx), <- (f2n_n2f hy). f_equal.
   apply hf.
   rewrite 2 restrict_n2f.
   generalize (h x hx) (h y hy).
   rewrite Eq. apply n2f_ext.
 - intros hf x y Eq.
   apply f2n_inj. apply hf; try apply f2n_ok.
   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).
Proof.
 intros h.
 rewrite <- (restrict_injective h), <- (restrict_surjective h).
 apply Endo_Injective_Surjective.
 - apply Fin_Finite.
 - intros 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.
Proof.
 intro hf.
 rewrite <- (restrict_surjective hf). intros Su.
 assert (Ij : Injective (restrict hf)).
 { apply Endo_Injective_Surjective; trivial.
   - apply Fin_Finite.
   - intros x y. destruct (Fin.eq_dec x y); [left|right]; trivial. }
 assert (Bi : Bijective (restrict hf)).
 { apply Injective_Surjective_Bijective; trivial.
   - apply Fin_Finite.
   - exact Fin.eq_dec. }
 destruct Bi as (g & Hg & Hg').
 exists (extend g).
 split.
 - apply extend_ok.
 - intros x Hx. split.
   + now rewrite <- (f2n_n2f Hx), <- (restrict_f2n hf), extend_f2n, Hg.
   + now rewrite <- (f2n_n2f Hx), extend_f2n, <- (restrict_f2n hf), Hg'.
Qed.