%
%
% Purpose : the pigeonhole principle 
%
%

pigeonhole[T: TYPE]: THEORY

BEGIN

  A, A1, A2, B, C, S, S1, S2, S3: VAR finite_set[T]
  x: VAR T
  n: VAR nat  

  pigeonhole: THEOREM
      card(A) + card(B) > card(union(A, B)) 
    IMPLIES
      EXISTS x: A(x) AND B(x)

  card_difference_alt: LEMMA
    card(difference(S, C)) <= n IFF card(intersection(S, C)) >= card(S) - n

  pigeonhole_difference: THEOREM
      subset?(A, S) AND
      card(A) > n AND
      card(difference(S, B)) <= n
    IMPLIES
      EXISTS x: A(x) AND B(x)

  majority_subset?(A, S): bool = 
    2 * card(A) > card(S) AND subset?(A, S)

  simple_majority?(A, S): bool = 
    2 * card(intersection(A, S)) > card(S)

  simple_majority_subset: LEMMA
    simple_majority?(A, S) IFF majority_subset?(intersection(A, S), S)

  majority_subset_nonempty: LEMMA
      majority_subset?(A, S) 
    IMPLIES 
      NOT empty?(S)

  simple_majority_nonempty: LEMMA
      simple_majority?(A, S)
    IMPLIES
      NOT empty?(S)

  majority_nonempty: LEMMA
      majority_subset?(A, S) 
    IMPLIES 
      NOT empty?(A)

  majority_pigeonhole: THEOREM
      2 * card(A) > card(S) AND 
      subset?(A, S) AND
      2 * card(B) >= card(S) AND 
      subset?(B, S) 
    IMPLIES
      EXISTS x: A(x) AND B(x)

  simple_majority_pigeonhole: THEOREM
      simple_majority?(A, S) AND 
      simple_majority?(B, S)
    IMPLIES
      EXISTS x: A(x) AND B(x)

  median_pigeonhole: LEMMA
      majority_subset?(A, S1) AND
      majority_subset?(B, S2) AND
      card(union(S1, S2)) - card(intersection(S1, S2)) <= 1
    IMPLIES
      EXISTS x: A(x) AND B(x)

  two_thirds_majority_subset?(A, S): bool = 
    3 * card(A) >= 2 * card(S) AND 
    subset?(A, S) 

  intersection_majority?(S1, S2): bool =
    2 * card(intersection(S1, S2)) > card(union(S1, S2))

  intersection_nonempty: LEMMA
     intersection_majority?(S1, S2) IMPLIES not empty?(S1)

  intersection_majority?(S1, S2, S3): bool = 
    2 * card(intersection(S1, S2)) > card(S3)

  byzantine_intersection_majority?(S1, S2, S3): bool =
    2 * card(intersection(S1, intersection(S2, S3))) >
      card(union(S1, S2)) + card(difference(S2, S3))


  two_thirds_overlap_pigeonhole: LEMMA
      two_thirds_majority_subset?(A, S1) AND
      two_thirds_majority_subset?(B, S2) AND
      intersection_majority?(S1, S2)
    IMPLIES
      EXISTS x: A(x) AND B(x)


  IMPORTING tau_declaration

  t: VAR tau_type
  e: VAR non_empty_finite_set[T]
  s, s1, s2: VAR finite_set[T]

  quorum?(s1, t)(s2): bool = 
    NOT empty?(s1) AND card(difference(s1, s2)) <= t(card(s1))

  quorum_exists?(s, t): bool = 
    EXISTS s1: quorum?(s, t)(s1)


  % Cardinality of a tau-reduced multi-set
  M(e, t): posnat = card(e) - 2 * t(card(e))

  nada_reduce: LEMMA M(e, nada) = card(e)
  mid_reduce: LEMMA M(e, mid) <= 2
  byz_reduce: LEMMA M(e, byz) >= card(e)/3


  

END pigeonhole