Overview

The usage documentation explains in general terms how to use the equivalence reasoner. It would be helpful for the reader to additionally have a concrete example that shows the equivalence reasoner in action. We shall provide such an example in the form of a documented Isabelle theory that forms an appendix “Example”. Our documentation shall make use of all the different features of the equivalence reasoner and explicitly point out where it uses them.

The Example

Our example shall be about the asymptotic behavior of sequences of positive reals.

Equivalence relations

Based on the relation ≼ where X ≼ Y ⟷ limsup (X / Y) ≤ 1, we shall define the following equivalences and configure the equivalence reasoner to take them and their inclusion relationships into account:

• Asymptotic equality: ≅ where X ≅ Y ⟷ X ≼ Y ∧ Y ≼ X
• Asymptotic equality up to a constant factor: ≃ where X ≃ Y ⟷ (∃c. X ≼ c * Y) ∧ (∃c. Y ≼ c * X)
• Asymptotic equality up to a polylogarithmic factor: ∼ where X ∼ Y ⟷ (∃k. X ≼ logᵏ * Y) ∧ (∃k. Y ≼ logᵏ * X)

Compatible functions

We shall define the following functions on sequences, which are compatible with the above equivalence relations, and configure the equivalence reasoner to use their compatibility:

• Pointwise addition
• Pointwise multiplication
• Pointwise raising to a constant power

Equivalence lemmas

We shall prove various lemmas that state conditional and unconditional equivalences involving the above equivalence relations and compatible functions. In particular, we shall prove the following propositions:

• log ∼ 1
• inf X Y ≅ X if X ≼ Y

Equivalence theorems

We shall prove several equivalences related to the worst-case time complexities of the following algorithms:

• Certain algorithms for multiplying integers:
  • The Karatsuba algorithm, which runs in Θ (n powr log 2 3) worst-case time
  • The Schönhage–Strassen algorithm, which runs in O (n * log n * log (log n)) worst-case time
  • The Harvey–Hoeven algorithm, which runs in O (n * log n) worst-case time
• The ordinary matrix multiplication algorithm applied of square matrices of integers that have as many bits as the respective matrices have rows and colums

As the complexity of integer multiplication, we directly consider n powr log 2 3, n * log n * log (log n), and n * log n, respectively, while we derive the complexity of matrix multiplication by counting the individual steps of the underlying integer multiplications and additions, taking the size of integers as the complexity of addition.

In our proofs, we shall use the equivalence reasoner, employing the above-mentioned equivalence lemmas as rewrite rules, as well as calculational reasoning.

Concretely, we shall prove the following theorems:

1. The complexities of Schönhage–Strassen and Harvey–Hoeven are in relation ∼.
2. The complexity of Schönhage–Strassen is in relation ∼ with the linear sequence.
3. The complexity of ordinary integer matrix multiplication is in relation ≃ with the complexity of the respective integer multiplication algorithm raised to the power of 3.
4. The complexity of ordinary integer matrix multiplication using Schönhage–Strassen is in relation ∼ with the cube sequence. (The proof should apply Theorem 2 before Theorem 3, so that rewriting is done under stacks of multiple compatible functions.)
5. The complexity of the integer multiplication algorithm that invokes the best algorithm for the respective integer size (out of Karatsuba, Schönhage–Strassen, and Harvey–Hoeven) is in relation ∼ with the linear sequence.