Documentation

Prove that the sequence 1, 3, S_{k-2} + 2 S_{k-1} is always odd.

We have:

>>> oddSequence1
Inductive lemma (strong): oddSequence
  Step: 1 (3 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3.1                         Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.3.3                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] oddSequence

Prove that the sequence 1, 3, 2 S_{k-1} - S_{k-2} generates sequence of odd numbers.

We have:

>>> oddSequence2
Lemma: oddSequence_0                    Q.E.D.
Lemma: oddSequence_1                    Q.E.D.
Inductive lemma (strong): oddSequence_sNp2
  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: oddSequence2
  Step: 1 (3 way case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3.1                         Q.E.D.
    Step: 1.3.2                         Q.E.D.
    Step: 1.Completeness                Q.E.D.
  Result:                               Q.E.D.
[Proven] oddSequence2

For strong induction to work, We have to instantiate the proof at a "smaller" value. This example demonstrates what happens if we don't. We have:

>>> won'tProve1 `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma (strong): lengthGood
  Step: 1
*** Failed to prove lengthGood.1.

*** Solver reported: canceled

Note that strong induction does not need an explicit base case, as the base-cases is folded into the inductive step. Here's an example demonstrating what happens when the failure is only at the base case.

>>> won'tProve2 `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma (strong): badLength
  Step: 1
*** Failed to prove badLength.1.
Falsifiable. Counter-example:
  xs = [] :: [Integer]