Copyright	(c) Levent Erkok
License	BSD3
Maintainer	erkokl@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

Documentation.SBV.Examples.TP.PigeonHole

Description

Proves the pigeon-hole principle. If a list of integers sum to more than the length of the list itself, then some cell must contain a value larger than 1.

Synopsis

overflow :: SList Integer -> SBool
pigeonHole :: TP (Proof (Forall "xs" [Integer] -> SBool))

Documentation

overflow :: SList Integer -> SBool Source #

Overflow: Some value is greater than 1.

pigeonHole :: TP (Proof (Forall "xs" [Integer] -> SBool)) Source #

\(\sum xs > \lvert xs \rvert \Rightarrow \textrm{overflow}\, xs\)

>>> runTP pigeonHole
Inductive lemma: pigeonHole
  Step: Base                   Q.E.D.
  Step: 1                      Q.E.D.
  Step: 2                      Q.E.D.
  Result:                      Q.E.D.
Functions proven terminating: sbv.foldr
[Proven] pigeonHole :: Ɐxs ∷ [Integer] → Bool