(*******************************************************************************)
(* Copyright 2015-2016 Catherine Dubois, Richard Genestier and Alain Giorgetti *) 
(* Samovar - FEMTO-ST institute                                                *)
(*******************************************************************************)

(*******************************************************************************)
(*      This file is distributed under the terms of the                        *)
(*       GNU Lesser General Public License Version 2.1                         *)
(*******************************************************************************)

(** Some definitions and lemmas related to finite functions. *)

Require Import List Compare_dec EqNat Decidable Omega.

Require Import prelude.

Set Implicit Arguments.

(** * General definitions *)

(* As in FinFun 8.5 *)
Definition bFun n (f:nat->nat) := forall x, x < n -> f x < n.

(* As in FinFun 8.5 *)
Definition bInjective n (f:nat->nat) :=
 forall x y, x < n -> y < n -> f x = f y -> x = y.

Definition bFull n (l : list nat)  := forall a, a < n ->  In a l. 

Definition bBelowl (n : nat) (l : list nat) := 
forall i, In i l -> i < n.

Definition bseq (n : nat) (l : list nat) := bBelowl n l /\ bFull n l.

Lemma bBelowl_cons n l x : bBelowl n (x::l) -> bBelowl n l.
Proof.
unfold bBelowl.
intros.
intuition.
Qed.

Lemma bInjective_map_NoDup f l n : 
 bInjective n f -> bBelowl n l -> NoDup l -> NoDup (map f l).
Proof.
induction l; simpl; constructor; trivial.
 rewrite in_map_iff. intros (y & E & Y). 
inversion_clear H1. apply H in E.
subst; contradiction.
eapply bBelowl_cons; eassumption.
apply H0; simpl; auto.
inversion_clear  H1.
apply IHl; auto.
eapply bBelowl_cons; eassumption.
Qed.

Lemma bInjective_carac (l:list nat) n : bseq n l -> NoDup l -> 
   forall f, bInjective n f <-> NoDup (map f l).
Proof.
 intros B L f. split.
 - intros Ij. apply bInjective_map_NoDup with (n:=n); trivial. 
   apply B.
 - intros N x y E1 E2 F.
   assert (X : In x l) by (apply B; assumption).  
   assert (Y : In y l) by (apply B; assumption).
   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.

(* Extracted from coq-8.5 *)
Lemma in_seq len start n :
    In n (seq start len) <-> start <= n < start+len.
  Proof.
   revert start. induction len; simpl; intros.
   - rewrite <- plus_n_O. split;[easy|].
     intros (H,H'). apply (Lt.lt_irrefl _ (Lt.le_lt_trans _ _ _ H H')).
   - rewrite IHlen, <- plus_n_Sm; simpl; split.
     * intros [H|H]; subst; intuition auto with arith.
     * intros (H,H'). destruct (Lt.le_lt_or_eq _ _ H); intuition.
  Qed.

(* Extracted from coq-8.5 *)
Lemma seq_NoDup len start : NoDup (seq start len).
  Proof.
   revert start; induction len; simpl; constructor; trivial.
   rewrite in_seq. intros (H,_). apply (Lt.lt_irrefl _ H).
  Qed.

Lemma bInjective_carac_seq n :  
   forall f, bInjective n f <-> NoDup (map f (seq 0 n)).
Proof.
apply bInjective_carac.
split.
intros x I.
apply in_seq in I .
easy.
intros x X.
apply in_seq; omega.
apply seq_NoDup.
Qed.
