(** * Preliminaries *)

(* Switch Coq into implicit argument mode *)

Global Set Implicit Arguments. 
Global Unset Strict Implicit.

(* Load basic Coq libraries *)

Require Export Omega List Morphisms.

(* Inversion tactic *)

Ltac inv H := inversion H; subst; clear H.

(* Beteva destuct tactics *)

Tactic Notation "destruct" "_":=
  match goal with
  | [ |- context[match ?X with _ => _ end] ] => destruct X
  | [ H : context[match ?X with _ => _ end] |- _ ] => destruct X 
  end.

Tactic Notation "destruct" "_" "eqn" ":" ident(E)   :=
  match goal with
  | [ |- context[match ?X with _ => _ end] ] => destruct X eqn:E
  | [ H : context[match ?X with _ => _ end] |- _ ] => destruct X eqn:E
  end.

Tactic Notation "destruct" "_" "eqn" ":" "_"   :=
  let E := fresh "E" in
  match goal with
  | [ |- context[match ?X with _ => _ end] ] => destruct X eqn:E
  | [ H : context[match ?X with _ => _ end] |- _ ] => destruct X eqn:E
  end.

Tactic Notation "destruct" "*" :=
  repeat destruct _.

Tactic Notation "destruct" "*" "eqn" ":" ident(E) :=
  repeat (let E := fresh E in destruct _ eqn:E; try progress inv E); try now congruence.

Tactic Notation "destruct" "*" "eqn" ":" "_" := destruct * eqn:E.

(* ** Decidability *)

Definition dec (X : Prop) : Type := {X} + {~ X}.

Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70).

(* Register dec as a type class *)

Existing Class dec.

Definition decision (X : Prop) (D : dec X) : dec X := D.
Arguments decision X {D}.

Tactic Notation "decide" constr(p) := 
  destruct (decision p).
Tactic Notation "decide" constr(p) "as" simple_intropattern(i) := 
  destruct (decision p) as i.

(* Hints for auto concerning dec *)

Hint Unfold dec.
Hint Extern 4 =>     
match goal with
  | [  |- dec ?p ] => exact (decision p)
end.

(* Improves type class inference *)

Hint Extern 4 =>     
match goal with
  | [  |- dec ((fun _ => _) _) ] => simpl
end : typeclass_instances.

(* Regiseva instance rules for dec *)

Instance True_dec :  dec True := 
  left I.

Instance False_dec :  dec False := 
  right (fun A => A).

Instance impl_dec (X Y : Prop) :  
  dec X -> dec Y -> dec (X -> Y).
Proof.
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto. 
Defined.

Instance and_dec (X Y : Prop) :  
  dec X -> dec Y -> dec (X /\ Y).
Proof. 
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto. 
Defined.

Instance or_dec (X Y : Prop) : 
  dec X -> dec Y -> dec (X \/ Y).
Proof. 
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto. 
Defined.

(* Coq standard modules make "not" and "iff" opaque for type class inference, can be seen with Print HintDb typeclass_instances. *)

Instance not_dec (X : Prop) : 
  dec X -> dec (~ X).
Proof. 
(* Goal: forall _ : dec X, dec (not X) *)
  unfold not. auto.
Defined.

Instance iff_dec (X Y : Prop) : 
  dec X -> dec Y -> dec (X <-> Y).
Proof. 
(* Goal: @In X y (@cons X x A') *)
  unfold iff. auto.
Qed.

Lemma dec_DN X : 
  dec X -> ~~ X -> X.
Proof. 
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto. 
Qed.

Lemma dec_DM_and X Y :  
  dec X -> dec Y -> ~ (X /\ Y) -> ~ X \/ ~ Y.
Proof. 
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto. 
Qed.

Lemma dec_DM_impl X Y :  
  dec X -> dec Y -> ~ (X -> Y) -> X /\ ~ Y.
Proof. 
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto. 
Qed.

Lemma dec_prop_iff (X Y : Prop) : 
  (X <-> Y) -> dec X -> dec Y.
Proof.
(* Goal: forall (_ : iff X Y) (_ : dec X), dec Y *)
  unfold dec; tauto.
Defined.

Instance bool_eq_dec : 
  eq_dec bool.
Proof.
(* Goal: forall x y : nat, dec (@eq nat x y) *)
  intros x y. hnf. decide equality.
Defined.

Instance nat_eq_dec : 
  eq_dec nat.
Proof.
(* Goal: forall x y : nat, dec (@eq nat x y) *)
  intros x y. hnf. decide equality.
Defined.

Instance prod_eq_dec X Y : eq_dec X -> eq_dec Y -> eq_dec (X * Y).
Proof.
(* Goal: @Proper (forall _ : list X, nat) (@respectful (list X) nat (@equi X) (@eq nat)) (@card X D) *)
  intros ? ? ? ?. hnf. decide equality. eapply X1. eapply X0.
Defined.

Instance nat_le_dec (x y : nat) : dec (x <= y) := 
  le_dec x y.

(* * Lists *)

(* Notations for lists *)

Definition equi X (A B : list X) : Prop :=
  incl A B /\ incl B A.

Hint Unfold equi.

Export ListNotations.
Notation "| A |" := (length A) (at level 65).
Notation "x 'el' A" := (In x A) (at level 70).
Notation "A <<= B" := (incl A B) (at level 70).
Notation "A === B" := (equi A B) (at level 70).

(* The following comments are for coqdoc *)
(** printing el ∊ *)
(** printing <<= ⊆ *)
(** printing === ≡ *)

(* A useful lemma *)

Lemma list_cycle  (X : Type) (A : list X) x :
  x::A <> A.
Proof.
(* Goal: not (@eq (list X) (@cons X x A) A) *)
  intros B.
(* Goal: False *)
  assert (C: |x::A| <> |A|) by (simpl; omega).
(* Goal: False *)
  apply C. now rewrite B.
Qed.

(* Decidability laws for lists *)

Instance list_eq_dec X :  
  eq_dec X -> eq_dec (list X).
Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
  intros D. apply list_eq_dec. exact D. 
Defined.

Instance list_in_dec (X : Type) (x : X) (A : list X) :  
  eq_dec X -> dec (x el A).
Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
  intros D. apply in_dec. exact D.
Defined.

Lemma list_sigma_forall X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
  {x | x el A /\ p x} + {forall x, x el A -> ~ p x}.
Proof.
(* Goal: @dupfree X (undup A) *)
  induction A as [|x A]; simpl.
(* Goal: @In X y (@cons X x A') *)
  - tauto.
  - destruct IHA as [[y [D E]]|D].
(* Goal: @In X y (@cons X x A') *)
    + eauto. 
    + destruct (p_dec x) as [E|E].
(* Goal: @In X y (@cons X x A') *)
      * eauto.
(* Goal: @In X y (@cons X x A') *)
      * right. intros y [[]|F]; auto. 
Defined.

Arguments list_sigma_forall {X} A p {p_dec}.

Instance list_forall_dec X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
  dec (forall x, x el A -> p x).
Proof.
(* Goal: dec (forall (x : X) (_ : @In X x A), p x) *)
  destruct (list_sigma_forall A (fun x => ~ p x)) as [[x [D E]]|D].
(* Goal: @In X y (@cons X x A') *)
  - right. auto.
(* Goal: @In X y (@cons X x A') *)
  - left. intros x E. apply dec_DN; auto.
Defined.

Instance list_exists_dec X A (p : X -> Prop) (p_dec : forall x, dec (p x)) :
  dec (exists x, x el A /\ p x).
Proof.
(* Goal: dec (@ex X (fun x : X => and (@In X x A) (p x))) *)
  destruct (list_sigma_forall A p) as [[x [D E]]|D].
(* Goal: @In X y (@cons X x A') *)
  - eauto.
  - right. intros [x [E F]]. exact (D x E F).
Defined.

Lemma list_exists_DM X A  (p : X -> Prop) : 
  (forall x, dec (p x)) ->
  ~ (forall x, x el A -> ~ p x) -> exists x, x el A /\ p x.
Proof. 
(* Goal: forall (_ : @incl X A B) (_ : @eq nat (card A) (card B)), @equi X A B *)
  intros D E. 
(* Goal: @ex X (fun x : X => and (@In X x A) (p x)) *)
  destruct (list_sigma_forall A p) as [F|F].
(* Goal: @In X y (@cons X x A') *)
  + destruct F as [x F]. eauto.
  + contradiction (E F).
Qed.

Lemma list_cc X (p : X -> Prop) A : 
  (forall x, dec (p x)) -> 
  (exists x, x el A /\ p x) -> {x | x el A /\ p x}.
Proof.
(* Goal: forall (_ : @incl X A B) (_ : @eq nat (card A) (card B)), @equi X A B *)
  intros D E. 
(* Goal: @sig X (fun x : X => and (@In X x A) (p x)) *)
  destruct (list_sigma_forall A p) as [[x [F G]]|F].
(* Goal: @In X y (@cons X x A') *)
  - eauto.
(* Goal: @In X y (@cons X x A') *)
  - exfalso. destruct E as [x [G H]]. apply (F x); auto.
Defined.

(* Membership

We use the following facts from the standard library List.
- [in_eq :  x el x::A]
- [in_nil :  ~ x el nil]
- [in_cons :  x el A -> x el y::A]
- [in_or_app :  x el A \/ x el B -> x el A++B]
- [in_app_iff :  x el A++B <-> x el A \/ x el B]
- [in_map_iff :  y el map f A <-> exists x, f x = y /\ x el A]
*)

Hint Resolve in_eq in_nil in_cons in_or_app.

Lemma in_sing X (x y : X) :
  x el [y] -> x = y.

Proof. simpl. intros [[]|[]]. reflexivity. Qed.

Lemma in_cons_neq X (x y : X) A :
  x el y::A -> x <> y -> x el A.

Proof. simpl. intros [[]|D] E; congruence. Qed.

(* Inclusion
-
-We use the following facts from the standard library List.
-- [A <<= B = forall y, x el A -> x el B]
-- [incl_refl :  A <<= A]
-- [incl_tl :  A <<= B -> A <<= x::B]
-- [incl_cons : x el B -> A <<= B -> x::A <<= B]
-- [incl_appl : A <<= B -> A <<= B++C]
-- [incl_appr : A <<= C -> A <<= B++C]
-- [incl_app : A <<= C -> B <<= C -> A++B <<= C]
-*)

Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app.

Lemma incl_nil X (A : list X) :
  nil <<= A.

Proof. intros x []. Qed.

Hint Resolve incl_nil.

Lemma incl_map X Y A B (f : X -> Y) :
  A <<= B -> map f A <<= map f B.

Proof.
(* Goal: forall _ : @incl X A B, @incl X (@cons X x A) (@cons X x B) *)
  intros D y E. apply in_map_iff in E as [x [E E']].
(* Goal: @In X y (@cons X x A') *)
  subst y. apply in_map_iff. eauto.
Qed.

Section Inclusion.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma incl_nil_eq A :
    A <<= nil -> A=nil.

  Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    intros D. destruct A as [|x A].
    - reflexivity.
(* Goal: @In X y (@cons X x A') *)
    - exfalso. apply (D x). auto.
  Qed.

  Lemma incl_shift x A B :
    A <<= B -> x::A <<= x::B.

(* Goal: @In X y (@cons X x A') *)
  Proof. intros D y E. destruct E; subst; auto. Qed.

  Lemma incl_lcons x A B :
    x::A <<= B <-> x el B /\ A <<= B.

  Proof. 
(* Goal: @equi X A B *)
    split. 
(* Goal: @In X y (@cons X x A') *)
    - intros D. split; hnf; auto.
(* Goal: @In X y (@cons X x A') *)
    - intros [D E] z [F|F]; subst; auto.
  Qed.

  Lemma incl_rcons x A B :
    A <<= x::B -> ~ x el A -> A <<= B.

  Proof. intros C D y E. destruct (C y E) as [F|F]; congruence. Qed.

  Lemma incl_lrcons x A B :
    x::A <<= x::B -> ~ x el A -> A <<= B.

  Proof.
(* Goal: forall (_ : @incl X (@cons X x A) (@cons X x B)) (_ : not (@In X x A)), @incl X A B *)
    intros C D y E.
(* Goal: @In X y (@cons X x A') *)
    assert (F: y el x::B) by auto.
(* Goal: @In X y B *)
    destruct F as [F|F]; congruence.
  Qed.

End Inclusion.

Hint Resolve incl_shift.

Definition inclp (X : Type) (A : list X) (p : X -> Prop) : Prop :=
  forall x, x el A -> p x.

(* Setoid rewriting with list inclusion and list equivalence *)

Instance in_equi_proper X : 
  Proper (eq ==> @equi X ==> iff) (@In X).

Proof. hnf. intros x y []. hnf. firstorder. Qed.

Instance incl_equi_proper X : 
  Proper (@equi X ==> @equi X ==> iff) (@incl X).

Proof. hnf. intros x y D. hnf. firstorder. Qed.

Instance incl_preorder X : PreOrder (@incl X).

(* Goal: @In X y (@cons X x A') *)
Proof. constructor; hnf; unfold incl; auto. Qed.

Instance equi_Equivalence X : Equivalence (@equi X).

Proof. constructor; hnf; firstorder. Qed.

Instance cons_equi_proper X : 
  Proper (eq ==> @equi X ==> @equi X) (@cons X).

Proof. hnf. intros x y []. hnf. firstorder. Qed.

Instance app_equi_proper X : 
  Proper (@equi X ==> @equi X ==> @equi X) (@app X).

Proof. 
(* Goal: @Proper (forall _ : list X, nat) (@respectful (list X) nat (@equi X) (@eq nat)) (@card X D) *)
  hnf. intros A B D. hnf. intros A' B' E.
(* Goal: @In X y (@cons X x A') *)
  destruct D, E; auto.
Qed.

(* Equivalence *)

Section Equi.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma equi_push x A :
    x el A -> A === x::A.

(* Goal: @In X y (@cons X x A') *)
  Proof. auto. Qed.

  Lemma equi_dup x A :
    x::A === x::x::A.

(* Goal: @In X y (@cons X x A') *)
  Proof. auto. Qed.

  Lemma equi_swap x y A:
    x::y::A === y::x::A.

(* Goal: @In X y (@cons X x A') *)
  Proof. split; intros z; simpl; tauto. Qed.

  Lemma equi_shift x A B :
    x::A++B === A++x::B.

  Proof. 
(* Goal: @equi X (@cons X x (@app X A B)) (@app X A (@cons X x B)) *)
    split; intros y.
    - intros [D|D].
(* Goal: @In X y (@cons X x A') *)
      + subst; auto.
(* Goal: @In X y (@cons X x A') *)
      + apply in_app_iff in D as [D|D]; auto.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    - intros D. apply in_app_iff in D as [D|D].
(* Goal: @In X y (@cons X x A') *)
      + auto.
(* Goal: @In X y (@cons X x A') *)
      + destruct D; subst; auto.
  Qed.

  Lemma equi_rotate x A :
    x::A === A++[x].
  
  Proof. 
(* Goal: lt (@length X (@cons X y A')) (@length X (@cons X y A)) *)
    split; intros y; simpl.
(* Goal: @In X y (@cons X x A') *)
    - intros [D|D]; subst; auto.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    - intros D. apply in_app_iff in D as [D|D].
(* Goal: @In X y (@cons X x A') *)
      + auto.
(* Goal: @In X y (@cons X x A') *)
      + apply in_sing in D. auto.
  Qed.
End Equi.

(* * Filter *)

Definition filter (X : Type) (p : X -> Prop) (p_dec : forall x, dec (p x)) : list X -> list X :=
  fix f A := match A with
              | nil => nil
              | x::A' => if decision (p x) then x :: f A' else f A'
            end.

Arguments filter {X} p {p_dec} A.

Section FilterLemmas.
  Variable X : Type.
  Variable p : X -> Prop.
  Context {p_dec : forall x, dec (p x)}.

  Lemma in_filter_iff x A :
    x el filter p A <-> x el A /\ p x.
    
  Proof. 
(* Goal: lt (@length X (@cons X y A')) (@length X (@cons X y A)) *)
    induction A as [|y A]; simpl.
(* Goal: @In X y (@cons X x A') *)
    - tauto.
    - decide (p y) as [B|B]; simpl;
(* Goal: @In X y (@cons X x A') *)
      rewrite IHA; intuition; subst; tauto.
  Qed.

  Lemma filter_incl A :
    filter p A <<= A.
  
  Proof.
(* Goal: @incl X (@filter X p p_dec A) A *)
    intros x D. apply in_filter_iff in D. apply D.
  Qed.

  Lemma filter_mono A B :
    A <<= B -> filter p A <<= filter p B.

  Proof.
(* Goal: forall _ : @incl X A B, @incl X (@filter X p p_dec A) (@filter X p p_dec B) *)
    intros D x E. apply in_filter_iff in E as [E E'].
(* Goal: @In X y (@cons X x A') *)
    apply in_filter_iff. auto.
  Qed.

  Lemma filter_fst x A :
    p x -> filter p (x::A) = x::filter p A.
  Proof.
(* Goal: @In X y (@cons X x A') *)
    simpl. decide (p x); tauto.
  Qed.

  Lemma filter_app A B :
    filter p (A ++ B) = filter p A ++ filter p B.
  Proof.
(* Goal: lt (@length X (@cons X y A')) (@length X (@cons X y A)) *)
    induction A as [|y A]; simpl.
    - reflexivity.
    - rewrite IHA. decide (p y); reflexivity.  
  Qed.

  Lemma filter_fst' x A :
    ~ p x -> filter p (x::A) = filter p A.
  Proof.
(* Goal: @In X y (@cons X x A') *)
    simpl. decide (p x); tauto.
  Qed.

End FilterLemmas.

(* * Element removal *)

Section Removal.
  Variable X : Type.
  Context {eq_X_dec : eq_dec X}.

  Definition rem (A : list X) (x : X) : list X :=
    filter (fun z => z <> x) A.

  Lemma in_rem_iff x A y :
    x el rem A y <-> x el A /\ x <> y.
  Proof.
(* Goal: iff (@In X x (rem A y)) (and (@In X x A) (not (@eq X x y))) *)
    apply in_filter_iff.
  Qed.

  Lemma rem_not_in x y A :
    x = y \/ ~ x el A -> ~ x el rem A y.
  Proof.
(* Goal: @In X y (@cons X x A') *)
    intros D E. apply in_rem_iff in E. tauto.
  Qed.

  Lemma rem_incl A x :
    rem A x <<= A.
  Proof.
(* Goal: @incl X (rem A x) A *)
    apply filter_incl.
  Qed.

  Lemma rem_mono A B x :
    A <<= B -> rem A x <<= rem B x.
  Proof.
(* Goal: forall _ : @incl X A B, @incl X (rem A x) (rem B x) *)
    apply filter_mono.
  Qed.

  Lemma rem_cons A B x :
    A <<= B -> rem (x::A) x <<= B.
  Proof.
(* Goal: forall _ : @In X x A, @incl X B (@app X A (rem B x)) *)
    intros E y F. apply E. apply in_rem_iff in F.
(* Goal: @In X y A *)
    destruct F as [[|]]; congruence.
  Qed.

  Lemma rem_cons' A B x y :
    x el B -> rem A y <<= B -> rem (x::A) y <<= B.
  Proof.
(* Goal: forall (_ : @In X x B) (_ : @incl X (rem A y) B), @incl X (rem (@cons X x A) y) B *)
    intros E F u G. 
(* Goal: @In X u B *)
    apply in_rem_iff in G as [[[]|G] H]. exact E.
(* Goal: @In X y (@cons X x A') *)
    apply F. apply in_rem_iff. auto.
  Qed.

  Lemma rem_in x y A :
    x el rem A y -> x el A.
  Proof.
(* Goal: forall _ : @In X x (rem A y), @In X x A *)
    apply rem_incl.
  Qed.

  Lemma rem_neq x y A :
    x <> y -> x el A -> x el rem A y.
  Proof.
(* Goal: @In X y (@cons X x A') *)
    intros E F. apply in_rem_iff. auto.
  Qed.

  Lemma rem_app x A B :
    x el A -> B <<= A ++ rem B x.
  Proof.
(* Goal: forall _ : @In X x A, @incl X B (@app X A (rem B x)) *)
    intros E y F. decide (x=y) as [[]|]; auto using rem_neq.
  Qed.

  Lemma rem_equi x A :
    x::A === x::rem A x.
  Proof.
    split; intros y; 
    intros [[]|E]; decide (x=y) as [[]|D]; 
    eauto using rem_in, rem_neq. 
  Qed.

  Lemma rem_fst x A :
    rem (x::A) x = rem A x.
  Proof.
(* Goal: @In X y (@cons X x A') *)
    unfold rem. rewrite filter_fst'; auto.
  Qed.

  Lemma rem_fst' x y A :
    x <> y -> rem (x::A) y = x::rem A y.
  Proof.
(* Goal: @In X y (@cons X x A') *)
    intros E. unfold rem. rewrite filter_fst; auto.
  Qed.

End Removal.

Hint Resolve rem_not_in rem_incl rem_mono rem_cons rem_cons' rem_app rem_in rem_neq.

(* * Duplicate-free lists *)

Inductive dupfree (X : Type) : list X -> Prop :=
| dupfreeN : dupfree nil
| dupfreeC x A : ~ x el A -> dupfree A -> dupfree (x::A).

Section Dupfree.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma dupfree_inv x A :
    dupfree (x::A) <-> ~ x el A /\ dupfree A.
  Proof. 
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    split; intros D.
(* Goal: @In X y (@cons X x A') *)
    - inv D; auto.
(* Goal: @In X y (@cons X x A') *)
    - apply dupfreeC; tauto.
  Qed.

  Lemma dupfree_map Y A (f : X -> Y) :
    (forall x y, x el A -> y el A -> f x = f y -> x=y) -> 
    dupfree A -> dupfree (map f A).

  Proof.
(* Goal: forall (_ : @incl X A B) (_ : @eq nat (card A) (card B)), @equi X A B *)
    intros D E. induction E as [|x A E' E]; simpl.
    - constructor.
    - constructor; [|now auto].
(* Goal: not (@dupfree X (@cons X x A)) *)
      intros F. apply in_map_iff in F as [y [F F']].
(* Goal: @In X y (@cons X x A') *)
      rewrite (D y x) in F'; auto.
  Qed.

  Lemma dupfree_filter p (p_dec : forall x, dec (p x)) A :
    dupfree A -> dupfree (filter p A).

  Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    intros D. induction D as [|x A C D]; simpl.
    - left.
    - decide (p x) as [E|E]; [|exact IHD].
(* Goal: @dupfree X (@cons X x (@filter X p p_dec A)) *)
      right; [|exact IHD].
(* Goal: False *)
      intros F. apply C. apply filter_incl in F. exact F.
   Qed.

  Lemma dupfree_dec A :
    eq_dec X -> dec (dupfree A).

  Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    intros D. induction A as [|x A].
    - left. left.
    - decide (x el A) as [E|E].
(* Goal: @In X y (@cons X x A') *)
      + right. intros F. inv F; tauto.
      + destruct (IHA) as [F|F].
        * auto using dupfree.
(* Goal: @In X y (@cons X x A') *)
        * right. intros G. inv G; tauto.
  Qed.

End Dupfree.

Section Undup.
  Variable X : Type.
  Context {eq_X_dec : eq_dec X}.
  Implicit Types A B : list X.

  Fixpoint undup (A : list X) : list X :=
    match A with
      | nil => nil
      | x::A' => if decision (x el A') then undup A' else  x :: undup A'
    end.

  Lemma undup_fp_equi A :
    undup A === A.
  Proof.
(* Goal: @dupfree X (undup A) *)
    induction A as [|x A]; simpl.
    - reflexivity.
(* Goal: @In X y (@cons X x A') *)
    - decide (x el A) as [E|E]; rewrite IHA; auto.
  Qed.

  Lemma dupfree_undup A :
    dupfree (undup A).
  Proof.
(* Goal: @dupfree X (undup A) *)
    induction A as [|x A]; simpl.
    - left.
(* Goal: @In X y (@cons X x A') *)
    - decide (x el A) as [E|E]; auto.
(* Goal: @In X y (@cons X x A') *)
      right; auto. now rewrite undup_fp_equi. 
  Qed.

  Lemma undup_incl A B :
    A <<= B <-> undup A <<= undup B.
  Proof.
(* Goal: iff (@equi X A B) (@equi X (undup A) (undup B)) *)
    now do 2 rewrite undup_fp_equi.
  Qed.

  Lemma undup_equi A B :
    A === B <-> undup A === undup B.
  Proof.
(* Goal: iff (@equi X A B) (@equi X (undup A) (undup B)) *)
    now do 2 rewrite undup_fp_equi.
  Qed.

  Lemma undup_eq A :
    dupfree A -> undup A = A.
  Proof.
(* Goal: lt (@length X (@cons X y A')) (@length X (@cons X y A)) *)
    intros E. induction E as [|x A E F]; simpl.
    - reflexivity.
(* Goal: @In X y (@cons X x A') *)
    - rewrite IHF. decide (x el A) as [G|G]; tauto.
  Qed.

  Lemma undup_idempotent A :
    undup (undup A) = undup A.

  Proof. apply undup_eq, dupfree_undup. Qed.

End Undup.

Section DupfreeLength.
  Variable X : Type.
  Implicit Types A B : list X.

  Lemma dupfree_reorder A x :
    dupfree A -> x el A -> 
    exists A', A === x::A' /\ |A'| < |A| /\ dupfree (x::A').

  Proof.
(* Goal: forall _ : lt (card A) (card B), @ex X (fun x : X => and (@In X x B) (not (@In X x A))) *)
    intros E. revert x. induction E as [|y A H]; intros x F.
    - contradiction F.
    - destruct F as [F|F].
      + subst y. exists A. auto using dupfree. 
      + specialize (IHE x F). destruct IHE as [A' [G [K1 K2]]].
(* Goal: @ex (list X) (fun A' : list X => and (@equi X (@cons X y A) (@cons X x A')) (and (lt (@length X A') (@length X (@cons X y A))) (@dupfree X (@cons X x A')))) *)
        exists (y::A'). split; [|split].
        * rewrite G. apply equi_swap.
        * simpl. omega.
        * { apply dupfree_inv in K2 as [K2 K3]. right. 
(* Goal: @In X y (@cons X x A') *)
            - intros [M|M]; subst; auto.
            - right; [|exact K3].
(* Goal: @In X y (@cons X x A') *)
              intros M; apply H. apply G. auto. }
   Qed.

  Lemma dupfree_le A B :
    dupfree A -> dupfree B -> A <<= B -> |A| <= |B|.

  Proof. 
(* Goal: forall (_ : @dupfree X A) (_ : @dupfree X B) (_ : @incl X A B), le (@length X A) (@length X B) *)
    intros E; revert B.
(* Goal: forall (B : list X) (_ : @dupfree X B) (_ : @incl X A B), le (@length X A) (@length X B) *)
    induction A as [|x A]; simpl; intros B F G.
    - omega.
    - apply incl_lcons in G as [G H]. 
(* Goal: le (S (@length X A)) (@length X B) *)
      destruct (dupfree_reorder F G) as [B' [K [L M]]].
(* Goal: le (S (@length X A)) (@length X B) *)
      apply dupfree_inv in E as [E1 E2].
(* Goal: le (S (@length X A)) (@length X B) *)
      apply dupfree_inv in M as [M1 M2].
(* Goal: le (S (@length X A)) (@length X B) *)
      cut (A <<= B').
(* Goal: gt (@length X A) n *)
(* Goal: @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
      { intros N. specialize (IHA E2 B' M2 N). omega. }
(* Goal: @incl X A B' *)
      apply incl_rcons with (x:=x); [|exact E1].
(* Goal: @incl X A (@cons X x B') *)
      rewrite H. apply K.
  Qed.

  Lemma dupfree_eq A B :
    dupfree A -> dupfree B -> A === B -> |A|=|B|.

  Proof. 
(* Goal: forall (_ : @dupfree X A) (_ : @dupfree X B) (_ : @equi X A B), @eq nat (@length X A) (@length X B) *)
    intros D E [F G]. 
(* Goal: @eq nat (@length X A) (@length X B) *)
    apply (dupfree_le D E) in F. 
(* Goal: @eq nat (@length X A) (@length X B) *)
    apply (dupfree_le E D) in G. 
(* Goal: gt (@length X A) n *)
(* Goal: @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
    omega.
  Qed.

  Lemma dupfree_lt A B x :
    dupfree A -> dupfree B -> A <<= B -> 
    x el B -> ~ x el A  -> |A| < |B|.

  Proof.
(* Goal: forall (_ : @dupfree X A) (_ : @dupfree X B) (_ : @incl X A B) (_ : @In X x B) (_ : not (@In X x A)), lt (@length X A) (@length X B) *)
    intros E F G H K.
(* Goal: lt (@length X A) (@length X B) *)
    destruct (dupfree_reorder F H) as [B' [L [M N]]].
(* Goal: lt (@length X A) (@length X B) *)
    rewrite (dupfree_eq F N L). 
(* Goal: gt (@length X A) n *)
(* Goal: @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
    cut (|A|<=|B'|). { simpl; omega. }
(* Goal: le (card A) (card B) *)
    apply dupfree_le.
    - exact E.
    - now inv N.
    - apply incl_rcons with (x:=x).
      + rewrite G. apply  L.
      + exact K.
  Qed.

  Lemma dupfree_ex A B :
    eq_dec X -> dupfree A -> dupfree B -> |A| < |B| -> exists x, x el B /\ ~ x el A.

  Proof.
(* Goal: forall (_ : forall x y : X, dec (@eq X x y)) (_ : @dupfree X A) (_ : @dupfree X B) (_ : lt (@length X A) (@length X B)), @ex X (fun x : X => and (@In X x B) (not (@In X x A))) *)
    intros D E F H.
(* Goal: @ex X (fun x : X => and (@In X x B) (not (@In X x A))) *)
    destruct (list_sigma_forall B (fun x => ~ x el A)) as [[x K]|K].
    - exists x; exact K.
    - exfalso. 
(* Goal: False *)
      assert (L : B <<= A).
(* Goal: @In X y (@cons X x A') *)
      { intros x L. apply dec_DN; auto. }
(* Goal: gt (@length X A) n *)
(* Goal: @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
      apply dupfree_le in L; auto; omega.
  Qed.

  Lemma dupfree_equi A B :
    eq_dec X -> dupfree A -> dupfree B -> A <<= B -> |A|=|B| -> A === B.

  Proof.
(* Goal: @equi X A B *)
    intros C D E F G. split. exact F.
(* Goal: @incl X B A *)
    destruct (list_sigma_forall B (fun x => ~ x el A)) as [[x [H K]]|H].
    - exfalso. assert (L:=dupfree_lt D E F H K). omega.
(* Goal: @In X y (@cons X x A') *)
    - intros x L. apply dec_DN; auto.
  Qed.

End DupfreeLength.
 
(* * Cardinality *)

Section Cardinality.
  Variable X : Type.
  Context {eq_X_dec : eq_dec X}.
  Implicit Types A B : list X.

  Definition card (A : list X) : nat := |undup A|.

  Lemma card_le A B :
    A <<= B -> card A <= card B.

  Proof.
(* Goal: forall _ : lt (card A) (card B), @ex X (fun x : X => and (@In X x B) (not (@In X x A))) *)
    intros E. apply dupfree_le.
    - apply dupfree_undup. 
    - apply dupfree_undup.
    - apply undup_incl, E.
  Qed.

  Lemma card_eq A B :
    A === B -> card A = card B.

  Proof.
(* Goal: gt (@length X A) n *)
(* Goal: @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
    intros [E F]. apply card_le in E. apply card_le in F. omega.
  Qed.

  Lemma card_equi A B :
    A <<= B -> card A = card B -> A === B.
  Proof.
(* Goal: forall (_ : @incl X A B) (_ : @eq nat (card A) (card B)), @equi X A B *)
    intros D E.
    apply <- undup_equi. apply -> undup_incl in D.
(* Goal: @equi X (@undup X eq_X_dec A) (@undup X eq_X_dec B) *)
    apply dupfree_equi; auto using dupfree_undup.    
  Qed.

  Lemma card_lt A B x :
    A <<= B -> x el B -> ~ x el A -> card A < card B.

  Proof.
(* Goal: forall (_ : @incl X A B) (_ : @In X x B) (_ : not (@In X x A)), lt (card A) (card B) *)
    intros D E F.
(* Goal: lt (card A) (card B) *)
    apply (dupfree_lt (A:= undup A) (B:= undup B) (x:=x)).
    - apply dupfree_undup.
    - apply dupfree_undup.
    - apply undup_incl, D.
    - apply undup_fp_equi, E.
    - rewrite undup_fp_equi. exact F.
  Qed.

  Lemma card_or A B :
    A <<= B -> A === B \/ card A < card B.

  Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    intros D.
(* Goal: or (@equi X A B) (lt (card A) (card B)) *)
    decide (card A = card B) as [F|F].
(* Goal: @In X y (@cons X x A') *)
    - left. apply card_equi; auto.
    - right. apply card_le in D. omega.
  Qed.

  Lemma card_ex A B :
    card A < card B -> exists x, x el B /\ ~ x el A.

  Proof.
(* Goal: forall _ : lt (card A) (card B), @ex X (fun x : X => and (@In X x B) (not (@In X x A))) *)
    intros E.
(* Goal: @ex X (fun x : X => and (@In X x B) (not (@In X x A))) *)
    destruct (dupfree_ex (A:=undup A) (B:=undup B)) as [x F].
    - exact eq_X_dec.
    - apply dupfree_undup.
    - apply dupfree_undup.
    - exact E.
    - exists x. setoid_rewrite undup_fp_equi in F. exact F.
     (*Coq bug: Must use setoid_rewrite here *)
  Qed.

  Lemma card_cons x A :
    card (x::A) = if decision (x el A) then card A else 1 + card A.
  Proof.
(* Goal: lt (@length X (@cons X y A')) (@length X (@cons X y A)) *)
    unfold card at 1; simpl. now decide (x el A). 
  Qed.

  Lemma card_cons_rem x A :
    card (x::A) = 1 + card (rem A x).
  Proof.
(* Goal: @eq nat (card (@cons X x A)) (Init.Nat.add (S O) (card (@rem X eq_X_dec A x))) *)
    rewrite (card_eq (rem_equi x A)). 
(* Goal: @eq nat (card (@cons X x (@rem X eq_X_dec A x))) (Init.Nat.add (S O) (card (@rem X eq_X_dec A x))) *)
    rewrite card_cons.
(* Goal: @eq nat (if @decision (@In X x (@rem X eq_X_dec A x)) (@list_in_dec X x (@rem X eq_X_dec A x) eq_X_dec) then card (@rem X eq_X_dec A x) else Init.Nat.add (S O) (card (@rem X eq_X_dec A x))) (Init.Nat.add (S O) (card (@rem X eq_X_dec A x))) *)
    decide (x el rem A x) as [D|D].
(* Goal: @In X y (@cons X x A') *)
    - apply in_rem_iff in D; tauto.
    - reflexivity.
  Qed.

  Lemma card_0 A :
    card A = 0 -> A = nil.
  Proof.
(* Goal: forall _ : @incl X A B, or (@equi X A B) (lt (card A) (card B)) *)
    destruct A as [|x A]; intros D.
    - reflexivity.
    - exfalso. rewrite card_cons_rem in D. omega.
  Qed.

End Cardinality.

Instance card_equi_proper X (D: eq_dec X) : 
  Proper (@equi X ==> eq) (@card X D).
Proof. 
(* Goal: @Proper (forall _ : list X, nat) (@respectful (list X) nat (@equi X) (@eq nat)) (@card X D) *)
  hnf. apply card_eq.
Qed.

Lemma complete_induction (p : nat -> Prop) (x : nat) :
(forall x, (forall y, y<x -> p y) -> p x) -> p x.

(* Goal: forall _ : forall (x : nat) (_ : forall (y : nat) (_ : lt y x), p y), p x, p x *)
Proof. intros A. apply A. induction x ; intros y B.
(* Goal: gt (@length X A) n *)
(* Goal: @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
exfalso ; omega.
apply A. intros z C. apply IHx. omega. Qed.

Lemma size_induction X (f : X -> nat) (p : X -> Prop) :
  (forall x, (forall y, f y < f x -> p y) -> p x) -> 
  forall x, p x.

Proof. 
(* Goal: forall (_ : forall (x : X) (_ : forall (y : X) (_ : lt (f y) (f x)), p y), p x) (x : X), p x *)
  intros IH x. apply IH. 
  assert (G: forall n y, f y < n -> p y).
(* Goal: forall (n : nat) (y : X) (_ : lt (f y) n), p y *)
(* Goal: forall (y : X) (_ : lt (f y) (f x)), p y *)
  { intros n. induction n.
    - intros y B. exfalso. omega.
    - intros y B. apply IH. intros z C. apply IHn. omega. }
(* Goal: forall (y : X) (_ : lt (f y) (f x)), p y *)
  apply G.
Qed.

(** Positions and map-products for lists *)

Section Positions.
  Variables (X: Type) (d: eq_dec X).
  Implicit Types (x y: X) (A B : list X).

  Fixpoint pos x A : option nat :=
    match A with
    | nil => None
    | y :: A' => if d x y then Some 0
                else match pos x A' with
                     | Some n => Some (S n)
                     | None => None
                     end
    end.

  Lemma el_pos x A :
    x el A -> { n | pos x A = Some n }.
  Proof.
(* Goal: forall _ : @In X x A, @sig nat (fun n : nat => @eq (option nat) (pos x A) (@Some nat n)) *)
    induction A as [|y A IH]; cbn; intros H.
    - destruct H as [].
    - destruct (d x y) as [<-|H1].
      + now exists 0.
      + destruct IH as [n IH].
(* Goal: @In X y (@cons X x A') *)
        * destruct H as [->|H]; tauto.
        * rewrite IH. now exists (S n).
  Qed.

  Fixpoint nth n A : option X :=
    match A, n with
    | nil, _ => None
    | x::_, 0 => Some x
    | _::A', S n' => nth n' A'
    end.

  Lemma nth_length A n :
    length A > n -> { x | nth n A = Some x }.
  Proof.
(* Goal: forall _ : @eq (option X) (nth n A) (@Some X x), @eq (option X) (nth n (@app X A B)) (@Some X x) *)
    revert n.
(* Goal: forall (n : nat) (_ : gt (@length X A) n), @sig X (fun x : X => @eq (option X) (nth n A) (@Some X x)) *)
    induction A as [|y A IH]; cbn; intros n H.
    - exfalso. omega.
    - destruct n as [|n]; cbn.
      + now exists y.
      + destruct (IH n) as [x H1]. omega. now exists x.
  Qed.
  
 Lemma pos_nth x A n :
    pos x A = Some n -> nth n A = Some x.
 Proof.
(* Goal: forall _ : @eq (option X) (nth n A) (@Some X x), @eq (option X) (nth n (@app X A B)) (@Some X x) *)
   revert n.
(* Goal: forall (n : nat) (y : X) (_ : lt (f y) n), p y *)
   induction A as [|y A IH]; cbn; intros n.
    - intros [=].
    - destruct (d x y) as [<-|H1].
      + now intros [= <-].
      + destruct (pos x A) as [k|]; intros [= <-]; cbn.
(* Goal: p y *)
        now apply IH.
  Qed.
  
  Lemma nth_app_l x n A B :
    nth n A = Some x -> nth n (A ++ B) = Some x.
  Proof.
(* Goal: forall _ : @eq (option X) (nth n A) (@Some X x), @eq (option X) (nth n (@app X A B)) (@Some X x) *)
    revert n.
(* Goal: forall (n : nat) (_ : @eq (option X) (nth n A) (@Some X x)), @eq (option X) (nth n (@app X A B)) (@Some X x) *)
    induction A as [|y A IH]; cbn; intros k H.
    - destruct k; discriminate H.
    - destruct k as [|k]; cbn in *. exact H.
(* Goal: @eq (option X) (nth k (@app X A B)) (@Some X x) *)
      apply IH, H.
  Qed.

End Positions.

Section MapProduct.
  Variables (X Y Z: Type) (f: X -> Y -> Z).

  Fixpoint map_pro (A: list X) (B: list Y) : list Z :=
    match A with
    | x :: A' => map_pro A' B ++ map (f x) B
    | nil => nil
    end.

  Lemma map_pro_in x A B :
    x el map_pro A B <-> exists a b, a el A /\ b el B /\ f a b = x.
  Proof.
(* Goal: iff (@In Z x (map_pro A B)) (@ex X (fun a : X => @ex Y (fun b : Y => and (@In X a A) (and (@In Y b B) (@eq Z (f a b) x))))) *)
  induction A as [|a A IH]; cbn.
  - firstorder.
  - rewrite in_app_iff, IH, in_map_iff. 
(* Goal: @In X y (@cons X x A') *)
    firstorder; subst; eauto.
  Qed.

End MapProduct.


(* Section pos. *)
  
(*   Definition elAt := nth_error. *)
(*   Notation "A '.[' i  ']'" := (elAt A i) (no associativity, at level 50). *)
  
(*   Fixpoint pos (X : Type) {e : eq_dec X} (s : X) (A : list X) := *)
(*     match A with *)
(*       | nil => None *)
(*       | a :: A => if decision (s = a) then Some 0 else match pos s A with None => None | Some n => Some (S n) end *)
(*     end. *)
  
(*   Lemma el_pos X (E : eq_dec X) s A : s el A -> exists m, pos s A = Some m. *)
(*   Proof. *)
(*     revert s; induction A; simpl; intros s H. *)
(*       - contradiction. *)
(*       - decide (s = a) as [D | D]; eauto;  *)
(*         destruct H; try congruence. *)
(*         destruct (IHA s H) as [n Hn]; eexists; now rewrite Hn. *)
(*   Qed. *)
  
(*   Lemma pos_elAt X (_ : eq_dec X) s A i : pos s A = Some i -> A .[i] = Some s. *)
(*   Proof. *)
(*     revert i s. induction A; intros i s. *)
(*     - destruct i; inversion 1. *)
(*     - simpl. decide (s = a). *)
(*       + inversion 1; subst; reflexivity. *)
(* Goal: @In X y (@cons X x A') *)
(*       + destruct i; destruct (pos s A) eqn:B; inversion 1; subst; eauto.  *)
(*   Qed. *)
  
(*   Lemma elAt_app X (A : list X) i B s : A .[i] = Some s -> (A ++ B).[i] = Some s. *)
(*   Proof. *)
(*     revert s B i. induction A; intros s B i H; destruct i; simpl; intuition; inv H. *)
(*   Qed. *)
  
(*   Lemma elAt_el (X : Type) A (s : X) m : A .[ m ] = Some s -> s el A. *)
(*   Proof. *)
(* Goal: @In X y (@cons X x A') *)
(*     revert A. induction m; intros []; inversion 1; eauto. *)
(*   Qed. *)
  
(*   Lemma el_elAt X {_ : eq_dec X} (s : X) A : s el A -> exists m, A .[ m ] = Some s. *)
(*   Proof. *)
(*     intros H; destruct (el_pos _ H); eexists; eauto using pos_elAt. *)
(*   Qed. *)

(* Lemma dupfree_elAt X (A : list X) n m s : dupfree A -> A.[n] = Some s -> A.[m] = Some s -> n = m. *)
(* Goal: @In X y (@cons X x A') *)
(* Proof with try tauto. *)
(*   intros H; revert n m; induction A; simpl; intros n m H1 H2. *)
(*   - destruct n; inv H1. *)
(*   - destruct n, m; inv H... *)
(*     + inv H1. simpl in H2. eapply elAt_el in H2... *)
(*     + inv H2. simpl in H1. eapply elAt_el in H1...  *)
(*     + inv H1. inv H2. rewrite IHA with n m...  *)
(* Qed. *)

(* Lemma nth_error_none A n l : nth_error l n = @None A -> length l <= n. *)
(* Proof. revert n; *)
(*   induction l; intros n. *)
(*   - simpl; omega. *)
(* Goal: @In X y (@cons X x A') *)
(*   - simpl. intros. destruct n. inv H. inv H. assert (| l | <= n). eauto. omega. *)
(* Qed. *)

(* End pos. *)
