Skip to content
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.

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

Fixed Ingest.v #37

Closed
wants to merge 50 commits into from
Closed
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
86c6e2b
Fixed Ingest.v
caldwellb Mar 25, 2023
17f3197
Updated coq-action.yml
caldwellb Apr 5, 2023
d041c3b
Add n_swap_semantics and fill in a_swap_semantics_ind
adrianleh Apr 5, 2023
a5da012
Finish up hopf rule
adrianleh Apr 5, 2023
2dca2a4
Improve name checking hook to check more names and ask for reasons to…
adrianleh Apr 5, 2023
fa28797
Add cnot_involutive and cnot_is_cnot_r
adrianleh Apr 10, 2023
05a7585
Clean up gate rules
adrianleh Apr 10, 2023
0f2c6ae
n_swap progress
caldwellb Apr 10, 2023
bcd3db2
b_swap!
adrianleh Apr 10, 2023
18ad74e
Add cast_fn_eq_dim het proofs
adrianleh Apr 19, 2023
c41f24b
Fix cast_fn_eq_dim usage
adrianleh Apr 19, 2023
d40fc3a
Nice cast tools
caldwellb Apr 19, 2023
326f5bc
Add bottom_to_top_grow_l and top_to_bottom_grow_r
adrianleh Apr 19, 2023
b1d45d3
Fix opaqueness breaking proofs
adrianleh Apr 20, 2023
ae6607d
Add n_cup_helper_grow_l
adrianleh Apr 20, 2023
40c68d5
Refactor cast for proofs to be explicit
adrianleh Apr 21, 2023
65dcbc1
Auto solve shelved cast goals
adrianleh Apr 21, 2023
0c59bf1
Refactor more parametric cast proof
adrianleh Apr 21, 2023
b3741b9
Add simpl_casts_in tactic
adrianleh Apr 21, 2023
2469ad2
rename cast parameters to fit convention
adrianleh Apr 21, 2023
5ccd82b
Add bundle_wires tactic
adrianleh Apr 27, 2023
e0a5aed
Progress to n_wrap_under
adrianleh Apr 28, 2023
c69a59e
Add {Z,X}_n_wrap_over_r_base_unswapped
adrianleh Apr 28, 2023
d3019b2
Add left versions of n_wrap
adrianleh Apr 28, 2023
7e1ac55
Add ZX_semantics notation "⟦ zx ⟧"
adrianleh May 11, 2023
3243e52
Add bell
adrianleh Jun 30, 2023
d3b720a
Simplify bell proof
adrianleh Jun 30, 2023
0ffa336
Remove broken example
adrianleh Jul 2, 2023
aa7e9c4
Add completeness.v
adrianleh Jul 7, 2023
bdd5d3c
Take .Old out back
adrianleh Jul 10, 2023
9e0ea5b
Getting started on the Harny completeness result.
caldwellb Oct 4, 2023
4918a35
Fixed naming, changed harny var defs
caldwellb Oct 9, 2023
e30b0ad
Add Harny_k
adrianleh Oct 9, 2023
ec1d619
Improve harny readability
adrianleh Oct 9, 2023
d7c59fb
Add Rsqrt
adrianleh Oct 9, 2023
19aab14
Added Csqrt
caldwellb Oct 9, 2023
93320f8
Updated to add Csqrt usage
caldwellb Oct 9, 2023
6bbe4b4
Add harny_simpl
adrianleh Oct 10, 2023
7af39c6
Updated Harny scalars to Complex numbers
caldwellb Oct 10, 2023
81a8d60
Restoring removed harny_db
caldwellb Oct 11, 2023
5d490cb
harny_completeness can use harny_general
caldwellb Oct 11, 2023
7747a8e
Completeness_BW finished
caldwellb Oct 13, 2023
6a0c19d
Partially completed Nancy completeness result
caldwellb Oct 17, 2023
4dca679
Nancy completeness result complete
caldwellb Oct 20, 2023
0e67006
Completeness_C done
caldwellb Oct 29, 2023
183ff5b
Cleanup completeness, separated computational rules
caldwellb Nov 13, 2023
825577b
Merge pull request #39 from inQWIRE/completeness
caldwellb Nov 13, 2023
ffe315b
Update README.md
caldwellb Nov 13, 2023
adf56de
Merge pull request #41 from inQWIRE/caldwellb-patch-1
caldwellb Nov 13, 2023
03e2cdf
Fix deprecation warnings in SemanticCore.
adrianleh Jan 15, 2024
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
Prev Previous commit
Next Next commit
Completeness_BW finished
  • Loading branch information
caldwellb committed Oct 13, 2023
commit 7747a8e231cfc9866464598dab2d51f0293f2c6d
210 changes: 210 additions & 0 deletions src/CoreData/QlibTemp.v
Original file line number Diff line number Diff line change
Expand Up @@ -167,3 +167,213 @@ Definition Csqrt (z : C) : C :=
end.

Notation "√ z" := (Csqrt z) : C_scope.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultplus0 :
⟨+∣ × ∣0⟩ = / (√2)%R .* I 1.
Proof.
unfold braplus.
rewrite Mscale_mult_dist_l.
rewrite Mmult_plus_distr_r.
rewrite Mmult00.
rewrite Mmult10.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmult0plus :
⟨0∣ × ∣+⟩ = / (√2)%R .* I 1.
Proof.
unfold xbasis_plus.
rewrite Mscale_mult_dist_r.
rewrite Mmult_plus_distr_l.
rewrite Mmult00.
rewrite Mmult01.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultplus1 :
⟨+∣ × ∣1⟩ = / (√2)%R .* I 1.
Proof.
unfold braplus.
rewrite Mscale_mult_dist_l.
rewrite Mmult_plus_distr_r.
rewrite Mmult01.
rewrite Mmult11.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmult1plus :
⟨1∣ × ∣+⟩ = / (√2)%R .* I 1.
Proof.
unfold xbasis_plus.
rewrite Mscale_mult_dist_r.
rewrite Mmult_plus_distr_l.
rewrite Mmult10.
rewrite Mmult11.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultminus0 :
⟨-∣ × ∣0⟩ = / (√2)%R .* I 1.
Proof.
unfold braminus.
rewrite Mscale_mult_dist_l.
rewrite Mmult_plus_distr_r.
rewrite Mmult00.
rewrite Mscale_mult_dist_l.
rewrite Mmult10.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmult0minus :
⟨0∣ × ∣-⟩ = / (√2)%R .* I 1.
Proof.
unfold xbasis_minus.
rewrite Mscale_mult_dist_r.
rewrite Mmult_plus_distr_l.
rewrite Mmult00.
rewrite Mscale_mult_dist_r.
rewrite Mmult01.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultminus1 :
⟨-∣ × ∣1⟩ = - / (√2)%R .* I 1.
Proof.
unfold braminus.
rewrite Mscale_mult_dist_l.
rewrite Mmult_plus_distr_r.
rewrite Mmult01.
rewrite Mscale_mult_dist_l.
rewrite Mmult11.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmult1minus :
⟨1∣ × ∣-⟩ = - / (√2)%R .* I 1.
Proof.
unfold xbasis_minus.
rewrite Mscale_mult_dist_r.
rewrite Mmult_plus_distr_l.
rewrite Mmult10.
rewrite Mscale_mult_dist_r.
rewrite Mmult11.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultminusminus :
⟨-∣ × ∣-⟩ = I 1.
Proof.
unfold braminus.
unfold xbasis_minus.
repeat rewrite Mscale_mult_dist_l.
repeat rewrite Mscale_mult_dist_r.
repeat rewrite Mmult_plus_distr_r.
repeat rewrite Mmult_plus_distr_l.
autorewrite with scalar_move_db.
rewrite Mmult00.
rewrite Mmult01.
rewrite Mmult10.
rewrite Mmult11.
Msimpl.
autorewrite with scalar_move_db.
solve_matrix.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultplusminus :
⟨+∣ × ∣-⟩ = Zero.
Proof.
unfold xbasis_minus.
unfold braplus.
repeat rewrite Mscale_mult_dist_l.
repeat rewrite Mscale_mult_dist_r.
repeat rewrite Mmult_plus_distr_r.
repeat rewrite Mmult_plus_distr_l.
autorewrite with scalar_move_db.
rewrite Mmult00.
rewrite Mmult01.
rewrite Mmult10.
rewrite Mmult11.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultminusplus :
⟨-∣ × ∣+⟩ = Zero.
Proof.
unfold xbasis_plus.
unfold braminus.
repeat rewrite Mscale_mult_dist_l.
repeat rewrite Mscale_mult_dist_r.
repeat rewrite Mmult_plus_distr_r.
repeat rewrite Mmult_plus_distr_l.
autorewrite with scalar_move_db.
rewrite Mmult00.
rewrite Mmult01.
rewrite Mmult10.
rewrite Mmult11.
Msimpl.
lma.
Qed.

(* @nocheck name *)
(* Conventional name *)
Lemma Mmultplusplus :
⟨+∣ × ∣+⟩ = I 1.
Proof.
unfold xbasis_plus.
unfold braplus.
repeat rewrite Mscale_mult_dist_l.
repeat rewrite Mscale_mult_dist_r.
repeat rewrite Mmult_plus_distr_r.
repeat rewrite Mmult_plus_distr_l.
autorewrite with scalar_move_db.
rewrite Mmult00.
rewrite Mmult01.
rewrite Mmult10.
rewrite Mmult11.
solve_matrix.
Qed.

#[export] Hint Rewrite
Mmult00 Mmult01 Mmult10 Mmult11
Mmultplus0 Mmultplus1 Mmultminus0 Mmultminus1
Mmult0plus Mmult0minus Mmult1plus Mmult1minus
Mmultplusplus Mmultplusminus Mmultminusplus Mmultminusminus
: ketbra_mult_db.

Lemma bra0transpose :
⟨0∣⊤ = ∣0⟩.
Proof. solve_matrix. Qed.

Lemma bra1transpose :
⟨1∣⊤ = ∣1⟩.
Proof. solve_matrix. Qed.

Lemma ket0transpose :
∣0⟩⊤ = ⟨0∣.
Proof. solve_matrix. Qed.

Lemma ket1transpose :
∣1⟩⊤ = ⟨1∣.
Proof. solve_matrix. Qed.
Loading