Documentation

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

We have:

>>> oddSequence1
Inductive lemma (strong): oddSequence
  Base: oddSequence.Base                Q.E.D.
  Asms: 1                               Q.E.D.
  Step 1: Case split one way:
    Case [1 of 1]: n[1]                 Q.E.D.
    Completeness:                       Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Step: oddSequence.Step                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
  Base: oddSequence_sNp2.Base           Q.E.D.
  Asms: 1                               Q.E.D.
  Step: 1                               Q.E.D.
  Asms: 2                               Q.E.D.
  Step: 2                               Q.E.D.
  Asms: 3                               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: oddSequence_sNp2.Step           Q.E.D.
Lemma: oddSequence
  Asms  : 1                             Q.E.D.
  Step 1: Case split 3 ways:
    Case [1 of 3]: n[1]                 Q.E.D.
    Case [2 of 3]: n[2]                 Q.E.D.
    Case [3 of 3]: n[3]                 Q.E.D.
    Completeness:                       Q.E.D.
  Result:                               Q.E.D.
[Proven] oddSequence

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'tProve `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma (strong): lengthGood
  Base: lengthGood.Base                 Q.E.D.
  Step: 1
*** Failed to prove lengthGood.1.

*** Solver reported: canceled