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

We have:

>>> oddSequence1
Inductive lemma (strong): oddSequence
  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] 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: 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

Interleave the elements of two lists. If one ends, we take the rest from the other.

Prove that interleave preserves total length.

The induction here is on the total length of the lists, and hence we use the generalized induction principle. We have:

>>> interleaveLen
Inductive lemma (strong): interleaveLen
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (2 way full 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.
  Result:                               Q.E.D.
[Proven] interleaveLen

Uninterleave the elements of two lists. We roughly split it into two, of alternating elements.

Generalized form of uninterleave with the auxilary lists made explicit.C

The functions uninterleave and interleave are inverses so long as the inputs are of the same length. (The equality would even hold if the first argument has one extra element, but we keep things simple here.)

We have:

>>> interleaveRoundTrip
Lemma: revCons                          Q.E.D.
Inductive lemma (strong): roundTripGen
  Step: Measure is non-negative         Q.E.D.
  Step: 1 (4 way full case split)
    Step: 1.1                           Q.E.D.
    Step: 1.2                           Q.E.D.
    Step: 1.3                           Q.E.D.
    Step: 1.4.1                         Q.E.D.
    Step: 1.4.2                         Q.E.D.
    Step: 1.4.3                         Q.E.D.
    Step: 1.4.4                         Q.E.D.
    Step: 1.4.5                         Q.E.D.
    Step: 1.4.6                         Q.E.D.
    Step: 1.4.7                         Q.E.D.
    Step: 1.4.8                         Q.E.D.
  Result:                               Q.E.D.
Lemma: interleaveRoundTrip
  Step: 1                               Q.E.D.
  Step: 2                               Q.E.D.
  Result:                               Q.E.D.
[Proven] interleaveRoundTrip

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