pigeon.why 1.16 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52

(** {1 Pigeon hole principle}

    Contributed by Yuto Takei (University of Tokyo) *)

theory Pigeonhole

  use import int.Int
  use import list.List
  use import list.Length
  use import list.Append
  use list.Mem
  use import set.Fset

  type t

  predicate pigeon_set (s: set t) =
    forall l: list t.
    (forall e: t. Mem.mem e l -> mem e s) ->
    (length l > cardinal s) ->
    exists e: t, l1 l2 l3: list t.
    l = l1 ++ (Cons e (l2 ++ (Cons e l3)))

  clone set.FsetInduction with type t = t, predicate p = pigeon_set

  lemma corner:
    forall s: set t, l: list t.
    (length l = cardinal s) ->
    (forall e: t. Mem.mem e l -> mem e s) ->
    (exists e: t, l1 l2 l3: list t.
    l = l1 ++ (Cons e (l2 ++ (Cons e l3)))) \/
    (forall e: t. mem e s -> Mem.mem e l)

  lemma pigeon_0:
    pigeon_set empty

  lemma pigeon_1:
    forall s: set t. pigeon_set s ->
    forall t: t. pigeon_set (add t s)

  lemma pigeon_2:
    forall s: set t.
    pigeon_set s

  lemma pigeonhole:
    forall s: set t, l: list t.
    (forall e: t. Mem.mem e l -> mem e s) ->
    (length l > cardinal s) ->
    exists e: t, l1 l2 l3: list t.
    l = l1 ++ (Cons e (l2 ++ (Cons e l3)))

end