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.