Merge pull request #45 from inQWIRE/circuit-proof

Add peephole optimization

.meta/assoc_count.py

@@ -0,0 +1,126 @@
+#!/usr/bin/env python3
+
+import re
+import os
+import sys
+import functools 
+
+
+MIN_PYTHON = (3, 10)
+if sys.version_info < MIN_PYTHON:
+  print(f"Your python version is {sys.version_info.major}.{sys.version_info.minor}. {MIN_PYTHON[0]}.{MIN_PYTHON[1]} is required")
+  exit(3)
+
+
+b_color_yellow = '\033[93m'
+b_color_cyan = '\033[96m'
+b_color_reset = '\033[0m'
+b_color_green = '\033[92m'
+b_color_red = '\033[91m'
+
+is_windows = sys.platform.startswith('win')
+if is_windows: # Disable colors on windows 
+  b_color_yellow = ''
+  b_color_cyan = ''
+  b_color_reset = ''
+  b_color_green = ''
+  b_color_red = ''
+  print("Warning: Windows detected. Disabling colored output")
+
+curr_dir = os.path.dirname(os.path.realpath(__file__))
+src_dir = f"{curr_dir}/../src"
+
+regex_assoc : list[re.Pattern] = list(map(re.compile, [
+  r".*rewrite.*assoc",
+  r".*rewrite.*dist",
+  r".*rewrite.*mixed_product",
+  r".*rewrite.*cast",
+  r".*cleanup_zx",
+  r".*cast_id",
+  r".*simpl_cast",
+  r".*bundle_wires",
+  r".*restore_dims",
+  r".*cast_irrelevance",
+  r".*apply .*_simplify",
+  r".*rewrite.*stack_empty_.",
+  r".*rewrite.*n_stack1_",
+  r".*rewrite.*n_wire_stack",
+  r".*rewrite.*wire_to_n_wire",
+  r".*rewrite.*wire_removal_",
+  r".*rewrite.*(n_wire|nstack1)_split",
+]))
+proof_regex = re.compile(r'Proof\.((?:(?!Proof\.|Qed\.|Defined\.|Admitted\.|Abort\.)(?!\b(?:Proof|Qed|Defined|Admitted|Abort)\b)[\s\S])*?)(Qed\.|Defined\.|Admitted\.|Abort\.)')
+stmt_regex = re.compile(r'(([a-z|A-Z|0-9])+(\t| |[a-z|A-Z|0-9]|.)*)(\t| )*(\n|;|$)')
+
+class Result:
+  non_assoc : int
+  assoc : int
+  repeat_assoc : int
+
+  def __init__(self, non_assoc : int = 0, assoc : int = 0, repeat_assoc : int = 0) -> None:
+    self.non_assoc = non_assoc  
+    self.assoc = assoc
+    self.repeat_assoc = repeat_assoc
+
+
+  def __add__(self, other):
+    return Result(self.non_assoc + other.non_assoc, self.assoc + other.assoc, self.repeat_assoc + other.repeat_assoc)
+
+  def __iadd__(self, other):
+    self.assoc += other.assoc
+    self.non_assoc += other.non_assoc
+    self.repeat_assoc += other.repeat_assoc
+    return self
+
+  def total_assoc(self) -> int:
+    return self.assoc + self.repeat_assoc
+
+  def total(self) -> int:
+    return self.total_assoc() + self.non_assoc
+
+  def __str__(self) -> str:
+    return \
+f"""{b_color_red}Number of repeated assoc lines:{b_color_reset} {self.repeat_assoc} ({self.repeat_assoc / self.total():.2%}) ({self.repeat_assoc / self.total_assoc():.2%} of all assoc lines)
+{b_color_yellow}Number of assoc lines:{b_color_reset} {self.assoc} ({self.assoc / self.total():.2%}) ({self.assoc / self.total_assoc():.2%} of all assoc lines)
+{b_color_cyan}Total of any assoc lines:{b_color_reset} {self.total_assoc()} ({self.total_assoc() / self.total():.2%})
+{b_color_green}Number of other proof lines:{b_color_reset} {self.non_assoc} ({self.non_assoc / self.total():.2%})
+Total lines: {self.total()}
+"""
+
+do_regex = re.compile(r'do \d+')
+
+
+def count_assoc_non_assoc(proof : str, proof_completion : str) -> Result:
+  if proof_completion != "Qed." and proof_completion != "Defined.":
+    return Result()
+  result = Result()
+  for stmt in stmt_regex.findall(proof):
+    if any(map(lambda pattern : pattern.match(stmt[0]), regex_assoc)):
+      if 'repeat' in stmt[0] or do_regex.match(stmt[0]):
+        result.repeat_assoc += 1
+      else:
+        result.assoc += 1
+    else:
+      result.non_assoc += 1
+  return result
+
+
+def count_assoc_file(file : str) -> tuple[int, int]:
+  with open(file) as f:
+    data = f.read()
+    proofs = proof_regex.findall(data)
+    result = functools.reduce(lambda curr, proof : count_assoc_non_assoc(proof[0], proof[-1]) + curr , proofs, Result())
+    return result
+
+result = Result()
+for dir, _, files in os.walk(src_dir):
+  for file in files:
+    print(f"Checking {dir}/{file}...")
+    if not file.endswith(".v"): # Make sure we only look at Coq files
+      continue
+    result += count_assoc_file(f"{dir}/{file}")
+
+print(result)
+
+
+

LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2021 INQWIRE
+Copyright (c) 2021 REDACTED
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -2,8 +2,6 @@
 
 Verifying the ZX Calculus
 
-[Check out the paper on arxiv](https://arxiv.org/abs/2205.05781)
-
 ## Building VyZX
 
 Works with Coq 8.16-8.18.

coq-vyzx.opam

@@ -3,17 +3,14 @@ opam-version: "2.0"
 version: "0.1.0"
 synopsis: "Coq library for reasoning about ZX diagrams"
 description: """
-inQWIRE's QuantumLib is a Coq library for reasoning
- about ZX diagrams.
+A Coq library for reasoning about ZX diagrams.
 """
-maintainer: ["inQWIRE Developers"]
-authors: ["inQWIRE"]
+maintainer: ["Anonymous"]
+authors: ["Anonymous"]
 license: "MIT"
-homepage: "https://github.com/inQWIRE/VyZX"
-bug-reports: "https://github.com/inQWIRE/VyZX/issues"
 depends: [
   "dune" {>= "2.8"}
-  "coq-quantumlib" {>= "1.3.0"}
+  "coq-quantumlib" {= "1.3.0"}
   "coq-sqir" {>= "1.3.0"}
   "coq-voqc" {>= "1.3.0"}
   "coq" {>= "8.16"}
@@ -33,4 +30,3 @@ build: [
     "@doc" {with-doc}
   ]
 ]
-dev-repo: "git+https://github.com/inQWIRE/VyZX.git"

dune-project

@@ -6,19 +6,17 @@
 (generate_opam_files true)
 
 (license MIT)
-(authors "inQWIRE")
-(maintainers "inQWIRE Developers")
-(source (github inQWIRE/VyZX))
+(authors "Anonymous")
+(maintainers "Anonymous")
 
 (package
  (name coq-vyzx)
  (synopsis "Coq library for reasoning about ZX diagrams")
- (description "\| inQWIRE's QuantumLib is a Coq library for reasoning
-              "\|  about ZX diagrams.
+ (description "\| A Coq library for reasoning about ZX diagrams.
  )
 
  (depends
-   (coq-quantumlib (>= 1.3.0))
+   (coq-quantumlib (= 1.3.0))
    (coq-sqir (>= 1.3.0))
    (coq-voqc (>= 1.3.0))
    (coq (>= 8.16))))

src/CoreData/Proportional.v

@@ -345,6 +345,16 @@ Proof.
   assumption.
 Qed.
 
+Lemma conjugate_diagrams : forall n m (zx0 zx1 : ZX n m),
+  zx0 ⊼ ∝ zx1 ⊼ -> zx0 ∝ zx1.
+Proof.
+  intros.
+  apply adjoint_diagrams.
+  unfold adjoint.
+  rewrite H.
+  easy.
+Qed.
+
 Lemma colorswap_adjoint_commute : forall n m (zx : ZX n m),
   ⊙ (zx †) ∝ (⊙ zx) †.
 Proof.
@@ -395,11 +405,3 @@ Proof.
   apply Z_spider_1_1_fusion.
 Qed.
 
-Lemma proportional_sound : forall {nIn nOut} (zx0 zx1 : ZX nIn nOut),
-  zx0 ∝ zx1 -> exists (zxConst : ZX 0 0), ⟦ zx0 ⟧ = ⟦ zxConst ↕ zx1 ⟧.
-Proof.
-  intros.
-  simpl; unfold proportional, proportional_general in H.
-  destruct H as [c [H cneq0]].
-  rewrite H.
-Abort.

src/CoreRules/CapCupRules.v

@@ -114,15 +114,6 @@ Unshelve.
   all: lia.
 Qed.
 
-Lemma n_cup_inv_n_swap_n_wire : forall n, n_cup n ∝ n_wire n ↕ n_swap n ⟷ n_cup_unswapped n.
-Proof.
-  intros.
-  strong induction n.
-  destruct n; [ | destruct n].
-  - simpl. rewrite n_cup_0_empty. cleanup_zx. simpl_casts. easy.
-  - simpl. rewrite n_cup_1_cup. cleanup_zx. simpl_casts. bundle_wires. cleanup_zx. easy.    
-Admitted. (*TODO*)
-
 Lemma n_cup_unswapped_colorswap : forall n, ⊙ (n_cup_unswapped n) ∝ n_cup_unswapped n.
 Proof. 
   intros.
@@ -207,4 +198,72 @@ Qed.
   (fun n => @n_cap_unswapped_transpose n)
   (fun n => @n_cup_transpose n)
   (fun n => @n_cap_transpose n)
-  : transpose_db.
+  : transpose_db.
+Local Open Scope ZX_scope.
+
+Lemma bigyank_cap : forall (zx1 : ZX 1 1),
+  ⊂ ↕ zx1 ∝ — ↕ ⊂ ⟷ top_to_bottom 3 ⟷ (— ↕ — ↕ zx1).
+Proof.
+  intros.
+  rewrite top_to_bottom_grow_r.
+  simpl_casts.
+  rewrite top_to_bottom_2.
+  repeat rewrite compose_assoc.
+  rewrite (stack_assoc — —).
+  zx_simpl.
+  repeat rewrite ComposeRules.compose_assoc.
+  rewrite <- (stack_wire_distribute_l ⨉ (— ↕ zx1)).
+  rewrite <- swap_comm.
+  rewrite stack_wire_distribute_l.
+  rewrite <- (ComposeRules.compose_assoc (⨉ ↕ —)).
+  rewrite (stack_assoc_back — (zx1)).
+  zx_simpl.
+  rewrite <- (stack_wire_distribute_r ⨉ (— ↕ zx1)).
+  rewrite <- swap_comm.
+  solve_prop 1.
+  Unshelve.
+  all: lia.
+Qed.
+
+Lemma bigyank_cup : forall (zx1 : ZX 1 1),
+  top_to_bottom 3 ⟷ (⊃ ↕ zx1) ∝ — ↕ ⊃ ⟷ zx1.
+Proof.
+  intros.
+  rewrite (stack_empty_r_rev zx1) at 2.
+  simpl_casts.
+  rewrite <- (stack_compose_distr — zx1).
+  cleanup_zx.
+  rewrite top_to_bottom_grow_l.
+  cleanup_zx.
+  rewrite top_to_bottom_2.
+  rewrite ComposeRules.compose_assoc.
+  rewrite <- (nwire_removal_l ⊃).
+  rewrite <- (wire_removal_r zx1).
+  rewrite (stack_compose_distr).
+  zx_simpl.
+  rewrite <- (ComposeRules.compose_assoc (— ↕ ⨉)).
+  rewrite stack_assoc.
+  simpl_casts.
+  rewrite <- stack_wire_distribute_l.
+  rewrite <- swap_comm.
+  rewrite stack_wire_distribute_l.
+  rewrite <- 2 (ComposeRules.compose_assoc (⨉ ↕ —)).
+  rewrite (stack_assoc_back — zx1 —). 
+  simpl_casts.
+  rewrite <- (stack_wire_distribute_r (⨉) (— ↕ zx1)).
+  rewrite <- swap_comm.
+  zx_simpl.
+  rewrite stack_wire_distribute_r.
+  repeat rewrite ComposeRules.compose_assoc.
+  assert ((⨉ ↕ — ⟷ (— ↕ ⨉ ⟷ (⊃ ↕ —))) ∝ (— ↕ ⊃)) as Hrw. { shelve. }
+  rewrite Hrw; clear Hrw.
+  rewrite (stack_assoc zx1).
+  zx_simpl.
+  bundle_wires.
+  rewrite <- (stack_compose_distr zx1 —).
+  zx_simpl.
+  easy.
+Unshelve.
+  all: try lia.
+  solve_prop 1.
+Qed.

src/CoreRules/CastRules.v

@@ -146,7 +146,7 @@ Proof.
 Qed.
 
 Lemma cast_compose_distribute :
-  forall n n' m o o' prfn prfo (zx0 : ZX n m) (zx1 : ZX m o),
+  forall {n} n' {m o} o' prfn prfo (zx0 : ZX n m) (zx1 : ZX m o),
   cast n' o' prfn prfo (zx0 ⟷ zx1) ∝
   cast n' m prfn eq_refl zx0 ⟷ cast m o' eq_refl prfo zx1.
 Proof.
@@ -156,6 +156,18 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma cast_compose_distribute_general :
+  forall {n} n' {m} m' {o} o' prfn prfm prfo (zx0 : ZX n m) (zx1 : ZX m o),
+  cast n' o' prfn prfo (zx0 ⟷ zx1) ∝
+  cast n' m' prfn prfm zx0 ⟷ cast m' o' prfm prfo zx1.
+Proof.
+  intros.
+  subst.
+  simpl_casts.
+  reflexivity.
+Qed.
+
+
 Lemma cast_compose_l :
   forall {n n' m m' o} prfn prfm (zx0 : ZX n m) (zx1 : ZX m' o),
     cast n' m' prfn prfm zx0 ⟷ zx1 ∝ 

src/CoreRules/ComposeRules.v

@@ -110,4 +110,4 @@ Proof.
   rewrite n_wire_semantics.
   Msimpl.
   reflexivity.
-Qed.
+Qed.

src/CoreRules/CoreAutomation.v

@@ -39,6 +39,8 @@ Tactic Notation "bundle_wires" := wire_to_n_wire_safe; (* change wires to n_wire
   (fun n m o p => @nwire_stack_compose_topleft n m o p)
   (fun n m o p => @nwire_stack_compose_botleft n m o p)
   : cleanup_zx_db.
+#[export] Hint Rewrite <- nstack1_compose : cleanup_zx_db.
+#[export] Hint Rewrite <- nstack_compose : cleanup_zx_db.
 Tactic Notation "cleanup_zx" := auto_cast_eqn (autorewrite with cleanup_zx_db).
 
 #[export] Hint Rewrite
@@ -62,3 +64,5 @@ Tactic Notation "cleanup_zx" := auto_cast_eqn (autorewrite with cleanup_zx_db).
 Ltac transpose_of H := intros; apply transpose_diagrams; repeat (simpl; autorewrite with transpose_db); apply H.
 Ltac adjoint_of H := intros; apply adjoint_diagrams; repeat (simpl; autorewrite with adjoint_db); apply H.
 Ltac colorswap_of H := intros; apply colorswap_diagrams; repeat (simpl; autorewrite with colorswap_db); apply H.
+
+Ltac zx_simpl := simpl; repeat (cleanup_zx; simpl_casts).