From Undecidability.Shared.Libs.PSL Require Export BaseLists Removal.
Section Cardinality.
Variable X : eqType.
Implicit Types A B : list X.
Fixpoint card A :=
match A with
| nil => 0
| x::A => if Dec (x el A) then card A else 1 + card A
end.
Lemma card_cons x A :
x el A -> card (x::A) = card A.
Proof.
intros H. cbn. decide (x el A) as [H1|H1]; tauto.
Qed.
Lemma card_cons' x A :
~ x el A -> card (x::A) = 1 + card A.
Proof.
intros H. cbn. decide (x el A) as [H1|H1]; tauto.
Qed.
Lemma card_in_rem x A :
x el A -> card A = 1 + card (rem A x).
Proof.
intros D.
induction A as [|y A].
- contradiction D.
- decide (y = x) as [->|H].
+ clear D. rewrite rem_fst.
cbn. decide (x el A) as [H1|H1].
* auto.
* now rewrite (rem_id H1).
+ assert (x el A) as H1 by (destruct D; tauto). clear D.
rewrite (rem_fst' _ H). specialize (IHA H1).
simpl card at 2.
decide (y el rem A x) as [H2|H2].
* rewrite card_cons. exact IHA.
apply in_rem_iff in H2. intuition.
* rewrite card_cons'. now rewrite IHA.
contradict H2. now apply in_rem_iff.
Qed.
Lemma card_not_in_rem A x :
~ x el A -> card A = card (rem A x).
Proof.
intros D; rewrite rem_id; auto.
Qed.
Lemma card_le A B :
A <<= B -> card A <= card B.
Proof.
revert B.
induction A as [|x A]; intros B D; cbn.
- lia.
- apply incl_lcons in D as [D D1].
decide (x el A) as [E|E].
+ auto.
+ rewrite (card_in_rem D).
enough (card A <= card (rem B x)) by lia.
apply IHA. auto.
Qed.
Lemma card_eq A B :
A === B -> card A = card B.
Proof.
intros [E F]. apply card_le in E. apply card_le in F. lia.
Qed.
Lemma card_cons_rem x A :
card (x::A) = 1 + card (rem A x).
Proof.
rewrite (card_eq (rem_equi x A)). cbn.
decide (x el rem A x) as [D|D].
- exfalso. apply in_rem_iff in D; tauto.
- reflexivity.
Qed.
Lemma card_0 A :
card A = 0 -> A = nil.
Proof.
destruct A as [|x A]; intros D.
- reflexivity.
- exfalso. rewrite card_cons_rem in D. lia.
Qed.
Lemma card_ex A B :
card A < card B -> exists x, x el B /\ ~ x el A.
Proof.
intros D.
decide (B <<= A) as [E|E].
- exfalso. apply card_le in E. lia.
- apply list_exists_not_incl; auto.
Qed.
Lemma card_equi A B :
A <<= B -> card A = card B -> A === B.
Proof.
revert B.
induction A as [|x A]; cbn; intros B D E.
- symmetry in E. apply card_0 in E. now rewrite E.
- apply incl_lcons in D as [D D1].
decide (x el A) as [F|F].
+ rewrite (IHA B); auto.
+ rewrite (IHA (rem B x)).
* symmetry. apply rem_reorder, D.
* auto.
* apply card_in_rem in D. lia.
Qed.
Lemma card_lt A B x :
A <<= B -> x el B -> ~ x el A -> card A < card B.
Proof.
intros D E F.
decide (card A = card B) as [G|G].
+ exfalso. apply F. apply (card_equi D); auto.
+ apply card_le in D. lia.
Qed.
Lemma card_or A B :
A <<= B -> A === B \/ card A < card B.
Proof.
intros D.
decide (card A = card B) as [F|F].
- left. apply card_equi; auto.
- right. apply card_le in D. lia.
Qed.
End Cardinality.
Instance card_equi_proper (X: eqType) :
Proper (@equi X ==> eq) (@card X).
Proof.
hnf. apply card_eq.
Qed.
Section Cardinality.
Variable X : eqType.
Implicit Types A B : list X.
Fixpoint card A :=
match A with
| nil => 0
| x::A => if Dec (x el A) then card A else 1 + card A
end.
Lemma card_cons x A :
x el A -> card (x::A) = card A.
Proof.
intros H. cbn. decide (x el A) as [H1|H1]; tauto.
Qed.
Lemma card_cons' x A :
~ x el A -> card (x::A) = 1 + card A.
Proof.
intros H. cbn. decide (x el A) as [H1|H1]; tauto.
Qed.
Lemma card_in_rem x A :
x el A -> card A = 1 + card (rem A x).
Proof.
intros D.
induction A as [|y A].
- contradiction D.
- decide (y = x) as [->|H].
+ clear D. rewrite rem_fst.
cbn. decide (x el A) as [H1|H1].
* auto.
* now rewrite (rem_id H1).
+ assert (x el A) as H1 by (destruct D; tauto). clear D.
rewrite (rem_fst' _ H). specialize (IHA H1).
simpl card at 2.
decide (y el rem A x) as [H2|H2].
* rewrite card_cons. exact IHA.
apply in_rem_iff in H2. intuition.
* rewrite card_cons'. now rewrite IHA.
contradict H2. now apply in_rem_iff.
Qed.
Lemma card_not_in_rem A x :
~ x el A -> card A = card (rem A x).
Proof.
intros D; rewrite rem_id; auto.
Qed.
Lemma card_le A B :
A <<= B -> card A <= card B.
Proof.
revert B.
induction A as [|x A]; intros B D; cbn.
- lia.
- apply incl_lcons in D as [D D1].
decide (x el A) as [E|E].
+ auto.
+ rewrite (card_in_rem D).
enough (card A <= card (rem B x)) by lia.
apply IHA. auto.
Qed.
Lemma card_eq A B :
A === B -> card A = card B.
Proof.
intros [E F]. apply card_le in E. apply card_le in F. lia.
Qed.
Lemma card_cons_rem x A :
card (x::A) = 1 + card (rem A x).
Proof.
rewrite (card_eq (rem_equi x A)). cbn.
decide (x el rem A x) as [D|D].
- exfalso. apply in_rem_iff in D; tauto.
- reflexivity.
Qed.
Lemma card_0 A :
card A = 0 -> A = nil.
Proof.
destruct A as [|x A]; intros D.
- reflexivity.
- exfalso. rewrite card_cons_rem in D. lia.
Qed.
Lemma card_ex A B :
card A < card B -> exists x, x el B /\ ~ x el A.
Proof.
intros D.
decide (B <<= A) as [E|E].
- exfalso. apply card_le in E. lia.
- apply list_exists_not_incl; auto.
Qed.
Lemma card_equi A B :
A <<= B -> card A = card B -> A === B.
Proof.
revert B.
induction A as [|x A]; cbn; intros B D E.
- symmetry in E. apply card_0 in E. now rewrite E.
- apply incl_lcons in D as [D D1].
decide (x el A) as [F|F].
+ rewrite (IHA B); auto.
+ rewrite (IHA (rem B x)).
* symmetry. apply rem_reorder, D.
* auto.
* apply card_in_rem in D. lia.
Qed.
Lemma card_lt A B x :
A <<= B -> x el B -> ~ x el A -> card A < card B.
Proof.
intros D E F.
decide (card A = card B) as [G|G].
+ exfalso. apply F. apply (card_equi D); auto.
+ apply card_le in D. lia.
Qed.
Lemma card_or A B :
A <<= B -> A === B \/ card A < card B.
Proof.
intros D.
decide (card A = card B) as [F|F].
- left. apply card_equi; auto.
- right. apply card_le in D. lia.
Qed.
End Cardinality.
Instance card_equi_proper (X: eqType) :
Proper (@equi X ==> eq) (@card X).
Proof.
hnf. apply card_eq.
Qed.