pigeon.mlw 1.88 KB
Newer Older
1

2
(** {1 Pigeon hole principle} *)
3

4
module Pigeonhole
5

6 7
  use int.Int
  use map.Map
8

9
  let rec lemma pigeonhole (n m: int) (f: int -> int)
10 11 12
    requires { 0 <= m < n }
    requires { forall i. 0 <= i < n -> 0 <= f i < m }
    ensures  { exists i1, i2. 0 <= i1 < i2 < n /\ f i1 = f i2 }
13 14 15 16 17 18 19 20
    variant  { m }
  = for i = 0 to n - 1 do
      invariant { forall k. 0 <= k < i -> f k < m - 1 }
      if f i = m - 1 then begin
        for j = i + 1 to n - 1 do
          invariant { forall k. i < k < j -> f k < m - 1 }
          if f j = m - 1 then return
        done;
21
        let function g k = if k < i then f k else f (k + 1) in
22 23 24 25
        pigeonhole (n - 1) (m - 1) g;
        return end
    done;
    pigeonhole n (m - 1) f
26 27 28 29 30 31 32 33 34

end

(* An instance where a list is included into a set with fewer elements.

   Contributed by Yuto Takei (University of Tokyo) *)

module ListAndSet

35 36 37 38
  use int.Int
  use list.List
  use list.Length
  use list.Append
39
  use list.Mem as Mem
40
  use set.Fset
41 42 43 44 45 46 47 48 49 50

  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)))

51 52
  clone set.FsetInduction as FSI with
    type t = t, predicate p = pigeon_set
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80

  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