Embedded Files
My Journey to Understanding Proofs better by Learning the Model of a Theorem Prover: Coq
My Journey to Understanding Proofs better by Learning the Model of a Theorem Prover: Coq
Plan of Attack
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
More basics with Natural Numbers
Aside: Lambda cube
Aside: Lambda cube
The point: To be able to do exercises from "Quantum Mechanics: The Theoretical Minimum"
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.
The dot product of two vectors a = [a1, a2, …, an] and b = [b1, b2, …, bn] is defined as:[1]
Exercise 1.2: Show that the inner product defined by Eq. 1.2 satisfies all the axioms of inner products.
Exercise 2.1: Prove that the vector |r in Eq. 2.5 is orthogonal to vector |l in Eq. 2.6.
Library Coq.Vectors.VectorDef vs. Mathematical Components.
Library Coq.Vectors.VectorDef vs. Mathematical Components.
Google Sites
Report abuse