The goal of this lecture is to formalize more informal proofs, this time about discrete mathematics (property of sums) and linear algebra (2x2 matrices).
Prove as many properties as time permits in the .v file about formalizing summations.
In the resource file about formalizing summations, Sigma is defined recursively. Define a tail-recursive version of it that uses an accumulator and prove the equivalence of these two implementations.
The goal of this exercise is to formalize 2-by-2 matrices, based on Section 5 of the accompanying informal lecture note:
Inductive m22 : Type := M22 : nat -> nat -> nat -> nat -> m22.
The idea is evaluating M22 x11 x12 x21 x22 yields a representation of the following 2-by-2 matrix of natural numbers:
+- -+
| x11 x12 |
| |
| x21 x22 |
+- -+
Subsidiary but fun point, time permitting: characterize the result of adding F^(n+1) and F^n, for any natural number n, where X^y denotes exponentiating the matrix X with the natural number y.
The goal of this exercise is to go from matrices of natural numbers to matrices of matrices of natural numbers:
Inductive mm22 : Type := MM22 : m22 -> m22 -> m22 -> m22 -> mm22.
implement addition, multiplication, and exponentiation
what do you make of the following matrix as you exponentiate it:
+- -+
| F^0 F^1 |
| |
| F^1 F^2 |
+- -+
where again X^y denotes exponentiating the matrix X with the natural number y and F is from Definition 25.