(*******************************************************************************)
(* 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                         *)
(*******************************************************************************)

(** General purpose definitions and lemmas. Some of them may already exist
 in the standard library. *)

Require Import List.

Section List_prelude.

Variable A : Type.
Variable eq_dec : forall (x y : A), {eq x y}+{~ eq x y}.

Fixpoint mem a l : bool :=
 match l with
 | nil => false
 | cons e t => if (eq_dec e a) then true else mem a t
end.

Fixpoint uniq l : bool :=
 match l with
 | nil => true
 | cons e t => if (mem e t) then false else uniq t
end.

Lemma in_mem :
 forall x l, In x l <-> mem x l = true.
Proof.
    split.
    (* -> *)
    induction l.
    simpl.
    intro.
    auto.
    simpl.
    intro.
    case_eq (eq_dec a x).
    intros.
    reflexivity.
    intros.
    destruct H.
    auto.
    apply IHl.
    assumption.
    (* <- *)
    induction l.
    simpl.
    intros.
    inversion H.
    simpl.
    intros.
    case_eq (eq_dec a x).
    intros.
    left.
    assumption.
    intros.
    rewrite H0 in H.
    right.
    apply IHl.
    assumption.
Qed.

Lemma no_in_mem :
    forall a l,
    ~List.In a l <-> mem a l = false.
  Proof.
    split.
  (* -> *)
    intros.
    induction l.
    simpl.
    reflexivity.
    simpl.
    case_eq (eq_dec a0 a).
    intros.
    rewrite e in H.
    simpl in *.
    destruct H.
    left.
    reflexivity.
    intros.
    simpl in H.
    assert (~(a0 = a) /\ ~(In a l)).
   split;intro; apply H ;tauto.
    inversion H1.
    apply (IHl H3).
  (* <- *)
    intros.
    induction l.
    apply in_nil.
    simpl in *.
    intro Hyp ; decompose [or] Hyp.
    case_eq (eq_dec a0 a);intros;  rewrite H1 in H ; [ inversion H |  contradiction ].
    case_eq (eq_dec a0 a);intros;  rewrite H1 in H ; [ inversion H |  apply (IHl H H0)].
Qed.

Lemma noDup_uniq :
    forall l,
    uniq l = true <-> NoDup l.
    Proof.
    split.
    (* -> *)
    induction l.
    simpl.
    intro.
    constructor. 
    simpl. 
    case_eq (mem a l); intros.
    inversion H0.
    constructor.
    rewrite <- no_in_mem in H.
    assumption.
    auto.
    (* <- *)
    induction l; simpl; intro.
    reflexivity.
    inversion H.
    case_eq (mem a l); intro.
    rewrite no_in_mem in H2.
    rewrite H4 in H2.
    inversion H2.
    apply (IHl H3).
Qed.

End List_prelude.

  (** Results about [nth_error] *)
  (* extracted from coq8.5*)
Set Implicit Arguments.

Section Lists1.

  Variable A : Type.

  Lemma nth_error_In l n (x:A) : nth_error l n = Some x -> In x l.
  Proof.
    revert n. induction l as [|a l IH]; intros [|n]; simpl; try easy.
    - injection 1; auto.
    - eauto.
  Qed.

  Lemma In_nth_error l (x: A) : In x l -> exists n, nth_error l n = Some x.
  Proof.
    induction l as [|a l IH].
    - easy.
    - intros [H|H].
      * subst; exists 0; simpl; auto with arith.
      * destruct (IH H) as (n,Hn).
        exists (S n); simpl; auto with arith.
  Qed.

  Lemma nth_error_None (l: list A) n : nth_error l n = None <-> length l <= n.
  Proof.
    revert n. induction l; destruct n; simpl.
    - split; auto.
    - split; auto with arith.
    - split; now auto with arith.
    - rewrite IHl; split; auto with arith.
  Qed.

  Lemma nth_error_Some (l: list A) n : nth_error l n <> None <-> n < length l.
  Proof.
   revert n. induction l; destruct n; simpl.
    - split; [now destruct 1 | inversion 1].
    - split; [now destruct 1 | inversion 1].
    - split; now auto with arith.
    - rewrite IHl; split; auto with arith.
  Qed.

  Lemma nth_error_split l n (a: A) : nth_error l n = Some a ->
    exists l1, exists l2, l = l1 ++ a :: l2 /\ length l1 = n.
  Proof.
    revert l.
    induction n as [|n IH]; intros [|x l] H; simpl in *; try easy.
    - exists nil; exists l. injection H; clear H; intros; now subst.
    - destruct (IH _ H) as (l1 & l2 & H1 & H2).
      exists (x::l1); exists l2; simpl; split; now f_equal.
  Qed.

  Lemma nth_error_app1 (l: list A) l' n : n < length l ->
    nth_error (l++l') n = nth_error l n.
  Proof.
    revert l.
    induction n; intros [|a l] H; auto; try solve [inversion H].
    simpl in *. apply IHn. auto with arith.
  Qed.

  Lemma nth_error_app2 (l: list A) l' n : length l <= n ->
    nth_error (l++l') n = nth_error l' (n-length l).
  Proof.
    revert l.
    induction n; intros [|a l] H; auto; try solve [inversion H].
    simpl in *. apply IHn. auto with arith.
  Qed.

  (** Alternative characterisations of being without duplicates,
      thanks to [nth_error] and [nth] *)

  Lemma NoDup_nth_error (l: list A) :
    NoDup l <->
    (forall i j, i<length l -> nth_error l i = nth_error l j -> i = j).
  Proof.
    split.
    { intros H; induction H as [|a l Hal Hl IH]; intros i j Hi E.
      - inversion Hi.
      - destruct i, j; simpl in *; auto.
        * elim Hal. eapply nth_error_In; eauto.
        * elim Hal. eapply nth_error_In; eauto.
        * f_equal. apply IH; auto with arith. }
    { induction l as [|a l]; intros H; constructor.
      * intro Ha. apply In_nth_error in Ha. destruct Ha as (n,Hn).
        assert (n < length l) by (now rewrite <- nth_error_Some, Hn).
        specialize (H 0 (S n)). simpl in H. discriminate H; auto with arith.
      * apply IHl.
        intros i j Hi E. apply eq_add_S, H; simpl; auto with arith. }
  Qed.


(** *** Predicate for List addition/removal (no need for decidability) *)


  (* [Add a l l'] means that [l'] is exactly [l], with [a] added
     once somewhere *)
  Inductive Add (a:A) : list A -> list A -> Prop :=
    | Add_head l : Add a l (a::l)
    | Add_cons x l l' : Add a l l' -> Add a (x::l) (x::l').

  Lemma Add_app a l1 l2 : Add a (l1++l2) (l1++a::l2).
  Proof.
   induction l1; simpl; now constructor.
  Qed.

  Lemma Add_split a l l' :
    Add a l l' -> exists l1 l2, l = l1++l2 /\ l' = l1++a::l2.
  Proof.
   induction 1.
   - exists nil; exists l; split; trivial.
   - destruct IHAdd as (l1 & l2 & Hl & Hl').
     exists (x::l1); exists l2; split; simpl; f_equal; trivial.
  Qed.

  Lemma Add_in a l l' : Add a l l' ->
   forall x, In x l' <-> In x (a::l).
  Proof.
   induction 1; intros; simpl in *; rewrite ?IHAdd; tauto.
  Qed.

  Lemma Add_length a l l' : Add a l l' -> length l' = S (length l).
  Proof.
   induction 1; simpl; auto with arith.
  Qed.

  Lemma Add_inv a l : In a l -> exists l', Add a l' l.
  Proof.
   intro Ha. destruct (in_split _ _ Ha) as (l1 & l2 & ->).
   exists (l1 ++ l2). apply Add_app.
  Qed.

  Lemma incl_Add_inv a l u v :
    ~In a l -> incl (a::l) v -> Add a u v -> incl l u.
  Proof.
   intros Ha H AD y Hy.
   assert (Hy' : In y (a::u)).
   { rewrite <- (Add_in AD). apply H; simpl; auto. }
   destruct Hy'; [ subst; now elim Ha | trivial ].
  Qed.


  Lemma NoDup_length_incl (l: list A) l' :
    NoDup l -> length l' <= length l -> incl l l' -> incl l' l.
  Proof.
   intros N. revert l'. induction N as [|a l Hal N IH].
   - destruct l'; easy.
   - intros l' E H x Hx.
     destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. }
     rewrite (Add_in AD) in Hx. simpl in Hx.
     destruct Hx as [Hx|Hx]; [left; trivial|right].
     revert x Hx. apply (IH l''); trivial.
     * apply le_S_n. now rewrite <- (Add_length AD).
     * now apply incl_Add_inv with a l'.
  Qed.

(** *** NoDup and map *)

(** NB: the reciprocal result holds only for injective functions,
    see [FinFun.v] *)


Lemma NoDup_map_inv B (f:A->B) l : NoDup (map f l) -> NoDup l.
Proof.
 induction l; simpl; inversion_clear 1; subst; constructor; auto.
 intro H. now apply (in_map f) in H.
Qed.

End Lists1.

(** *** Boolean operations over lists *)

  Section Bool1.
    Variable A : Type.
    Variable f : A -> bool.

(*
Fixpoint find (l:list A) : option A :=
      match l with
	| nil => None
	| x :: tl => if f x then Some x else find tl
      end.
*)

    Lemma find_some (l: list A) x : find f l = Some x -> In x l /\ f x = true.
    Proof.
     induction l as [|a l IH]; simpl; [easy| ].
     case_eq (f a); intros Ha Eq.
     * injection Eq as ->; auto.
     * destruct (IH Eq); auto.
    Qed.

    Lemma find_none l : find f l = None -> forall x, In x l -> f x = false.
    Proof.
     induction l as [|a l IH]; simpl; [easy|].
     case_eq (f a); intros Ha Eq x IN; [easy|].
     destruct IN as [<-|IN]; auto.
    Qed.
End Bool1.
