Formalizing two-by-two matrices

The goal of this chapter is to formalize more informal proofs, this time about linear algebra (2x2 matrices).

Resources

• An decade-old informal lecture note (latest version: 22 Apr 2012).
• The .v file about formalizing two-by-two matrices (latest version: 28 Mar 2025).

Exercise 04

The goal of this exercise is to formalize two-by-two 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 |
+-       -+

1. formalize Definition 9
2. formalize and prove Property 10
3. formalize and prove Property 12
4. formalize Definition 13
5. formalize and prove Proposition 14
6. how does your formalization of Proposition 14 compare with the informal proof of Proposition 14?
7. solve Exercise 25

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.

Exercise 05

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.

1. implement addition, multiplication, and exponentiation

2. 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.

Resources

• An decade-old informal lecture note (latest version: 22 Apr 2012).
• The .v file about formalizing two-by-two matrices (latest version: 28 Mar 2025).

Version

Created by splitting a previous chapter about informal proofs [05 June 2025]