work in progress on compilation and semantics

src/Compilation.v

@@ -18,7 +18,7 @@
  *)
 From Coq Require Import String Arith.
 From SQIR Require Import ExtractionGateSet.
-From Qunity Require Import Lists Reals Types Syntax Contexts Typing Matrix.
+From Qunity Require Import Lists Reals Types Syntax Contexts Typing Value Matrix.
 Import ListNotations.
 Import ExtractionGateSet (control).
 
@@ -434,8 +434,9 @@ Fixpoint compile_erases {x tx t' l} (P : erases x tx t' l) :=
 
 (* type : d * t' -> t' *)
 Fixpoint compile_erasure {d t' l}
-  (P : for_all (fun '(x, tx) => erases x tx t' l) d) :
-  ocom :=
+  (P : forall x tx, in_list (x, tx) d -> erases x tx t' l) {struct d} :
+  ocom.
+:=
   match P with
   | for_all_nil _ =>
       oskip

src/Complex.v

 From Coq Require Import List Reals.
-From Coquelicot Require Export Complex.
+From QuantumLib Require Export Complex.
 Import ListNotations.
 
 Open Scope R_scope.

src/Int.v

 From Coq Require Export Fin.
-From Coq Require Import List Basics FinFun Equality.
+From Coq Require Import List Basics FinFun.
 From VFA Require Import Perm.
 From Qunity Require Import Tactics.
 
@@ -7,69 +7,20 @@ Set Implicit Arguments.
 
 Open Scope vector_scope.
 
-Definition int := t.
+Definition int n : Set := t n.
 
-Definition destruct_int n (j : int (S n)) : option (int n) :=
-  match j with
-  | F1 => None
-  | FS j' => Some j'
-  end.
-
-Fixpoint destruct_sum n0 n1 : int (n0 + n1) -> int n0 + int n1 :=
-  match n0 with
-  | 0 => inr
-  | S n0' => fun j => match destruct_int j with
-                      | None => inl F1
-                      | Some j' => match destruct_sum n0' n1 j' with
-                                   | inl j0 => inl (FS j0)
-                                   | inr j1 => inr j1
-                                   end
-                      end
-  end.
-
-Fixpoint destruct_prod n0 n1 : int (n0 * n1) -> int n0 * int n1 :=
-  match n0 with
-  | 0 =>
-      fun j => match j with end
-  | S n0' =>
-      fun j => match destruct_sum n1 (n0' * n1) j with
-      | inl j1 => (F1, j1)
-      | inr j' => let (j0, j1) := destruct_prod n0' n1 j' in (FS j0, j1)
-      end
-  end.
-
-Lemma destruct_int_spec0 :
-  forall n, destruct_int (n:=n) F1 = None.
-Proof. reflexivity. Qed.
-
-Lemma destruct_int_spec1 :
-  forall n (j : int n), destruct_int (FS j) = Some j.
-Proof. reflexivity. Qed.
-
-Lemma destruct_sum_spec0 :
-  forall n0 n1 j0, destruct_sum n0 n1 (L n1 j0) = inl j0.
-Proof.
-  intros n0.
-  induction n0 as [| n0 IH];
-  intros n1 j0; dependent destruction j0; simpl; auto.
-  rewrite IH. reflexivity.
-Qed.
-
-Lemma destruct_sum_spec1 :
-  forall n0 n1 j1, destruct_sum n0 n1 (R n0 j1) = inr j1.
-Proof.
-  intros n0.
-  induction n0 as [| n0 IH];
-  intros n1 j0; dependent destruction j0; simpl; auto; rewrite IH; reflexivity.
-Qed.
-
-Lemma destruct_prod_spec :
-  forall n0 n1 j0 j1,
-  destruct_prod n0 n1 (depair j0 j1) = (j0, j1).
-Proof.
-  intros n0.
-  induction n0 as [| n0 IH]; intros n1 j0 j1; dependent destruction j0; simpl.
-  - rewrite destruct_sum_spec0. reflexivity.
-  - rewrite destruct_sum_spec1, IH. reflexivity.
-Qed.
+Definition int_case0 P (j : int 0) : P j :=
+  match j with end.
 
+Definition int_cases :
+  forall n (P : int (S n) -> Type),
+  P F1 ->
+  (forall j, P (FS j)) ->
+  forall j, P j :=
+  fun n P H1 Hs j =>
+  match j with
+  | @F1 n =>
+      fun (P : int (S n) -> Type) (H1 : P F1) (Hs : forall j, P (FS j)) => H1
+  | @FS n j' =>
+      fun _ _ Hs => Hs j'
+  end P H1 Hs.

src/Matrix.v

@@ -66,6 +66,12 @@ Definition outer_product {n m} (u' : Vector n) (u : Vector m) : Matrix n m :=
 Definition swap n0 n1 : Matrix (n1 * n0) (n0 * n1) :=
   Msum n0 (fun i0 => Msum n1 (fun i1 => (e_i i1 <*> e_i i0) * adjoint (e_i i0 <*> e_i i1))%M).
 
+Fixpoint msum_list {m n} (l : list (Matrix m n)) : Matrix m n :=
+  match l with
+  | [] => Zero
+  | A :: l' => A .+ msum_list l'
+  end.
+
 Definition tensor_super {m0 m1 n0 n1}
   (f0 : Superoperator m0 n0) (f1 : Superoperator m1 n1) :
   Superoperator (m0 * m1) (n0 * n1) :=

src/Qubity.v

-(* Qunity - A Unified Language for Quantum and Classical Computing
- * Copyright (C) 2022 University of Maryland
- *
- * This file is part of Qunity.
- *
- * Qunity is free software: you can redistribute it and/or modify it under the
- * terms of the GNU General Public License as published by the Free Software
- * Foundation, either version 3 of the License, or (at your option) any later
- * version.
- *
- * This program is distributed in the hope that it will be useful, but WITHOUT
- * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
- * FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
- * details.
- *
- * You should have received a copy of the GNU General Public License along with
- * this program. If not, see <https://www.gnu.org/licenses>.
- *)
+From Coq Require Import List Arith Lia Basics Equality.
+From Qunity Require Import Int Vector.
+Import EqNotations.
+Import Nat (add_assoc).
+
+Set Implicit Arguments.
+
+Declare Scope q_scope.
+Open Scope q_scope.
+
+Inductive type : Set :=
+ | void
+ | unit
+ | sum (t0 t1 : type).
+
+Infix "+" := sum : q_scope.
+
+Fixpoint size t : nat :=
+  match t with
+  | void | unit => 0
+  | t0 + t1 => S (max (size t0) (size t1))
+  end.
+
+Fixpoint cardinal t : nat :=
+  match t with
+  | void => 0
+  | unit => 1
+  | t0 + t1 => cardinal t0 + cardinal t1
+  end.
+
+Fixpoint empty n : type :=
+  match n with
+  | 0 => void
+  | S n' => empty n' + empty n'
+  end.
+
+Fixpoint singleton n : type :=
+  match n with
+  | 0 => unit
+  | S n' => singleton n' + empty n'
+  end.
+
+Fixpoint prod t0 t1 : type :=
+  match t0 with
+  | void => empty (siz
+  | unit => t1
+  | t00 + t01 => t00 * t1 + t01 * t1
+  end
+where "t0 * t1" := (prod t0 t1).
+
+Inductive val : forall n, type n -> Set :=
+  | null : val unit
+  | left n (t0 t1 : type n) : val t0 -> val (t0 + t1)
+  | right n (t0 t1 : type n) : val t1 -> val (t0 + t1).
+
+Fixpoint pair n0 n1 (t0 : type n0) (t1 : type n1) (v0 : val t0) (v1 : val t1) :
+  val (t0 * t1) :=
+  match v0 with
+  | null => v1
+  | left t01 v00 => left (t01 * t1) (v00, v1)
+  | right t00 v01 => right (t00 * t1) (v01, v1)
+  end
+where "( t1 , t2 , .. , tn )" := (pair .. (pair t1 t2) .. tn).
+
+Fixpoint values n (t : type n) : vector (val t) (cardinal t) :=
+  match t with
+  | void =>
+      nil (val void)
+  | unit =>
+      null :: nil (val unit)
+  | t0 + t1 =>
+      compose (left (t0:=t0) t1) (values t0) ++
+      compose (right t0 (t1:=t1)) (values t1)
+  end.
+
+Fixpoint encode n (t : type n) (v : val t) : vector bool n :=
+  match v with
+  | null => nil bool
+  | left t1 v0 => false :: encode v0
+  | right t0 v1 => true :: encode v1
+  end.
+
+Fixpoint decode (l : list bool) : forall t : type (length l), option (val t).
+Proof.
+  destruct l; intros [| | n t0 t1 ].
+  - apply None.
+  - apply Some, null.
+  - apply None.
+  - apply None.
+  - apply None.
+  - destruct b.
+    + apply (option_map (left (t0:=t0) t1)).
+  match n with
+  | 0 =>
+      fun (t : type 0) _ =>
+      match t in type 0 return option (val t) with
+      | void => None
+      | unit => Some null
+      | _ + _ => False_rect Datatypes.unit
+      end
+  | S n' =>
+      fun (t : type (S n')) (b : vector bool (S n')) =>
+      let head := hd b in
+      let tail := tl b in
+      match t in type (S n') return option (val t) with
+      | t0 + t1 => 
+          match head return option (val (n:=n') (t0 + t1)) with
+          | false => option_map (left (t0:=t0) t1) (decode (n:=n') t0 tail)
+          | true => option_map (right t0 (t1:=t1)) (decode (n:=n') t1 tail)
+          end
+      | _ => False_rect Datatypes.unit
+      end
+  end.
+
+Lemma cardinal_void :
+  forall n, cardinal (sized_void n) = 0.
+Proof.
+  intros n. induction n; simpl; lia.
+Qed.
+
+Lemma cardinal_unit :
+  forall n, cardinal (sized_unit n) = 1.
+Proof.
+  intros n. induction n; simpl; try rewrite cardinal_void; lia.
+Qed.
+
+Lemma cardinal_le_pow_2_n :
+  forall n (t : type n), cardinal t <= 2 ^ n.
+Proof.
+  intros n t. induction t; simpl; lia.
+Qed.
+
+Lemma qubit_representation_unique :
+  forall n, 
+
+Definition maybe t := unit + t.
+
+Definition bit := unit + unit.
+
+Definition trit
 
 From Coq Require Import List ListSet ZArith.
 From Qunity Require Import Reals.
@@ -26,16 +148,48 @@ Open Scope qubity_scope.
 
 Local Coercion const : Z >-> real.
 
-Definition reg := set nat.
+Definition reg : Set := list nat.
 
-Inductive com :=
+Inductive com : Set :=
   | skip
   | gphase (gamma : real)
   | u3 (theta phi lambda : real)
-  | ctrl (i0 i1 i : reg) (c : com)
-  | seq (c c' : com).
+  | ctrl (i0 i1 i : reg) (l : list com).
+
+Definition disjoint (i0 i1 : reg) : Prop :=
+  forall n, In n i0 -> In n i1 -> False.
 
-Infix ";;" := seq (at level 50) : qubity_scope.
+Inductive well_formed : com -> nat -> Prop :=
+  | well_formed_skip n :
+      well_formed skip n
+  | well_formed_gphase gamma n :
+      well_formed (gphase gamma) n
+  | well_formed_u3 theta phi lambda n :
+      well_formed (u3 theta phi lambda) (S n)
+  | well_formed_ctrl i0 i1 i l n :
+      ForallOrdPairs disjoint [i0; i1; i] ->
+      Forall (fun m => m < n) i0 ->
+      Forall (fun m => m < n) i1 ->
+      Forall (fun m => m < n) i ->
+      Forall (fun c => well_formed c (length i)) l ->
+      well_formed (ctrl i0 i1 i l) n.
+
+Fixpoint qubits c :=
+  match c with
+  | skip | gphase _ => Some 0
+  | u3 _ _ _ => Some 1
+  | ctrl i0 i1 i l => map qubits l
+  end
+with qubits_list l :=
+  match l with
+  | [] | None :: _ => 
+      if forallb (fun c' => match c' with
+                                            | None => false
+
+Definition well_formed c n :=
+  match c with
+  | skip | gphase _ => true
+  | u3 _ _ _ => 
 
 Fixpoint qubits c :=
   match c with
@@ -45,6 +199,11 @@ Fixpoint qubits c :=
   | c;; c' => max (qubits c) (qubits c')
   end.
 
+Fixpoint depth c :=
+  match c with
+  | skip => 0
+  | gphase _ | u3 _ _ _ => 1
+
 Definition pauli_x := u3 pi 0%Z pi.
 
 Definition cnot := ctrl [] [0] [1] pauli_x.

src/Semantics.v

 From Coq Require Import Arith Bool Equality FunctionalExtensionality Reals Lia.
-From QuantumLib Require Import Complex Quantum.
-From Qunity Require Import Reals Matrix Types Syntax Contexts Typing Value.
+From QuantumLib Require Import Quantum.
+From Qunity Require Import Reals Complex Matrix Types Syntax Contexts Typing Value.
 
 Declare Scope qunity_scope.
 Open Scope nat_scope.
-Open Scope matrix_scope.
 Open Scope qunity_scope.
+Open Scope matrix_scope.
 
 Local Coercion ctx2type : context >-> type.
+Local Coercion valuation2value : valuation >-> expr.
+
+Definition linearize (d : context)  {t'} (f : valuation -> Vector (cardinal t')) :
+  Matrix (cardinal t') (cardinal d) :=
+  msum_list (map (fun e => outer_product (f e) (ket d e)) (valuations d)).
+
+Definition null_sem (_ : valuation) : Vector (cardinal qunit) :=
+  ket qunit null.
+
+Definition cvar_sem t (e : expr) (_ : valuation) : Vector (cardinal t) :=
+  ket t e.
+
+Definition qvar_sem t (v : valuation) : Vector (cardinal t) :=
+  match v with
+  | (_, e) :: [] => ket t e
+  | _ => Zero
+  end.
+
+(* v is the quantum valuation tau *)
+Definition pure_pair_sem (d d0 d1 : context) (t0 t1 : type)
+  (M0 : Matrix (cardinal t0) (cardinal (d * d0)))
+  (M1 : Matrix (cardinal t1) (cardinal (d * d1)))
+  (v : valuation) : 
+  Vector (cardinal (t0 * t1)) :=
+  let v' : valuation := firstn (length d) v in
+  let v2 := skipn (length d) v in
+  let v0 : valuation := firstn (length d0) v2 in
+  let v1 : valuation := skipn (length d0) v2 in
+  (M0 * (ket d v' <*> ket d0 v0)) <*> (M1 * (ket d v' <*> ket d1 v1)).
 
-Definition pure_expr_sem {g d e t} (P : has_pure_type g d e t) (s : valuation) :
-  Matrix (cardinal g) (cardinal t) :=
+Definition case_sem 
+  (gj d : context) (t t' : type)
+  (Mj : Matrix (cardinal t) (cardinal gj))
+  (Mj' : valuation -> Matrix (cardinal t') (cardinal d))
+  (v : expr) :
+  Matrix (cardinal t') (cardinal t) :=
+  msum_list (map (fun sj : valuation =>
+                  adjoint Mj (val_index gj sj) (val_index t v) .* Mj' sj)
+                 (valuations gj)).
+
+Definition ctrl_sem
+  (g d d' : context) (t t' : type)
+  (E : Superoperator (cardinal t) (cardinal t'))
+  (M : expr -> Matrix (cardinal t') (cardinal t))
+  (s tau_tau' : valuation) :
+  Vector (cardinal t') :=
+  let tau : valuation := firstn (length d) tau_tau' in
+  let tau' : valuation := skipn (length d) tau_tau' in
+  msum_list (map (fun v =>
+                  E (outer_product (ket (g * d) (qpair s tau))
+                                   (ket (g * d) (qpair s tau)))
+                    (val_index t v) (val_index t v) .*
+                  M v * ket (d * d') tau_tau')
+       (values t)).
+
+Definition pure_swap_sem
+  (d1 d2 d3 d4 : context) (t : type)
+  (M : Matrix (cardinal t) (cardinal (d1 * d2 * d3 * d4)))
+  (v : valuation) :
+  Vector (cardinal t) :=
+  let tau1 : valuation := firstn (length d1) v in
+  let tau324 := skipn (length d1) v in
+  let tau3 : valuation := firstn (length d3) tau324 in
+  let tau24 := skipn (length d3) tau324 in
+  let tau2 : valuation := firstn (length d2) tau24 in
+  let tau4 : valuation := skipn (length d2) tau24 in
+  M * ket (d1 * d2 * d3 * d4) (qpair tau1 (qpair tau2 (qpair tau3 tau4))).
+
+Definition pure_prog_sem {f t t'} (P : has_prog_type f (t ~> t')) :
+  Matrix (cardinal t') (cardinal t) :=
+  Zero. (* TODO *)
+
+(* v is the classical valuation sigma, of type g *)
+Fixpoint pure_expr_sem {g d e t}
+  (P : has_pure_type g d e t) (v : valuation) {struct P}  :
+  Matrix (cardinal t) (cardinal d) :=
   match P with
   | has_type_null _ =>
-      I 1
+      linearize [] null_sem
   | has_type_cvar _ x t _ =>
-      @e_i (cardinal t) (val_index t (s x))
-  | _ => Zero (* TODO *)
+      linearize [] (cvar_sem t (v x))
+  | has_type_qvar _ x t =>
+      linearize [(x, t)] (qvar_sem t)
+  | has_pure_type_pair _ d d0 d1 _ _ t0 t1 P0 P1 =>
+      linearize (d ++ d0 ++ d1)
+      (pure_pair_sem d d0 d1 t0 t1 (pure_expr_sem P0 v) (pure_expr_sem P1 v))
+  | has_type_ctrl g _ d d' _ _ t t' Pe _ Pp _ =>
+      let s := firstn (length g) v in
+      linearize (d ++ d')
+      (ctrl_sem g d d' t t' (mixed_expr_sem Pe) (pattern_sem Pp s) s)
+  | has_pure_type_app g d _ _ t t' Pf Pe =>
+      pure_prog_sem Pf * pure_expr_sem Pe v
+  | has_pure_type_swap _ d1 d2 d3 d4 _ t P' =>
+      linearize (d1 ++ d3 ++ d2 ++ d4)
+      (pure_swap_sem d1 d2 d3 d4 t (pure_expr_sem P' v))
+  end
+with pattern_sem {g d l t t'}
+  (P : has_pattern_type g d l t t') (s : valuation) (v : expr) {struct P} :
+  Matrix (cardinal t') (cardinal t) :=
+  match P with
+  | has_type_nil _ _ _ _ =>
+      Zero
+  | has_type_cons g gj d _ _ _ _ _ _ Pe P' Pp =>
+      let Mj := pure_expr_sem Pe [] in
+      let Mj' := fun sj => pure_expr_sem P' (s ++ sj) in
+      case_sem gj d t t' Mj Mj' v .+ pattern_sem Pp s v
+  end
+with mixed_expr_sem {d e t} (P : has_mixed_type d e t) {struct P} :
+  Superoperator (cardinal d) (cardinal t) :=
+  match P with
+  | has_type_mix _ _ _ P' =>
+      super (pure_expr_sem P' [])
+  | _ => SZero (* TODO *)
   end.
 
+
+
 Lemma val_cardinal_nonzero :
   forall t, inhabited (val t) -> cardinal t <> 0.
 Proof.

src/Value.v

@@ -34,8 +34,8 @@ Fixpoint values t : list expr :=
 
 Fixpoint val_index t e : nat :=
   match t, e with
-  | t0 + t1, apply (left _ _) e0 => val_index t0 e0
-  | t0 + t1, apply (right _ _) e1 => cardinal t0 + val_index t1 e1
+  | t0 + t1, e0 |> left _ _ => val_index t0 e0
+  | t0 + t1, e1 |> right _ _ => cardinal t0 + val_index t1 e1
   | t0 * t1, #(e0, e1) => cardinal t1 * val_index t0 e0 + val_index t1 e1
   | _, _ => 0
   end.
@@ -53,8 +53,8 @@ Fixpoint indexed_val t n : expr :=
 
 Fixpoint encode_val t e : nat :=
   match t, e with
-  | t0 + t1, apply (left _ _) e0 => encode_val t0 e0
-  | t0 + t1, apply (right _ _) e1 => 2 ^ size t0 + encode_val t1 e1
+  | t0 + t1, e0 |> left _ _ => encode_val t0 e0
+  | t0 + t1, e1 |> right _ _ => 2 ^ size t0 + encode_val t1 e1
   | t0 * t1, #(e0, e1) => 2 ^ size t1 * encode_val t0 e0 + encode_val t1 e1
   | _, _ => 0
   end.

src/Vector.v

-From Coq Require Export Fin.
-From Coq Require Import List Basics FinFun Equality.
-From VFA Require Import Perm.
-From Qunity Require Import Tactics.
+From Coq Require Import Bool List Basics FunctionalExtensionality.
+From Qunity Require Import Int Tactics.
+Import ListNotations.
 
 Set Implicit Arguments.
 
 Open Scope vector_scope.
 
-Notation int := t.
-
-Definition destruct_int n (j : int (S n)) : option (int n) :=
-  match j with
-  | F1 => None
-  | FS j' => Some j'
-  end.
-
-Fixpoint destruct_sum {n0 n1} : int (n0 + n1) -> int n0 + int n1 :=
-  match n0 with
-  | 0 => inr
-  | S n0' => fun j => match destruct_int j with
-                      | None => inl F1
-                      | Some j' => match destruct_sum j' with
-                                   | inl j0 => inl (FS j0)
-                                   | inr j1 => inr j1
-                                   end
-                      end
-  end.
-
-Fixpoint destruct_prod {n0 n1} : int (n0 * n1) -> int n0 * int n1 :=
-  match n0 with
-  | 0 =>
-      fun j => match j with end
-  | S n0' =>
-      fun j => match destruct_sum j with
-      | inl j1 => (F1, j1)
-      | inr j' => let (j0, j1) := destruct_prod j' in (FS j0, j1)
-      end
-  end.
-
-Definition vector (A : Set) n := int n -> A.
+Definition vector (A : Set) n : Set := int n -> A.
 
 Definition hd A n (v : vector A (S n)) : A := v F1.
 
@@ -62,14 +30,8 @@ Fixpoint forallb n : vector bool n -> bool :=
   | S n' => fun v => hd v && forallb (tl v)
   end.
 
-Definition app A n0 n1 (v0 : vector A n0) (v1 : vector A n1) :
-  vector A (n0 + n1) :=
-  fun j => match destruct_sum j with
-           | inl j0 => v0 j0
-           | inr j1 => v1 j1
-           end.
-
-Infix "++" := app : vector_scope.
+Definition eqb_vector n A eqb (v v' : vector A n) : bool :=
+  forallb (fun j => eqb (v j) (v' j)).
 
 Fixpoint to_list A n : vector A n -> list A :=
   match n with
@@ -77,48 +39,12 @@ Fixpoint to_list A n : vector A n -> list A :=
   | S n' => fun v => (hd v :: to_list (tl v))%list
   end.
 
-Definition nodup A n (v : vector A n) :=
-  forall j k, v j = v k -> j = k.
-
-Lemma cast_correct :
-  forall n (j : int n) H, cast j H = j.
-Proof.