Documentation

Construct a list of size n, containing numbers 1 to n.

>>> up 0
[] :: [SInteger]
>>> up 5
[1,2,3,4,5] :: [SInteger]

Keep consing the first argument on to the accumulator, until we hit zero. After that, return the second argument. Normally, we'd define this as a local function, but the definition needs to be visible for the proofs.

Construct a list of size n, containing numbers n-1 down to 0.

>>> down 0
[] :: [SInteger]
>>> down 5
[5,4,3,2,1] :: [SInteger]

Prove that reverse (down n) is the same as up n

>>> runTP upDown
Lemma: n2iNonNeg                        Q.E.D.
Lemma: revCons                          Q.E.D.
Inductive lemma (strong): upDownGen
  Step: Measure is non-negative         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.2.3                         Q.E.D.
    Step: 1.2.4                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
Lemma: upDown                           Q.E.D.
[Proven] upDown :: Ɐn ∷ Nat → Bool