sbv-13.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.TP.Peano

Description

Modeling Peano arithmetic in SBV and proving various properties using TP. Most of the properties we prove come from https://en.wikipedia.org/wiki/Peano_axioms.

Synopsis

Documentation

data Nat Source #

Natural numbers. (If you are looking at the haddock documents, note the plethora of definitions the call to mkSymbolic generates. You can mostly ignore these, except for the case analyzer, the testers and accessors.)

Constructors

Zero 
Succ 

Fields

Instances

Instances details
Arbitrary Nat Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

arbitrary :: Gen Nat #

shrink :: Nat -> [Nat] #

Num Nat Source #

Numeric instance. Choices: We clamp everything at Zero. Negation is identity.

Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

(+) :: Nat -> Nat -> Nat #

(-) :: Nat -> Nat -> Nat #

(*) :: Nat -> Nat -> Nat #

negate :: Nat -> Nat #

abs :: Nat -> Nat #

signum :: Nat -> Nat #

fromInteger :: Integer -> Nat #

Num SNat Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

(+) :: SNat -> SNat -> SNat #

(-) :: SNat -> SNat -> SNat #

(*) :: SNat -> SNat -> SNat #

negate :: SNat -> SNat #

abs :: SNat -> SNat #

signum :: SNat -> SNat #

fromInteger :: Integer -> SNat #

SymVal Nat Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

mkSymVal :: MonadSymbolic m => VarContext -> Maybe String -> m (SBV Nat) Source #

mkSymValInit :: State -> SBV Nat -> IO () Source #

literal :: Nat -> SBV Nat Source #

fromCV :: CV -> Nat Source #

isConcretely :: SBV Nat -> (Nat -> Bool) -> Bool Source #

minMaxBound :: Maybe (Nat, Nat) Source #

free :: MonadSymbolic m => String -> m (SBV Nat) Source #

free_ :: MonadSymbolic m => m (SBV Nat) Source #

mkFreeVars :: MonadSymbolic m => Int -> m [SBV Nat] Source #

symbolic :: MonadSymbolic m => String -> m (SBV Nat) Source #

symbolics :: MonadSymbolic m => [String] -> m [SBV Nat] Source #

unliteral :: SBV Nat -> Maybe Nat Source #

unlitCV :: SBV Nat -> Maybe (Kind, CVal) Source #

isConcrete :: SBV Nat -> Bool Source #

isSymbolic :: SBV Nat -> Bool Source #

HasKind Nat Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

kindOf :: Nat -> Kind Source #

hasSign :: Nat -> Bool Source #

intSizeOf :: Nat -> Int Source #

isBoolean :: Nat -> Bool Source #

isBounded :: Nat -> Bool Source #

isReal :: Nat -> Bool Source #

isFloat :: Nat -> Bool Source #

isDouble :: Nat -> Bool Source #

isRational :: Nat -> Bool Source #

isFP :: Nat -> Bool Source #

isUnbounded :: Nat -> Bool Source #

isADT :: Nat -> Bool Source #

isChar :: Nat -> Bool Source #

isString :: Nat -> Bool Source #

isList :: Nat -> Bool Source #

isSet :: Nat -> Bool Source #

isTuple :: Nat -> Bool Source #

isArray :: Nat -> Bool Source #

isRoundingMode :: Nat -> Bool Source #

isUninterpreted :: Nat -> Bool Source #

showType :: Nat -> String Source #

OrdSymbolic SNat Source #

Symbolic ordering. We only define less-than, other methods use the defaults.

Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

(.<) :: SNat -> SNat -> SBool Source #

(.<=) :: SNat -> SNat -> SBool Source #

(.>) :: SNat -> SNat -> SBool Source #

(.>=) :: SNat -> SNat -> SBool Source #

smin :: SNat -> SNat -> SNat Source #

smax :: SNat -> SNat -> SNat Source #

inRange :: SNat -> (SNat, SNat) -> SBool Source #

HasInductionSchema (Forall ta Nat -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

inductionSchema :: (Forall ta Nat -> SBool) -> ProofObj Source #

SymVal extraT => HasInductionSchema (Forall ta Nat -> Forall extraS extraT -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

inductionSchema :: (Forall ta Nat -> Forall extraS extraT -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2) => HasInductionSchema (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

inductionSchema :: (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3) => HasInductionSchema (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

inductionSchema :: (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4) => HasInductionSchema (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

inductionSchema :: (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> SBool) -> ProofObj Source #

(SymVal extraT1, SymVal extraT2, SymVal extraT3, SymVal extraT4, SymVal extraT5) => HasInductionSchema (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) Source # 
Instance details

Defined in Documentation.SBV.Examples.TP.Peano

Methods

inductionSchema :: (Forall ta Nat -> Forall extraS1 extraT1 -> Forall extraS2 extraT2 -> Forall extraS3 extraT3 -> Forall extraS4 extraT4 -> Forall extraS5 extraT5 -> SBool) -> ProofObj Source #

cv2Nat :: String -> [CV] -> Nat Source #

Conversion from SMT values to Nat values.

_undefiner_Nat :: a Source #

Autogenerated definition to avoid unused-variable warnings from GHC.

type SNat = SBV Nat Source #

Symbolic version of the type Nat.

sZero :: SBV Nat Source #

Symbolic version of the constructor Zero.

sSucc :: SBV Nat -> SBV Nat Source #

Symbolic version of the constructor Succ.

isZero :: SBV Nat -> SBool Source #

Field recognizer predicate.

isSucc :: SBV Nat -> SBool Source #

Field recognizer predicate.

getSucc_1 :: SBV Nat -> SBV Nat Source #

Field accessor function.

sprev :: SBV Nat -> SBV Nat Source #

Field accessor function.

sCaseNat :: Mergeable result => SBV Nat -> result -> (SBV Nat -> result) -> result Source #

Case analyzer for the type Nat.

Conversion to and from integers

n2i :: SNat -> SInteger Source #

Convert from Nat to Integer.

NB. When writing the properties below, we use the notation \(\overline{n}\) to mean n2i n.

i2n :: SInteger -> SNat Source #

Convert Non-negative integers to Nat. Negative numbers become Zero.

NB. When writing the properties below, we use the notation \(\underline{i}\) to mean i2n i.

n2iNonNeg :: TP (Proof (Forall "n" Nat -> SBool)) Source #

\(\overline{n} \geq 0\)

>>> runTP n2iNonNeg
Lemma: n2iNonNeg                        Q.E.D.
[Proven] n2iNonNeg :: Ɐn ∷ Nat → Bool

i2n2i :: TP (Proof (Forall "i" Integer -> SBool)) Source #

\(\overline{\underline{i}} = \max(i, 0)\).

>>> runTP i2n2i
Lemma: i2n2i                            Q.E.D.
[Proven] i2n2i :: Ɐi ∷ Integer → Bool

n2i2n :: TP (Proof (Forall "n" Nat -> SBool)) Source #

\(\underline{\overline{n}} = n\)

>>> runTP n2i2n
Lemma: n2i2n                            Q.E.D.
[Proven] n2i2n :: Ɐn ∷ Nat → Bool

n2iAdd :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(\overline{m + n} = \overline{m} + \overline{n}\)

>>> runTP n2iAdd
Lemma: n2iAdd                           Q.E.D.
[Proven] n2iAdd :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Addition

Correctness

addCorrect :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(\overline{m + n} = \overline{m} + \overline{n}\)

>>> runTP addCorrect
Lemma: addCorrect                       Q.E.D.
[Proven] addCorrect :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Left and right unit

addLeftUnit :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(0 + m = m\)

>>> runTP addLeftUnit
Lemma: addLeftUnit                      Q.E.D.
[Proven] addLeftUnit :: Ɐm ∷ Nat → Bool

addRightUnit :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(m + 0 = m\)

>>> runTP addRightUnit
Lemma: addRightUnit                     Q.E.D.
[Proven] addRightUnit :: Ɐm ∷ Nat → Bool

Addition with non-zero values

addSucc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m + \mathrm{Succ}\,n = \mathrm{Succ}\,(m + n)\)

>>> runTP addSucc
Lemma: caseZero                         Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
Lemma: addSucc                          Q.E.D.
[Proven] addSucc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Associativity

addAssoc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\(m + (n + o) = (m + n) + o\)

>>> runTP addAssoc
Lemma: addAssoc                         Q.E.D.
[Proven] addAssoc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

Commutativity

addComm :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m + n = n + m\)

>>> runTP addComm
Lemma: addLeftUnit                      Q.E.D.
Lemma: addRightUnit                     Q.E.D.
Lemma: caseZero                         Q.E.D.
Lemma: addSucc                          Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
Lemma: addComm                          Q.E.D.
[Proven] addComm :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Multiplication

Correctness

mulCorrect :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(\overline{m * n} = \overline{m} * \overline{n}\)

>>> runTP mulCorrect
Lemma: caseZero                         Q.E.D.
Lemma: addCorrect                       Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Result:                               Q.E.D.
Lemma: mullCorrect                      Q.E.D.
[Proven] mullCorrect :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Left and right absorption

mulLeftAbsorb :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(0 * m = 0\)

>>> runTP mulLeftAbsorb
Lemma: mulLeftAbsorb                    Q.E.D.
[Proven] mulLeftAbsorb :: Ɐm ∷ Nat → Bool

mulRightAbsorb :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(m * 0 = 0\)

>>> runTP mulRightAbsorb
Lemma: mulRightAbsorb                   Q.E.D.
[Proven] mulRightAbsorb :: Ɐm ∷ Nat → Bool

Left and right unit

mulLeftUnit :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(\mathrm{Succ\,0} * m = m\)

>>> runTP mulLeftUnit
Lemma: mulLeftUnit                      Q.E.D.
[Proven] mulLeftUnit :: Ɐm ∷ Nat → Bool

mulRightUnit :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(m * \mathrm{Succ\,0} = m\)

>>> runTP mulRightUnit
Lemma: mulRightUnit                     Q.E.D.
[Proven] mulRightUnit :: Ɐm ∷ Nat → Bool

Distribution over addition

distribLeft :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\(m * (n + o) = m * n + m * o\)

>>> runTP distribLeft
Lemma: caseZero                         Q.E.D.
Lemma: addAssoc                         Q.E.D.
Lemma: addComm                          Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: 7                               Q.E.D.
  Step: 8                               Q.E.D.
  Step: 9                               Q.E.D.
  Result:                               Q.E.D.
Lemma: distribLeft                      Q.E.D.
[Proven] distribLeft :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

distribRight :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\((m + n) * o = m * o + n * o\)

>>> runTP distribRight
Lemma: caseZero                         Q.E.D.
Lemma: addAssoc                         Q.E.D.
Lemma: addComm                          Q.E.D.
Lemma: addSucc                          Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: 7                               Q.E.D.
  Result:                               Q.E.D.
Lemma: distribRight                     Q.E.D.
[Proven] distribRight :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

Multiplication with non-zero values

mulSucc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m * \mathrm{Succ}\,n = m * n + m\)

>>> runTP mulSucc
Lemma: addLeftUnit                      Q.E.D.
Lemma: distribLeft                      Q.E.D.
Lemma: mulRightUnit                     Q.E.D.
Lemma: addComm                          Q.E.D.
Lemma: mulSucc
  Step: 1                               Q.E.D.
  Step: 2 (defn of +)                   Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Result:                               Q.E.D.
[Proven] mulSucc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Associativity

mulAssoc :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\(m * (n * o) = (m * n) * o\)

>>> runTP mulAssoc
Lemma: caseZero                         Q.E.D.
Lemma: distribRight                     Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Result:                               Q.E.D.
Lemma: mulAssoc                         Q.E.D.
[Proven] mulAssoc :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

Commutativity

mulComm :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m * n = n * m\)

>>> runTP mulComm
Lemma: mulRightAbsorb                   Q.E.D.
Lemma: caseZero                         Q.E.D.
Lemma: mulRightUnit                     Q.E.D.
Lemma: distribLeft                      Q.E.D.
Lemma: caseSucc
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Result:                               Q.E.D.
Lemma: mulComm                          Q.E.D.
[Proven] mulComm :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Ordering

Transitivity of <

ltTrans :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\(m < n \;\wedge\; n < o \;\rightarrow\; m < o\)

>>> runTP ltTrans
Lemma: addAssoc                         Q.E.D.
Lemma: ltTrans
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Result:                               Q.E.D.
[Proven] ltTrans :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

Irreflexivity of <

ltIrreflexive :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(\neg(m < m)\)

>>> runTP ltIrreflexive
Lemma: cancel                           Q.E.D.
Lemma: ltIrreflexive
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] ltIrreflexive :: Ɐm ∷ Nat → Bool

Trichotomy

lteEquiv :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m \geq n = \overline{m} \geq \overline{n}\)

>>> runTP lteEquiv
Lemma: n2iAdd                           Q.E.D.
Lemma: n2iNonNeg                        Q.E.D.
Lemma: n2i2n                            Q.E.D.
Lemma: i2n2i                            Q.E.D.
Lemma: addRightUnit                     Q.E.D.
Lemma: lteEquiv_ltr
  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.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: lteEquiv_rtl
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Step: 7 (2 way case split)
    Step: 7.1                           Q.E.D.
    Step: 7.2.1                         Q.E.D.
    Step: 7.2.2                         Q.E.D.
    Step: 7.2.3                         Q.E.D.
    Step: 7.2.4                         Q.E.D.
    Step: 7.2.5                         Q.E.D.
    Step: 7.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: lteEquiv                         Q.E.D.
[Proven] lteEquiv :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

ordered :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m \geq n \;\lor\; n \geq m\)

>>> runTP ordered
Lemma: lteEquiv                         Q.E.D.
Lemma: ordered
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] ordered :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

trichotomy :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m < n \;\lor\; m = n \;\lor\; n < m\)

>>> runTP trichotomy
Lemma: ordered                          Q.E.D.
Lemma: trichotomy                       Q.E.D.
[Proven] trichotomy :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

Addition and ordering

addOrder :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\(m < n \;\rightarrow\; m + o < n + o\)

>>> runTP addOrder
Lemma: addAssoc                         Q.E.D.
Lemma: addComm                          Q.E.D.
Lemma: addOrder
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Result:                               Q.E.D.
[Proven] addOrder :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

Multiplication and ordering

mulOrder :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> Forall "o" Nat -> SBool)) Source #

\(o > 0 \;\wedge\; m < n \;\rightarrow\; m * o < n * o\)

>>> runTP mulOrder
Lemma: distribRight                     Q.E.D.
Lemma: mulOrder
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: 4                               Q.E.D.
  Step: 5                               Q.E.D.
  Step: 6                               Q.E.D.
  Result:                               Q.E.D.
[Proven] mulOrder :: Ɐm ∷ Nat → Ɐn ∷ Nat → Ɐo ∷ Nat → Bool

Order and sum

orderSum :: TP (Proof (Forall "m" Nat -> Forall "n" Nat -> SBool)) Source #

\(m < n \;\rightarrow\; \exists o.\; m + o = n\)

>>> runTP orderSum
Lemma: orderSum                         Q.E.D.
[Proven] orderSum :: Ɐm ∷ Nat → Ɐn ∷ Nat → Bool

0 and 1 relationship

zeroLtOne :: TP (Proof SBool) Source #

\(0 < 1\)

>>> runTP zeroLtOne
Lemma: zeroLtOne                        Q.E.D.
[Proven] zeroLtOne :: Bool

nothingBetweenZeroAndOne :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(m > 0 \;\rightarrow\; m \geq 1\)

>>> runTP nothingBetweenZeroAndOne
Lemma: nothingBetweenZeroAndOne         Q.E.D.
[Proven] nothingBetweenZeroAndOne :: Ɐm ∷ Nat → Bool

0 is the minimum

minimumElt :: TP (Proof (Forall "m" Nat -> SBool)) Source #

\(m \geq 0\)

>>> runTP minimumElt
Lemma: minimumElt                       Q.E.D.
[Proven] minimumElt :: Ɐm ∷ Nat → Bool

There is no maximum element

noMaximumElt :: TP (Proof (Forall "m" Nat -> Exists "n" Nat -> SBool)) Source #

\(\forall m \;\exists n \;.\; m < n\)

>>> runTP noMaximumElt
Lemma: noMaximumElt                     Q.E.D.
[Proven] noMaximumElt :: Ɐm ∷ Nat → ∃n ∷ Nat → Bool