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 (fun 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 toSumList1 {X: Type} (Y: Type) (A: list X): list (X + Y) :=
  map inl A.
Definition toSumList2 {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 (fun 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 (fun 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 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. lia.
    + intros H [E | E].
      * now symmetry in E.
      * tauto.
Qed.

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

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

Lemma count_in_equiv (X: eqType) (x:X) A : count A x > 0 <-> x el 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 el A -> count A x = 1.
Proof.
  intros D E. induction D.
  - contradiction E.
  - cbn. dec.
    + f_equal. subst x0. now apply notInZero.
    + destruct E as [E | E]; [> congruence | auto].
Qed.

Lemma toSumList1_count (X: eqType) (x: X) (Y: eqType) (A: list X) :
  count (toSumList1 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 (toSumList2 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 (toSumList1 Y A ) (inr y) = 0.
Proof.
  induction A; dec; firstorder.
Qed.

Lemma toSumList2_missing (X Y: eqType) (x: X) (A: list Y):
  count (toSumList2 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; lia.
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 H0. rewrite <- !length_zero_iff_nil. lia.
Qed.

Lemma countZero (X: eqType) (x: X) (A: list X) : count A x = 0 -> not (x el 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; lia.
Qed.