# Coq Theorem Prover

# My Journey to Understanding Proofs better by Learning the Model of a Theorem Prover: Coq

# Plan of Attack

- Understand a proof with natural numbers with Coq.
- Understand a proof with vectors.
- Understand a proof with Qubits.
- Going further with software foundations?

## More basics with Natural Numbers

### Aside: Lambda cube

## The point: To be able to do exercises from "Quantum Mechanics: The Theoretical Minimum"

**Exercise 1.1: a) Using the axioms for inner products, prove {⟨A| + ⟨B|} |C⟩ = ⟨A|C⟩ + ⟨B|C⟩. **

First example of a vector proof. For this simple case I'll likely find many examples off the shelf.

**b) Prove ⟨A|A⟩ is a real number.**

I think this is defined by the complex conjugate of A_dagger dot A. Since the complex conjugate just negates the i component.

Dot product is (I'll need to learn how to put latex here as well)

Exercise 1.2: Show that the inner product defined by Eq. 1.2 satisfies all the axioms of inner products.

B|A = β∗ 1 β∗ 2 β∗ 3 β∗ 4 β∗ 5 ⎛ ⎜⎜⎜⎜⎝ α1 α2 α3 α4 α5 ⎞ ⎟⎟⎟⎟⎠ = β∗ 1α1 + β∗ 2α2 + β∗ 3α3 + β∗ 4α4 + β∗ 5α5. (1.2)

Exercise 2.1: Prove that the vector |r in Eq. 2.5 is orthogonal to vector |l in Eq. 2.6.

|r = 1 √2 |u + 1 √2 |d. (2.5)

|l = 1 √2 |u − 1 √2 |d. (2.6)