Require Export Bool Omega List Setoid Morphisms Tactics.

Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Records.
Global Unset Printing Implicit Defensive.
Global Set Regular Subst Tactic.

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

Hint Extern 4 =>
match goal with
|[ H: ?x el nil |- _ ] => destruct H
end.

Lemma in_sing {X} (x y:X) :
    x el [y] -> x = y.
Proof.
    cbn. intros [[]|[]]. reflexivity.
Qed.

Lemma in_concat_iff A l (a:A) : a el concat l <-> exists l', a el l' /\ l' el l.
Proof.
  induction l; cbn.
  - intuition. now destruct H.
  - rewrite in_app_iff, IHl. firstorder subst. auto.
Qed.

Lemma incl_nil X (A : list X) :
  nil <<= A.
Proof. intros x []. Qed.

Hint Rewrite <- app_assoc : list.
Hint Rewrite rev_app_distr map_app prod_length : list.
Hint Resolve in_eq in_nil in_cons in_or_app.
Hint Resolve incl_refl incl_tl incl_cons incl_appl incl_appr incl_app incl_nil.

Definition dec (X: Prop) : Type := {X} + {~ X}.
Coercion dec2bool P (d: dec P) := if d then true else false.
Existing Class dec.
Definition Dec (X: Prop) (d: dec X) : dec X := d.
Arguments Dec X {d}.

Hint Extern 4 => (* Improves type class inference *)
match goal with
  | [ |- dec ((fun _ => _) _) ] => cbn
end : typeclass_instances.

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

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

Structure eqType := EqType {
  eqType_X :> Type;
  eqType_dec : eq_dec eqType_X }.

Arguments EqType X {_} : rename.
Canonical Structure eqType_CS X (A: eq_dec X) := EqType X.
Existing Instance eqType_dec.

Instance list_eq_dec X :
  eq_dec X -> eq_dec (list X).
Proof.
  unfold dec. decide equality.
Defined.

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

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" "*" :=
  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.

Hint Extern 4 =>
match goal with
|[ H: False |- _ ] => destruct H
|[ H: true=false |- _ ] => discriminate H
|[ H: false=true |- _ ] => discriminate H
end.

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.
  intros IH x. apply IH.
  assert (G: forall n y, f y < n -> p y).
  { intros n. induction n.
    - intros y B. exfalso. omega.
    - intros y B. apply IH. intros z C. apply IHn. omega. }
  apply G.
Qed.

Fixpoint count (X: Type) `{eq_dec X} (A: list X) (x: X) {struct A} : nat :=
  match A with
  | nil => O
  | cons y A' => if Dec (x=y) then S(count A' x) else count A' x end.

Class finTypeC (type:eqType) : Type := FinTypeC {
                                            enum: list type;
                                            enum_ok: forall x: type, count enum x = 1
                                          }.

Structure finType : Type := FinType {
                                type:> eqType;
                                class: finTypeC type }.

Arguments FinType type {class}.
Existing Instance class | 0.

Canonical Structure finType_CS (X : Type) {p : eq_dec X} {class : finTypeC (EqType X)} : finType := FinType (EqType X).

Definition elem (F: finType) := @enum (type F) (class F).
Hint Unfold elem.
Hint Unfold class.

Ltac dec := repeat (destruct Dec).

Lemma countIn (X:eqType) (x:X) A:
  count A x > 0 -> x el A.
Proof.
  induction A.
  - cbn. omega.
  - cbn. dec.
    + intros. left. symmetry. exact e.
    + intros. right. apply IHA. exact H.
Qed.

Lemma elem_spec (X: finType) (x:X) : x el (elem X).
Proof.
  apply countIn. pose proof (enum_ok x) as H. unfold elem. omega.
Qed.

Hint Resolve elem_spec.
Hint Resolve enum_ok.

Lemma countSplit (X: eqType) (A B: list X) (x: X) : count A x + count B x = count (A ++ B) x.
Proof.
  induction A.
  - reflexivity.
  - cbn. decide (x=a).
    +cbn. f_equal; exact IHA.
    + exact IHA.
Qed.

Lemma notInZero (X: eqType) (x: X) A :
  not (x el A) <-> count A x = 0.
Proof.
  split; induction A.
  - reflexivity.
  - intros H. cbn in *. dec.
    + exfalso. apply H. left. congruence.
    + apply IHA. intros F. apply H. now right.
  - tauto.
  - cbn. dec.
    + subst a. omega.
    + intros H [E | E].
      * now symmetry in E.
      * tauto.
Qed.

Definition Injective {A B} (f : A->B) :=
 forall x y, f x = f y -> x = y.

Lemma inductive_count (S:eqType) (Y:eqType) A (s:S) n (f: S -> Y):
Injective f -> count A s = n -> count (map (fun a:S => f a) A) (f s) = n.
Proof.
intros inj. revert n. induction A; intros n HC.
- destruct n; try discriminate HC. reflexivity.
- simpl in *. decide (s=a). rewrite e in *. destruct n. discriminate HC. inversion HC.
  decide (f a = f a); try contradiction. rewrite (IHA n H0). now rewrite H0.
  decide (f s = f a). apply inj in e. contradiction. now apply IHA.
Qed.

Lemma diff_constructors_count_zero (F X Y:eqType) (A: list F) (f: F -> X) (g: Y -> X) x:
(forall a b, f a <> g b) -> count (map (fun (a:F) => f a) A) (g x) = 0.
Proof.
intros dis. induction A. auto. cbn. decide (g x = f a).
exfalso. apply (dis a x). symmetry. assumption. assumption.
Qed.

Lemma in_count_app (X:eqType) (A B: list X) a:
  count (A++B) a = count A a + count B a.
Proof.
  revert B a. induction A; intros B b; cbn. auto.
  decide (b = a); rewrite IHA; now cbn.
Qed.

Section fix_X.
  Variable X:Type.
  Implicit Types (A B: list X) (a b c: X).

  Lemma last_app_eq A B a b :
    A++[a] = B++[b] -> A = B /\ a = b.
  Proof.
    intros H%(f_equal (@rev X)). rewrite !rev_app_distr in H. split.
    - inv H. apply (f_equal (@rev X)) in H2. now rewrite !rev_involutive in H2.
    - now inv H.
  Qed.

  Lemma rev_eq A B:
    List.rev A = List.rev B <-> A = B.
  Proof.
    split.
    - intros H%(f_equal (@rev X)). now rewrite !rev_involutive in H.
    - now intros <-.
  Qed.

  Lemma rev_nil A:
    rev A = [] -> A = [].
  Proof.
    destruct A. auto. now intros H%symmetry%app_cons_not_nil.
  Qed.

  Lemma map_inj (Y:Type) A B (f: X -> Y) :
    Injective f -> map f A = map f B <-> A = B.
  Proof.
    intros inj. split.
    - revert B. induction A; intros B H; cbn in *; destruct B; auto; cbn in H; inv H.
      rewrite (inj a x H1). specialize (IHA B H2). now subst.
    - now intros <-.
  Qed.
End fix_X.