From Undecidability.Shared.Libs.PSL Require Export Base.
From Undecidability.Shared.Libs.PSL Require Import FinTypesDef.


Ltac dec := repeat (destruct Dec).

Ltac listComplete := intros x; simpl; dec; destruct x; try congruence.
Ltac deq x := destruct (Dec (x=x)) as [[] | isnotequal]; [> | contradict isnotequal; reflexivity] .

Fixpoint prodLists {X Y: Type} (A: list X) (B: list Y) {struct A} :=
  match A with
  | nil nil
  | cons x A' map ( y (x,y)) B prodLists A' B end.

Lemma prod_nil (X Y: Type) (A: list X) :
  prodLists A ([]: list Y) = [].
Proof.
  induction A.
  - reflexivity.
  - cbn. assumption.
Qed.



Definition toOptionList {X: Type} (A: list X) :=
  None :: map (@Some _) A .

Definition {X: Type} (Y: Type) (A: list X): list (X + Y) :=
  map inl A.
Definition {Y: Type} (X: Type) (A: list Y): list (X + Y) :=
  map inr A.



Lemma countMap (X Y: eqType) (x:X) (B: list Y) y :
  count ( map ( y (x,y)) B) (x, y) = count B y.
Proof.
  induction B.
  - reflexivity.
  - simpl. dec; congruence.
Qed.



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 countMapZero (X Y: eqType) (x x':X) (B: list Y) y : x' x count ( map ( y (x,y)) B) (x', y) =0.
Proof.
  intros ineq. induction B.
  - reflexivity.
  - simpl. dec.
     + inversion e; congruence.
     + exact IHB.
Qed.


Lemma notInZero (X: eqType) (x: X) A :
  not (x 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. .
    + intros H [E | E].
      * now symmetry in E.
      * tauto.
Qed.


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


Lemma InCount (X:eqType) (x:X) A:
  x A count A x > 0.
Proof.
  induction A.
  - intros [].
  - intros [[] | E]; cbn.
    + deq a. .
    + specialize (IHA E). dec; .
Qed.


Lemma count_in_equiv (X: eqType) (x:X) A : count A x > 0 x A.
Proof.
  split.
  - apply countIn.
  - apply InCount.
Qed.


Lemma countApp (X: eqType) (x: X) (A B: list X) :
  count (A x::B) x > 0.
Proof.
  auto using InCount.
Qed.


Lemma dupfreeCount (X: eqType) (x:X) (A: list X) : dupfree A x A count A x = 1.
Proof.
  intros D E. induction D.
  - contradiction E.
  - cbn. dec.
    + f_equal. subst . now apply notInZero.
    + destruct E as [E | E]; [> congruence | auto].
Qed.


Lemma toSumList1_count (X: eqType) (x: X) (Y: eqType) (A: list X) :
  count ( Y A) (inl x) = count A x .
Proof.
  induction A; simpl; dec; congruence.
Qed.


Lemma toSumList2_count (X Y: eqType) (y: Y) (A: list Y):
  count ( X A) (inr y) = count A y.
Proof.
  induction A; simpl; dec; congruence.
Qed.


Lemma toSumList1_missing (X Y: eqType) (y: Y) (A: list X):
  count ( Y A ) (inr y) = 0.
Proof.
  induction A; dec; firstorder.
Qed.


Lemma toSumList2_missing (X Y: eqType) (x: X) (A: list Y):
  count ( X A ) (inl x) = 0.
Proof.
  induction A; dec; firstorder.
Qed.


Lemma cons_incll (X: Type) (A B: list X) (x:X) : x::A B A B.
Proof.
  unfold "<<=". auto.
Qed.


Lemma card_length_leq (X: eqType) (A: list X) : card A length A.
Proof.
  induction A; auto. cbn. dec; .
Qed.



Lemma appendNil (X: Type) (A B: list X) :
  A B = nil A = nil B = nil.
Proof.
  intros H. assert (|A B| = 0) by now rewrite H.
  rewrite app_length in . rewrite !length_zero_iff_nil. .
Qed.


Lemma countZero (X: eqType) (x: X) (A: list X) : count A x = 0 not (x A).
Proof.
  induction A; cbn in *; dec; firstorder congruence.
Qed.


Lemma NullMul a b : a > 0 b > 0 a * b > 0.
Proof.
  induction 1; cbn; .
Qed.