Why3 Standard Library index



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

Generated by why3doc 0.88.0