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

We have:

>>> oddSequence1
Inductive lemma (strong): oddSequence1
  Step: Measure is non-negative         Q.E.D.
  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] oddSequence1 :: Ɐn ∷ Integer → Bool

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: Measure is non-negative                   Q.E.D.
  Step: 1                                         Q.E.D.
  Step: 2                                         Q.E.D.
  Step: 3 (simplify)                              Q.E.D.
  Step: 4                                         Q.E.D.
  Step: 5 (simplify)                              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 :: Ɐn ∷ Integer → Bool

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: Measure is non-negative         Q.E.D.
  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: Measure is non-negative         Q.E.D.
  Step: 1
*** Failed to prove badLength.1.
Falsifiable. Counter-example:
  xs = [] :: [Integer]

The measure for strong induction should always produce a non-negative measure. The measure, in general, is an integer, or a tuple of integers, for tuples upto size 5. The ordering is lexicographic. This allows us to do proofs over 5-different arguments where their total measure goes down. If the measure can be negative, then we flag that as a failure, as demonstrated here. We have:

>>> won'tProve3 `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma (strong): badMeasure
  Step: Measure is non-negative
*** Failed to prove badMeasure.Measure is non-negative.
Falsifiable. Counter-example:
  x = -1 :: Integer

The measure must always go down using lexicographic ordering. If not, SBV will flag this as a failure. We have:

>>> won'tProve4 `catch` (\(_ :: SomeException) -> pure ())
Inductive lemma (strong): badMeasure
  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
*** Failed to prove badMeasure.1.2.2.

*** Solver reported: canceled

We prove that summing a list can be done by halving the list, summing parts, and adding the results. The proof uses strong induction. We have:

>>> sumHalves
Inductive lemma: sumAppend
  Step: Base                            Q.E.D.
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Step: 3                               Q.E.D.
  Result:                               Q.E.D.
Inductive lemma (strong): sumHalves
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way full case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2 (2 way full case split)
      Step: 1.2.1                       Q.E.D.
      Step: 1.2.2.1                     Q.E.D.
      Step: 1.2.2.2                     Q.E.D.
      Step: 1.2.2.3                     Q.E.D.
      Step: 1.2.2.4                     Q.E.D.
      Step: 1.2.2.5                     Q.E.D.
      Step: 1.2.2.6 (simplify)          Q.E.D.
  Result:                               Q.E.D.
[Proven] sumHalves :: Ɐxs ∷ [Integer] → Bool