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

Documentation.SBV.Examples.TP.SortHelpers

Description

Various definitions and lemmas that are useful for sorting related proofs.

Synopsis

nonDecreasing :: (Ord a, SymVal a) => SList a -> SBool
isPermutation :: SymVal a => SList a -> SList a -> SBool
nonDecrTail :: (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
nonDecrIns :: (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool))
sublist :: SymVal a => SList a -> SList a -> SBool
sublistCorrect :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool))
sublistElem :: (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistTail :: (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool))
sublistIfPerm :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool))

Documentation

nonDecreasing :: (Ord a, SymVal a) => SList a -> SBool Source #

A predicate testing whether a given list is non-decreasing.

isPermutation :: SymVal a => SList a -> SList a -> SBool Source #

Are two lists permutations of each other?

nonDecrTail :: (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) Source #

The tail of a non-decreasing list is non-decreasing. We have:

>>> runTP $ nonDecrTail @Integer
Lemma: nonDecrTail                      Q.E.D.
[Proven] nonDecrTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool

nonDecrIns :: (Ord a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> SBool)) Source #

If we insert an element that is less than the head of a nonDecreasing list, it remains nondecreasing. We have:

>>> runTP $ nonDecrIns @Integer
Lemma: nonDecrInsert                    Q.E.D.
[Proven] nonDecrInsert :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Bool

sublist :: SymVal a => SList a -> SList a -> SBool Source #

Sublist relationship

sublistCorrect :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> Forall "x" a -> SBool)) Source #

sublist correctness. We have:

>>> runTP $ sublistCorrect @Integer
Inductive lemma: countNonNeg
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                         Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Inductive lemma: countElem
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                         Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Inductive lemma: elemCount
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: sublistCorrect
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
[Proven] sublistCorrect :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Ɐx ∷ Integer → Bool

sublistElem :: (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #

If one list is a sublist of another, then its head is an elem. We have:

>>> runTP $ sublistElem @Integer
Inductive lemma: countNonNeg
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                         Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Inductive lemma: countElem
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1.1                         Q.E.D.
    Step: 1.1.2                         Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Inductive lemma: elemCount
  Step: Base                            Q.E.D.
  Step: 1 (2 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2.1                         Q.E.D.
    Step: 1.2.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: sublistCorrect
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
Lemma: sublistElem
  Step: 1                               Q.E.D.
  Result:                               Q.E.D.
[Proven] sublistElem :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool

sublistTail :: (Eq a, SymVal a) => TP (Proof (Forall "x" a -> Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #

If one list is a sublist of another so is its tail. We have:

>>> runTP $ sublistTail @Integer
Lemma: sublistTail                      Q.E.D.
[Proven] sublistTail :: Ɐx ∷ Integer → Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool

sublistIfPerm :: (Eq a, SymVal a) => TP (Proof (Forall "xs" [a] -> Forall "ys" [a] -> SBool)) Source #

Permutation implies sublist. We have:

>>> runTP $ sublistIfPerm @Integer
Lemma: sublistIfPerm                    Q.E.D.
[Proven] sublistIfPerm :: Ɐxs ∷ [Integer] → Ɐys ∷ [Integer] → Bool