Library Cardinality

Copyright (c) 2018 by Swirlds, Inc. Implemented by Karl Crary.

Require Import Nat.
Require Import List.
Require Import Decidable.
Require Import Omega.

Require Import Tact.
Require Import Decide.


Lemma permutation_length :
  forall (T : Type) (p q : list T),
    NoDup p
    -> NoDup q
    -> (forall x, In x p <-> In x q)
    -> length p = length q.

Lemma NoDup_app :
  forall (T : Type) (p q : list T),
    NoDup p
    -> NoDup q
    -> (forall x, In x p -> In x q -> False)
    -> NoDup (p ++ q).
nil
Lemma inclusion_exclusion :
  forall T (p q u : list T),
    (forall (x y : T), decidable (x = y))
    -> NoDup p
    -> NoDup q
    -> NoDup u
    -> List.incl p u
    -> List.incl q u
    -> exists r,
         NoDup r
         /\ List.incl r p
         /\ List.incl r q
         /\ length r >= length p + length q - length u.
nil
Lemma enumerate_subset :
  forall T (P : T -> Prop) (u : list T),
    (forall x, In x u -> decidable (P x))
    -> NoDup u
    -> exists p,
         NoDup p
         /\ forall x, In x p <-> (P x /\ In x u).
nil
Lemma deduplicate :
  forall T (l : list T),
    (forall (x y : T), decidable (x = y))
    -> exists l',
         NoDup l'
         /\ (forall x, In x l <-> In x l').
nil
Definition cardinality {T : Type} (P : T -> Prop) (n : nat) : Prop
  :=
  exists l,
    NoDup l
    /\ (forall x, P x <-> In x l)
    /\ length l = n.

Lemma cardinality_empty :
  forall T, cardinality (fun (x : T) => False) 0.

Lemma cardinality_singleton :
  forall (T : Type) (x : T),
    cardinality (fun y => y = x) 1.

Lemma cardinality_In :
  forall (T : Type) (l : list T),
    NoDup l
    -> cardinality (fun x => In x l) (length l).

Lemma cardinality_fun :
  forall (T : Type) (P : T -> Prop) n n',
    cardinality P n
    -> cardinality P n'
    -> n = n'.

Lemma cardinality_iff :
  forall (T : Type) (P Q : T -> Prop) n,
    (forall x, P x <-> Q x)
    -> cardinality P n
    -> cardinality Q n.

Lemma cardinality_empty' :
  forall T (P : T -> Prop),
    (forall x, ~ P x)
    -> cardinality P 0.
Lemma cardinality_nonempty :
  forall T (P : T -> Prop) p,
    cardinality P p
    -> p > 0
    -> exists x, P x.

Lemma cardinality_subset :
  forall (T : Type) (P Q : T -> Prop) n,
    (forall x, Q x -> decidable (P x))
    -> incl P Q
    -> cardinality Q n
    -> exists m,
         cardinality P m
         /\ m <= n.

Lemma pigeonhole :
  forall S T (P : S -> Prop) (Q : T -> Prop) (f : S -> T) l m n,
    (forall (x y : T), decidable (x = y))
    -> (forall x, P x -> Q (f x))
    -> cardinality P l
    -> cardinality Q m
    -> l > m * n
    -> exists y n',
         Q y
         /\ cardinality (fun x => P x /\ f x = y) n'
         /\ n' > n.
nil
Lemma cardinality_sum :
  forall T (A B : T -> Prop) a b,
    cardinality A a
    -> cardinality B b
    -> (forall x, A x -> B x -> False)
    -> cardinality (fun x => A x \/ B x) (a + b).

Lemma cardinality_partition :
  forall T (A B U : T -> Prop) a b,
    incl A U
    -> incl B U
    -> cardinality U (a + b)
    -> cardinality A a
    -> cardinality B b
    -> (forall x, A x -> B x -> False)
    -> forall x, U x -> A x \/ B x.

Lemma cardinality_difference :
  forall T (A B : T -> Prop) a b,
    (forall (x y : T), decidable (x = y))
    -> cardinality A a
    -> cardinality B b
    -> a < b
    -> exists x, ~ A x /\ B x.
nil
Lemma cardinality_corr_le :
  forall S T (P : S -> Prop) (Q : T -> Prop) (R : S -> T -> Prop) p q,
    (forall x x' y, P x -> P x' -> Q y -> R x y -> R x' y -> x = x')
    -> (forall x, P x -> exists y, R x y /\ Q y)
    -> cardinality P p
    -> cardinality Q q
    -> p <= q.
nil
Lemma cardinality_corr_eq :
  forall S T (P : S -> Prop) (Q : T -> Prop) (R : S -> T -> Prop) p q,
    (forall x x' y, P x -> P x' -> Q y -> R x y -> R x' y -> x = x')
    -> (forall x y y', P x -> Q y -> Q y' -> R x y -> R x y' -> y = y')
    -> (forall x, P x -> exists y, R x y /\ Q y)
    -> (forall y, Q y -> exists x, R x y /\ P x)
    -> cardinality P p
    -> cardinality Q q
    -> p = q.

Lemma cardinality_map_inj :
  forall S T (P : S -> Prop) (Q : T -> Prop) (f : S -> T) p q,
    (forall x, P x -> Q (f x))
    -> (forall x y, P x -> P y -> f x = f y -> x = y)
    -> cardinality P p
    -> cardinality Q q
    -> p <= q.

Lemma cardinality_map_surj :
  forall S T (P : S -> Prop) (Q : T -> Prop) (f : T -> S) p q,
    (forall x, Q x -> P (f x))
    -> (forall x, P x -> exists y, Q y /\ x = f y)
    -> cardinality P p
    -> cardinality Q q
    -> p <= q.

Lemma cardinality_incl :
  forall T (P Q : T -> Prop) p q,
    incl P Q
    -> cardinality P p
    -> cardinality Q q
    -> p <= q.

Lemma cardinality_image :
  forall S T (P : S -> Prop) (f : S -> T) n,
    (forall x y, P x -> P y -> f x = f y -> x = y)
    -> cardinality P n
    -> cardinality (fun x => exists y, x = f y /\ P y) n.
nil
cons

Lemma cardinality_tabulate :
  forall (S T : Type) (P : S -> Prop) (Q : S -> T -> Prop) l m,
    cardinality P l
    -> (forall x, P x -> exists m', cardinality (Q x) m' /\ m <= m')
    -> exists n,
         cardinality (fun xy => P (fst xy) /\ Q (fst xy) (snd xy)) n
         /\ l * m <= n.
nil
Lemma cardinality_finite :
  forall T (P : T -> Prop) n, cardinality P n -> finite P.

Lemma finite_cardinality :
  forall T (P : T -> Prop),
    (forall (x y : T), decidable (x = y))
    -> finite P
    -> exists i, cardinality P i.

Lemma cardinality_gt_decide :
  forall (T : Type) (P U : T -> Prop) n n',
    (forall x, decidable (P x))
    -> incl P U
    -> cardinality U n
    -> decidable (exists p, cardinality P p /\ p > n').

Definition cardinality_lt {T : Type} (P : T -> Prop) (n : nat) : Prop
  :=
  ~ exists l,
      NoDup l
      /\ (forall x, In x l -> P x)
      /\ length l >= n.

Lemma cardinality_impl_cardinality_lt :
  forall T (P : T -> Prop) m n,
    m < n
    -> cardinality P m
    -> cardinality_lt P n.

Lemma cardinality_lt_increase :
  forall T (P : T -> Prop) m n,
    m <= n
    -> cardinality_lt P m
    -> cardinality_lt P n.

Lemma cardinality_lt_impl_lt :
  forall T (P Q : T -> Prop) p q,
    incl P Q
    -> cardinality P p
    -> cardinality_lt Q q
    -> p < q.

Lemma cardinality_lt_by_contradiction :
  forall T (P : T -> Prop) p,
    (forall Q q, incl Q P -> cardinality Q q -> q >= p -> False)
    -> cardinality_lt P p.