(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

From Coq Require Import ClassicalDescription.
From Coq Require Import List.

Open Scope list_scope.


Section List_compl.

(** Complements on lists. *)

Context {A : Set}.

Lemma nth_cons : forall a0 a (l : list A) i, nth i l a = nth (S i) (a0 :: l) a.
Proof.
induction i;simpl;intros;auto.
Qed.

Lemma length_cons : forall (l : list A) a, (length l < length (a :: l))%nat.
Proof.
induction l;simpl;auto.
Qed.

Lemma length_cons_1 : forall a (l : list A), length (a :: l) = (length l + 1)%nat.
Proof.
induction l;simpl;auto.
Qed.

End List_compl.


Section List_compl_bis.

Context {A B : Type}.

Lemma map_nth_alt :
  forall (f : A -> B) l da db n,
    (n < length l)%nat ->
    nth n (map f l) db = f (nth n l da).
Proof.
intros f l da db.
induction l.
intros n Hn; simpl in Hn; contradict Hn; auto with arith.
intros n; case n.
intros Hnn; now simpl.
clear n; intros n Hn.
apply trans_eq with (nth n (map f l) db).
easy.
rewrite IHl.
easy.
simpl in Hn; auto with arith.
Qed.

Lemma map_ext_strong :
 forall (f g : A -> B) l, (forall a, In a l -> f a = g a) -> map f l = map g l.
Proof.
intros f g; induction l; try easy.
intros H1; simpl.
rewrite IHl.
rewrite H1; try easy.
apply in_eq.
intros b Hb; apply H1.
now apply in_cons.
Qed.

Lemma in_map_inv :
  forall (f : A -> B) l y,
    In y (map f l) -> exists x, In x l /\ y = f x.
Proof.
intros f l y Hy.
destruct l as [ | a l]; try easy.
destruct (In_nth _ _ (f a) Hy) as [n [Hn1 Hn2]].
rewrite map_length in Hn1; rewrite map_nth in Hn2.
exists (nth n (a :: l) a); split; try easy.
now apply nth_In.
Qed.

End List_compl_bis.


Section List_select.

Context {A B : Type}.
Variable P : A -> Prop.

Fixpoint select (l : list A) : list A :=
  match l with
  | nil => nil
  | x :: l' => match excluded_middle_informative (P x) with
    | left _ => x :: select l'
    | right _ => select l'
    end
  end.

Lemma select_length : forall (l : list A), (length (select l) <= length l)%nat.
Proof.
induction l.
simpl; auto with arith.
simpl; case (excluded_middle_informative _); simpl; auto with arith.
Qed.

Lemma In_select_In : forall (l : list A) x, In x (select l) -> In x l.
Proof.
intros l x; induction l.
easy.
simpl.
case (excluded_middle_informative (P a)).
intros H1 H2; case (in_inv H2).
intros H3; now left.
intros H3; right; now apply IHl.
intros H1 H2; right; now apply IHl.
Qed.

Lemma In_select_P : forall (l : list A) x, In x (select l) -> P x.
Proof.
intros l; induction l; simpl.
intros x H; easy.
intros x; case (excluded_middle_informative _); intros H1 H2.
case (in_inv H2).
intros H3; now rewrite <- H3.
intros H3; now apply IHl.
now apply IHl.
Qed.

Lemma In_select_P_inv : forall (l : list A) x, In x l -> P x -> In x (select l).
Proof.
intros l; induction l; simpl.
intros x H; easy.
intros x H1; case H1; intros H2.
rewrite <- H2.
intros H3; case (excluded_middle_informative _); try easy.
intros _; apply in_eq.
intros H3; case (excluded_middle_informative _); intros H4.
apply in_cons; apply IHl; easy.
apply IHl; easy.
Qed.

Lemma NoDup_select : forall (l : list A), NoDup l -> NoDup (select l).
Proof.
intros l; induction l.
easy.
intros H1; simpl.
case (excluded_middle_informative _); intros H2.
apply NoDup_cons_iff; split.
intros H3.
absurd (In a l).
replace l with (nil++l) by easy.
apply NoDup_remove_2; easy.
now apply In_select_In.
apply IHl.
apply (proj1 (NoDup_cons_iff a l) H1).
apply IHl.
apply (proj1 (NoDup_cons_iff a l) H1).
Qed.

End List_select.


Definition RemoveUseless {A B : Type} (f : A -> B) (l : list B) :=
  select (fun x => exists y, f y = x) l.