Skip to content

Updates/absolute fusion example #62

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
wjbs merged 2 commits into from
Oct 25, 2025
Merged

Updates/absolute fusion example #62

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e3a4ed7
Updated README for visualizer
caldwellb Oct 14, 2025
77391ad
Updated Z_absolute_fusion_
caldwellb Oct 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,14 @@ Finally, build VyZX:
make
```

## Using the visualizer

To use the integrated visualization, two things will need to be installed and you must be using VSCode.

First, install [rocq-lsp](https://github.com/ejgallego/rocq-lsp) and install the associated VSCode extension.

Then install our VSCode extension, [ZXViz](https://marketplace.visualstudio.com/items?itemName=inQWIRE.vizx). It can also be built from source following the instructions [here](https://github.com/inQWIRE/ViZX/).

## Contributing

To contribute please make sure you use our validator hooks.
Expand Down
55 changes: 19 additions & 36 deletions src/CoreData/ZXCore.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,9 +190,9 @@
Definition n_wire := fun n => n ↑ Wire.
Definition n_box := fun n => n ↑ Box.

#[global]

Check warning on line 193 in src/CoreData/ZXCore.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 193 in src/CoreData/ZXCore.v

View workflow job for this annotation

GitHub Actions / build (8.20, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments n_wire !_%nat_scope /.
#[global]

Check warning on line 195 in src/CoreData/ZXCore.v

View workflow job for this annotation

GitHub Actions / build (8.19, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use

Check warning on line 195 in src/CoreData/ZXCore.v

View workflow job for this annotation

GitHub Actions / build (8.20, default) 

The '%' scope delimiter in 'Arguments' commands is deprecated, use
Arguments n_box !_%nat_scope /.

Lemma n_wire_semantics {n} : ⟦ n_wire n ⟧ = I (2^n).
Expand Down Expand Up @@ -221,7 +221,7 @@

(* Transpose of a diagram *)

Reserved Notation "zx ⊤" (at level 0). (* \top *)

Check warning on line 224 in src/CoreData/ZXCore.v

View workflow job for this annotation

GitHub Actions / build (8.20, default) 

Postfix notations (i.e. starting with a nonterminal symbol and
Fixpoint transpose {nIn nOut} (zx : ZX nIn nOut) : ZX nOut nIn :=
match zx with
| ⦰ => ⦰
Expand All @@ -237,7 +237,7 @@

(* Negating the angles of a diagram, complex conjugate *)

Reserved Notation "zx ⊼" (at level 0). (* \barwedge *)

Check warning on line 240 in src/CoreData/ZXCore.v

View workflow job for this annotation

GitHub Actions / build (8.20, default) 

Postfix notations (i.e. starting with a nonterminal symbol and
Fixpoint conjugate {n m} (zx : ZX n m) : ZX n m :=
match zx with
| Z n m α => Z n m (-α)
Expand Down Expand Up @@ -384,44 +384,27 @@
⟦ (Z_Spider nIn 1 α) ⟷ (Z_Spider 1 nOut β) ⟧ =
⟦ Z_Spider nIn nOut (α + β) ⟧.
Proof.
assert (expnonzero : forall a, exists b, (2 ^ a + (2 ^ a + 0) - 1)%nat = S b).
{
intros.
destruct (2^a)%nat eqn:E.
- contradict E.
apply Nat.pow_nonzero; easy.
- simpl.
rewrite <- plus_n_Sm.
exists (n + n)%nat.
lia.
}
intros.
prep_matrix_equality.
rewrite 2 ZX_semantic_equiv.
simpl.
unfold Mmult.
simpl.
rewrite Cplus_0_l.
destruct nIn, nOut.
- simpl.
destruct x,y; [simpl; autorewrite with Cexp_db | | | ]; lca.
- destruct x,y; simpl; destruct (expnonzero nOut);
rewrite H; [ lca | lca | | ].
+ destruct (x =? x0)%nat.
* simpl.
autorewrite with Cexp_db.
lca.
* simpl.
lca.
+ destruct (x =? x0)%nat; lca.
- destruct x,y; simpl; destruct (expnonzero nIn);
rewrite H; [lca | | lca | lca].
+ destruct (y =? x)%nat; [autorewrite with Cexp_db | ]; lca.
- destruct x,y; simpl; destruct (expnonzero nIn), (expnonzero nOut);
rewrite H,H0; [lca | lca | | ].
+ destruct (x =? x1)%nat; lca.
+ destruct (x =? x1)%nat, (y =? x0)%nat; [| lca | lca | lca].
autorewrite with Cexp_db.
lca.
Msimpl.
restore_dims.
autorewrite with scalar_move_db.
repeat rewrite Mmult_plus_distr_l.
repeat rewrite Mmult_plus_distr_r.
autorewrite with scalar_move_db.
restore_dims.
repeat rewrite Mmult_assoc.
restore_dims.
repeat rewrite <- (Mmult_assoc ⟨0∣).
repeat rewrite <- (Mmult_assoc ⟨1∣).
repeat rewrite Mmult00, Mmult10, Mmult01, Mmult11.
Msimpl.
restore_dims.
Msimpl.
autorewrite with scalar_move_db.
rewrite Cexp_add.
reflexivity.
Qed.

Lemma z_1_1_pi_σz :
Expand Down
Loading