Some more doc edits

Matrix.v

@@ -8,9 +8,9 @@ Require Import List.
 (* TODO: Use matrix equality everywhere, declare equivalence relation *)
 (* TODO: Make all nat arguments to matrix lemmas implicit *)
 
-(*******************************************)
-(** Matrix Definitions and Infrastructure **)
-(*******************************************)
+(*********************************************)
+(** * Matrix definitions and infrastructure **)
+(*********************************************)
 
 Declare Scope matrix_scope.
 Delimit Scope matrix_scope with M.
@@ -20,23 +20,21 @@ Local Open Scope nat_scope.
 
 Definition Matrix (m n : nat) := nat -> nat -> C.
 
-(* Definition Vector (n : nat) := Matrix n 1. *)
-
 Definition WF_Matrix {m n: nat} (A : Matrix m n) : Prop := 
   forall x y, x >= m \/ y >= n -> A x y = C0. 
 
 Notation Vector n := (Matrix n 1).
 
 Notation Square n := (Matrix n n).
 
-(* Showing equality via functional extensionality *)
+(** Equality via functional extensionality *)
 Ltac prep_matrix_equality :=
   let x := fresh "x" in 
   let y := fresh "y" in 
   apply functional_extensionality; intros x;
   apply functional_extensionality; intros y.
 
-(* Matrix Equivalence *)
+(** Matrix equivalence *)
 
 Definition mat_equiv {m n : nat} (A B : Matrix m n) : Prop := 
   forall i j, i < m -> j < n -> A i j = B i j.
@@ -62,7 +60,7 @@ Proof.
   + rewrite WFA, WFB; trivial; left; try lia.
 Qed.
 
-(* Printing *)
+(** Printing *)
 
 Parameter print_C : C -> string.
 Fixpoint print_row {m n} i j (A : Matrix m n) : string :=
@@ -78,7 +76,7 @@ Fixpoint print_rows {m n} i j (A : Matrix m n) : string :=
 Definition print_matrix {m n} (A : Matrix m n) : string :=
   print_rows m n A.
 
-(* 2D List Representation *)
+(** 2D list representation *)
 
 Definition list2D_to_matrix (l : list (list C)) : 
   Matrix (length l) (length (hd [] l)) :=
@@ -104,7 +102,7 @@ Proof.
     simpl; lia.
 Qed.
 
-(* Example *)
+(** Example *)
 Definition M23 : Matrix 2 3 :=
   fun x y => 
   match (x, y) with
@@ -130,9 +128,9 @@ Proof.
   do 4 (try destruct x; try destruct y; simpl; trivial).
 Qed.
 
-(*****************************)
-(** Operands and Operations **)
-(*****************************)
+(*******************************)
+(** * Operands and operations **)
+(*******************************)
 
 Definition Zero {m n : nat} : Matrix m n := fun x y => 0%R.
 
@@ -142,7 +140,7 @@ Definition I (n : nat) : Square n :=
 (* Optional coercion to scalar (should be limited to 1 × 1 matrices):
 Definition to_scalar (m n : nat) (A: Matrix m n) : C := A 0 0.
 Coercion to_scalar : Matrix >-> C.
- *)
+*)
 
 (* This isn't used, but is interesting *)
 Definition I__inf := fun x y => if x =? y then C1 else C0.
@@ -180,35 +178,36 @@ Definition inner_product {n} (u v : Vector n) : C :=
 Definition outer_product {n} (u v : Vector n) : Square n := 
   Mmult u (adjoint v).
 
-(* Kronecker of n copies of A *)
+(** Kronecker of n copies of A *)
 Fixpoint kron_n n {m1 m2} (A : Matrix m1 m2) : Matrix (m1^n) (m2^n) :=
   match n with
   | 0    => I 1
   | S n' => kron (kron_n n' A) A
   end.
 
-(* Kronecker product of a list *)
+(** Kronecker product of a list *)
 Fixpoint big_kron {m n} (As : list (Matrix m n)) : 
   Matrix (m^(length As)) (n^(length As)) := 
   match As with
   | [] => I 1
   | A :: As' => kron A (big_kron As')
   end.
 
-(* Product of n copies of A *)
+(** Product of n copies of A *)
 Fixpoint Mmult_n n {m} (A : Square m) : Square m :=
   match n with
   | 0    => I m
   | S n' => Mmult A (Mmult_n n' A)
   end.
 
-(* Indexed sum over matrices *)
+(** Indexed sum over matrices *)
 Fixpoint Msum {m1 m2} n (f : nat -> Matrix m1 m2) : Matrix m1 m2 :=
   match n with
   | 0 => Zero
   | S n' => Mplus (Msum n' f) (f n')
 end.
 
+(** Notations *)
 Infix "∘" := dot (at level 40, left associativity) : matrix_scope.
 Infix ".+" := Mplus (at level 50, left associativity) : matrix_scope.
 Infix ".*" := scale (at level 40, left associativity) : matrix_scope.
@@ -307,9 +306,9 @@ Lemma Mscale_simplify : forall (n m: nat) (a b : Matrix n m) (c d : C),
 Proof. intros; subst; easy. 
 Qed.
 
-(**********************************)
-(** Proofs about Well-Formedness **)
-(**********************************)
+(************************************)
+(** * Proofs about well-formedness **)
+(************************************)
 
 Lemma WF_Matrix_dim_change : forall (m n m' n' : nat) (A : Matrix m n),
   m = m' ->
@@ -382,30 +381,6 @@ Proof.
   assumption.
 Qed. 
 
-
-(* More succinct but sometimes doesn't succeed 
-Lemma WF_kron : forall {m n o p: nat} (A : Matrix m n) (B : Matrix o p), 
-                  WF_Matrix A -> WF_Matrix B -> WF_Matrix (A ⊗ B).
-Proof.
-  unfold WF_Matrix, kron.
-  intros m n o p A B WFA WFB x y H.
-  bdestruct (o =? 0). rewrite WFB; [lca|lia]. 
-  bdestruct (p =? 0). rewrite WFB; [lca|lia].  
-  rewrite WFA.
-  rewrite Cmult_0_l; reflexivity.
-  destruct H.
-  unfold ge in *.
-  left. 
-  apply Nat.div_le_lower_bound; trivial.
-  rewrite Nat.mul_comm.
-  assumption.
-  right.
-  apply Nat.div_le_lower_bound; trivial.
-  rewrite Nat.mul_comm.
-  assumption.
-Qed. 
-*)
-
 Lemma WF_transpose : forall {m n : nat} (A : Matrix m n), 
                      WF_Matrix A -> WF_Matrix A⊤. 
 Proof. unfold WF_Matrix, transpose. intros m n A H x y H0. apply H. 
@@ -475,35 +450,14 @@ Qed.
 
 Local Close Scope nat_scope.
 
-(***************************************)
-(* Tactics for showing well-formedness *)
-(***************************************)
+(****************************************)
+(** Tactics for showing well-formedness *)
+(****************************************)
 
 Local Open Scope nat.
 Local Open Scope R.
 Local Open Scope C.
 
-(*
-Ltac show_wf := 
-  repeat match goal with
-  | [ |- WF_Matrix _ _ (?A × ?B) ]  => apply WF_mult 
-  | [ |- WF_Matrix _ _ (?A .+ ?B) ] => apply WF_plus 
-  | [ |- WF_Matrix _ _ (?p .* ?B) ] => apply WF_scale
-  | [ |- WF_Matrix _ _ (?A ⊗ ?B) ]  => apply WF_kron
-  | [ |- WF_Matrix _ _ (?A⊤) ]      => apply WF_transpose 
-  | [ |- WF_Matrix _ _ (?A†) ]      => apply WF_adjoint 
-  | [ |- WF_Matrix _ _ (I _) ]     => apply WF_I
-  end;
-  trivial;
-  unfold WF_Matrix;
-  let x := fresh "x" in
-  let y := fresh "y" in
-  let H := fresh "H" in
-  intros x y [H | H];
-    repeat (destruct x; try reflexivity; try lia);
-    repeat (destruct y; try reflexivity; try lia).
-*)
-
 (* Much less awful *)
 Ltac show_wf := 
   unfold WF_Matrix;
@@ -522,10 +476,7 @@ Ltac show_wf :=
      WF_Mmult_n WF_Msum : wf_db.
 #[export] Hint Extern 2 (_ = _) => unify_pows_two : wf_db.
 
-(* Hint Resolve WF_Matrix_dim_change : wf_db. *)
-
-
-(** Basic Matrix Lemmas **)
+(** * Basic matrix lemmas *)
 
 Lemma WF0_Zero_l :forall (n : nat) (A : Matrix 0%nat n), WF_Matrix A -> A = Zero.
 Proof.

Measurement.v

@@ -1,16 +1,13 @@
 Require Import VectorStates.
 
-(* ============================== *)
-(**    Measurement predicates    **)
-(* ============================== *)
+(** This file contains predicates for describing the outcomes of measurement. *)
 
-(* What is the probability of outcome ϕ given input ψ? *)
+(** * Probability of outcome ϕ given input ψ *)
 Definition probability_of_outcome {n} (ϕ ψ : Vector n) : R :=
   let c := (ϕ† × ψ) O O in
   (Cmod c) ^ 2.
 
-(* What is the probability of measuring ϕ on the first m qubits given
-  (m + n) qubit input ψ? *)
+(** * Probability of measuring ϕ on the first m qubits given (m + n) qubit input ψ *)
 Definition prob_partial_meas {m n} (ϕ : Vector (2^m)) (ψ : Vector (2^(m + n))) :=
   Rsum (2^n) (fun y => probability_of_outcome (ϕ ⊗ basis_vector (2^n) y) ψ).
 

Pad.v

@@ -1,7 +1,10 @@
 Require Export Complex.
 Require Export Quantum.
 
-(* Padding; used to extend a matrix to a larger space *)
+(** This file provides padding functions to extend a matrix to a larger space.
+   This is useful for describing the effect of 1- and 2-qubit gates on a larger
+   quantum space. *)
+
 Definition pad {n} (start dim : nat) (A : Square (2^n)) : Square (2^dim) :=
   if start + n <=? dim then I (2^start) ⊗ A ⊗ I (2^(dim - (start + n))) else Zero.
 
@@ -40,7 +43,7 @@ Definition pad_ctrl (dim m n: nat) (u: Square 2) :=
 Definition pad_swap (dim m n: nat) :=
   pad_ctrl dim m n σx × pad_ctrl dim n m σx × pad_ctrl dim m n σx.
 
-(** Well-formedness **)
+(** Well-formedness *)
 
 Lemma WF_pad_u : forall dim n u, WF_Matrix u -> WF_Matrix (pad_u dim n u).
 Proof.
@@ -67,6 +70,8 @@ Qed.
 
 #[export] Hint Resolve WF_pad WF_pad_u WF_pad_ctrl WF_pad_swap : wf_db.
 
+(** Unitarity *)
+
 Lemma pad_unitary : forall n (u : Square (2^n)) start dim,
     (start + n <= dim)%nat -> 
     WF_Unitary u ->
@@ -131,7 +136,7 @@ Proof.
     apply pad_ctrl_unitary; auto; apply σx_unitary. 
 Qed.
 
-(* Lemmas about commutation *)
+(** Lemmas about commutation *)
 
 Lemma pad_A_B_commutes : forall dim m n A B,
   m <> n ->

Permutations.v

@@ -1,10 +1,10 @@
 Require Import VectorStates.
 
-(* Facts about permutations and matrices that implement them *)
+(** Facts about permutations and matrices that implement them. *)
 
 Local Open Scope nat_scope.
 
-(* permutation on [0,...,n-1] *)
+(** * Permutations on (0,...,n-1) *)
 Definition permutation (n : nat) (f : nat -> nat) :=
   exists g, forall x, x < n -> (f x < n /\ g x < n /\ g (f x) = x /\ f (g x) = x).
 
@@ -99,7 +99,7 @@ Proof.
     destruct (Hg x0) as [_ [_ [_ ?]]]; lia.
 Qed.
 
-(* vsum terms can be arbitrarily reordered *)
+(** vsum terms can be arbitrarily reordered *)
 Lemma vsum_reorder : forall {d} n (v : nat -> Vector d) f,
   permutation n f ->
   vsum n v = vsum n (fun i => v (f i)).
@@ -121,7 +121,7 @@ Proof.
   exists g. auto.
 Qed.
 
-(* Permutation matrices *)
+(** * Permutation matrices *)
 
 Definition perm_mat n (p : nat -> nat) : Square n :=
   (fun x y => if (x =? p y) && (x <? n) && (y <? n) then C1 else C0).
@@ -216,7 +216,7 @@ Proof.
   contradiction.
 Qed.
 
-(* Given a permutation p over n qubits, produce a permutation over 2^n indices. *)
+(** Given a permutation p over n qubits, construct a permutation over 2^n indices. *)
 Definition qubit_perm_to_nat_perm n (p : nat -> nat) :=
   fun x:nat => funbool_to_nat n ((nat_to_funbool n x) ∘ p)%prg.
 
@@ -252,6 +252,7 @@ Proof.
   rewrite nat_to_funbool_inverse; auto.
 Qed.  
 
+(** Transform a (0,...,n-1) permutation into a 2^n by 2^n matrix. *)
 Definition perm_to_matrix n p :=
   perm_mat (2 ^ n) (qubit_perm_to_nat_perm n p).
 

Proportional.v

@@ -1,6 +1,8 @@
 Require Export Matrix.
 Require Import Setoid.
 
+(** Relation for equality up to a global phase. *)
+
 Definition proportional {m n : nat} (A B : Matrix m n) := 
   exists θ, A = Cexp θ .* B. 
 Infix "∝" := proportional (at level 70).

README.md

@@ -20,8 +20,6 @@ Run `make doc` to generate documentation.
 
 ## Directory Contents
 
-**TODO: Improve summaries. (Or remove entirely if the coqdoc documentation is sufficient.)**
-
 * Complex.v - Definition of Complex numbers, extending [Coquelicot](http://coquelicot.saclay.inria.fr/)'s.
 * Ctopology.v - A topology of open/closed sets is defined for the complex numbers, with lemmas about compactness.
 * DiscreteProb.v - Theory of discrete probability distributions and utility to describe running a quantum program ("apply_u") and sampling from the output distribution.