diff --git a/coq-vyzx.opam b/coq-vyzx.opam index 3f1cf83..86fc67e 100644 --- a/coq-vyzx.opam +++ b/coq-vyzx.opam @@ -13,9 +13,9 @@ homepage: "https://github.com/inQWIRE/VyZX" bug-reports: "https://github.com/inQWIRE/VyZX/issues" depends: [ "dune" {>= "2.8"} - "coq-quantumlib" {>= "1.3.0"} - "coq-sqir" {>= "1.3.0"} - "coq-voqc" {>= "1.3.0"} + "coq-quantumlib" {>= "1.6.0"} + "coq-sqir" {>= "1.3.2"} + "coq-voqc" {>= "1.3.2"} "coq" {>= "8.16"} "odoc" {with-doc} ] diff --git a/src/CoreData/Proportional.v b/src/CoreData/Proportional.v index 1a17209..d469e12 100644 --- a/src/CoreData/Proportional.v +++ b/src/CoreData/Proportional.v @@ -13,85 +13,704 @@ Definition proportional_general {T_0 m_0 n_0 T_1 m_1 n_1} (eval_1 : T_1 -> (Matrix m_1 n_1)) (t_0 : T_0) (t_1 : T_1) := exists (c : C), eval_0 t_0 = c .* eval_1 t_1 /\ c <> 0. -Notation " t1 '≡' t2 'by' eval" := - (proportional_general eval eval t1 t2) (at level 70). (* \equiv *) (* ZX Proportionality *) +Definition proportional_by {n m} (c : C) (zx0 zx1 : ZX n m) := + ⟦ zx0 ⟧ = c .* ⟦ zx1 ⟧ /\ c <> C0. + +Definition proportional_by_1 {n m} (zx0 zx1 : ZX n m) := + ⟦ zx0 ⟧ = ⟦ zx1 ⟧. + +Notation "zx0 '∝[' c ']' zx1" := + (proportional_by c%C zx0 zx1) (at level 70) : ZX_scope. + +Notation "zx0 '∝=' zx1" := + (proportional_by_1 zx0 zx1) (at level 70) : ZX_scope. + +Lemma proportional_by_1_defn {n m} (zx0 zx1 : ZX n m) : + zx0 ∝= zx1 <-> zx0 ∝[1] zx1. +Proof. + unfold proportional_by, proportional_by_1. + rewrite Mscale_1_l. + pose proof C1_nonzero. + intuition auto. +Qed. + +Lemma proportional_by_1_refl {n m} (zx0 : ZX n m) : + zx0 ∝= zx0. +Proof. + unfold proportional_by_1. + reflexivity. +Qed. + +Lemma proportional_by_1_sym {n m} (zx0 zx1 : ZX n m) : + zx0 ∝= zx1 -> zx1 ∝= zx0. +Proof. + unfold proportional_by_1. + now intros ->. +Qed. + +Lemma proportional_by_1_trans {n m} (zx0 zx1 zx2 : ZX n m) : + zx0 ∝= zx1 -> zx1 ∝= zx2 -> zx0 ∝= zx2. +Proof. + unfold proportional_by_1. + now intros -> ->. +Qed. + + +Add Parametric Relation n m : (ZX n m) (proportional_by_1) + reflexivity proved by proportional_by_1_refl + symmetry proved by proportional_by_1_sym + transitivity proved by proportional_by_1_trans + as proportional_by_1_setoid. + +Add Parametric Morphism n m o : (@Compose n m o) with signature + proportional_by_1 ==> proportional_by_1 ==> proportional_by_1 + as compose_prop_by_1_proper. +Proof. + unfold proportional_by_1. + cbn [ZX_semantics]. + congruence. +Qed. + +Add Parametric Morphism n m o p : (@Stack n m o p) with signature + proportional_by_1 ==> proportional_by_1 ==> proportional_by_1 + as stack_prop_by_1_proper. +Proof. + unfold proportional_by_1. + cbn [ZX_semantics]. + congruence. +Qed. + +Add Parametric Morphism n m n' m' prfn prfm : (@cast n' m' n m prfn prfm) + with signature proportional_by_1 ==> proportional_by_1 as + cast_prop_by_1_proper. +Proof. + unfold proportional_by_1. + intros ? ? ?. + now simpl_cast_semantics. +Qed. + +Add Parametric Morphism n m : (@transpose n m) with signature + proportional_by_1 ==> proportional_by_1 as + transpose_prop_by_1_proper. +Proof. + intros zx0 zx1. + unfold proportional_by_1. + rewrite 2!semantics_transpose_comm. + now intros ->. +Qed. + +Add Parametric Morphism n m : (@color_swap n m) with signature + proportional_by_1 ==> proportional_by_1 as + colorswap_prop_by_1_proper. +Proof. + intros zx0 zx1. + unfold proportional_by_1. + rewrite 2!semantics_colorswap_comm. + now intros ->. +Qed. + +Add Parametric Morphism n m : (@adjoint n m) with signature + proportional_by_1 ==> proportional_by_1 as + adjoint_prop_by_1_proper. +Proof. + intros zx0 zx1. + unfold proportional_by_1. + rewrite 2!semantics_adjoint_comm. + now intros ->. +Qed. + +Add Parametric Morphism n m : (@conjugate n m) with signature + proportional_by_1 ==> proportional_by_1 as + conjugate_prop_by_1_proper. +Proof. + intros zx0 zx1. + unfold proportional_by_1. + rewrite 2!semantics_conjugate_comm. + now intros ->. +Qed. + +Add Parametric Morphism n m k : (@n_stack n m k) with signature + proportional_by_1 ==> proportional_by_1 as + nstack_prop_by_1_proper. +Proof. + intros zx0 zx1 H. + induction k; [reflexivity|]. + cbn [n_stack]. + apply stack_prop_by_1_proper; auto. +Qed. + +Add Parametric Morphism k : (@n_stack1 k) with signature + proportional_by_1 ==> proportional_by_1 as + nstack1_prop_by_1_proper. +Proof. + intros zx0 zx1 H. + induction k; [reflexivity|]. + cbn [n_stack]. + apply stack_prop_by_1_proper; auto. +Qed. + +Add Parametric Morphism n m c : (@proportional_by n m c) with signature + proportional_by_1 ==> proportional_by_1 ==> iff + as proportional_by_proper_eq. +Proof. + unfold proportional_by, proportional_by_1. + now intros ? ? -> ? ? ->. +Qed. + +Lemma compose_prop_by_if_l {n m o} (zx0 zx1 : ZX n m) + (zx2 : ZX m o) (zx3 : ZX n o) c d : zx0 ∝[c] zx1 -> + zx0 ⟷ zx2 ∝[d] zx3 <-> zx1 ⟷ zx2 ∝[d / c] zx3. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + distribute_scale. + rewrite Mscale_inv by auto. + distribute_scale. + apply ZifyClasses.and_morph; [now rewrite Cmult_comm|]. + symmetry. + now apply Cdiv_nonzero_iff_r. +Qed. + +Lemma compose_prop_by_if_r {n m o} (zx0 : ZX n m) + (zx1 zx2 : ZX m o) (zx3 : ZX n o) c d : zx1 ∝[c] zx2 -> + zx0 ⟷ zx1 ∝[d] zx3 <-> zx0 ⟷ zx2 ∝[d / c] zx3. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + distribute_scale. + rewrite Mscale_inv by auto. + distribute_scale. + apply ZifyClasses.and_morph; [now rewrite Cmult_comm|]. + symmetry. + now apply Cdiv_nonzero_iff_r. +Qed. + +Lemma stack_prop_by_if_l {n m o p} (zx0 zx1 : ZX n m) + (zx2 : ZX o p) zx3 c d : zx0 ∝[c] zx1 -> + zx0 ↕ zx2 ∝[d] zx3 <-> zx1 ↕ zx2 ∝[d / c] zx3. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + restore_dims. + distribute_scale. + rewrite Mscale_inv by auto. + restore_dims. + distribute_scale. + apply ZifyClasses.and_morph; [now rewrite Cmult_comm|]. + symmetry. + now apply Cdiv_nonzero_iff_r. +Qed. + +Lemma stack_prop_by_if_r {n m o p} (zx0 : ZX n m) + (zx1 zx2 : ZX o p) zx3 c d : zx1 ∝[c] zx2 -> + zx0 ↕ zx1 ∝[d] zx3 <-> zx0 ↕ zx2 ∝[d / c] zx3. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + restore_dims. + distribute_scale. + rewrite Mscale_inv by auto. + restore_dims. + distribute_scale. + apply ZifyClasses.and_morph; [now rewrite Cmult_comm|]. + symmetry. + now apply Cdiv_nonzero_iff_r. +Qed. + + +Lemma compose_prop_by_compat_l {n m o} (zx0 zx1 : ZX n m) + (zx2 : ZX m o) c : zx0 ∝[c] zx1 -> + zx0 ⟷ zx2 ∝[c] zx1 ⟷ zx2. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + distribute_scale. + auto. +Qed. + +Lemma compose_prop_by_compat_r {n m o} (zx0 : ZX n m) + (zx1 zx2 : ZX m o) c : zx1 ∝[c] zx2 -> + zx0 ⟷ zx1 ∝[c] zx0 ⟷ zx2. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + distribute_scale. + auto. +Qed. + +Lemma stack_prop_by_compat_l {n m o p} (zx0 zx1 : ZX n m) + (zx2 : ZX o p) c : zx0 ∝[c] zx1 -> + zx0 ↕ zx2 ∝[c] zx1 ↕ zx2. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + distribute_scale. + auto. +Qed. + +Lemma stack_prop_by_compat_r {n m o p} (zx0 : ZX n m) + (zx1 zx2 : ZX o p) c : zx1 ∝[c] zx2 -> + zx0 ↕ zx1 ∝[c] zx0 ↕ zx2. +Proof. + unfold proportional_by. + cbn [ZX_semantics]. + intros [-> Hc]. + distribute_scale. + auto. +Qed. + +Lemma cast_prop_by_compat {n m n' m'} (zx0 zx1 : ZX n m) + prfn prfn' prfm prfm' c : zx0 ∝[c] zx1 -> + cast n' m' prfn prfm zx0 ∝[c] cast n' m' prfn' prfm' zx1. +Proof. + unfold proportional_by. + now simpl_cast_semantics. +Qed. + +Lemma transpose_prop_by_compat {n m} (zx0 zx1 : ZX n m) c : + zx0 ∝[c] zx1 -> + zx0 ⊤ ∝[c] zx1 ⊤. +Proof. + unfold proportional_by. + rewrite 2!semantics_transpose_comm. + intros [-> Hc]. + now rewrite Mscale_trans. +Qed. + +Lemma colorswap_prop_by_compat {n m} (zx0 zx1 : ZX n m) c : + zx0 ∝[c] zx1 -> + ⊙ zx0 ∝[c] ⊙ zx1. +Proof. + unfold proportional_by. + rewrite 2!semantics_colorswap_comm. + intros [-> Hc]. + now distribute_scale. +Qed. + +Lemma adjoint_prop_by_compat {n m} (zx0 zx1 : ZX n m) c : + zx0 ∝[c ^*] zx1 -> + zx0 † ∝[c] zx1 †. +Proof. + unfold proportional_by. + rewrite 2!semantics_adjoint_comm. + intros [-> Hc]. + rewrite Mscale_adj. + rewrite Cconj_involutive. + split; [reflexivity|]. + rewrite <- (Cconj_involutive c). + now apply Cconj_neq_0. +Qed. + + +Create HintDb zx_prop_by_db discriminated. +#[export] Hint Resolve + compose_prop_by_compat_l compose_prop_by_compat_r + stack_prop_by_compat_l stack_prop_by_compat_r + cast_prop_by_compat + transpose_prop_by_compat + adjoint_prop_by_compat + colorswap_prop_by_compat : zx_prop_by_db. + +(* For concrete examples with bad sizes *) +#[export] +Hint Extern 0 (?x ⟷ ?y ∝[?c] ?x ⟷ ?z) => + apply (compose_prop_by_compat_r x y z) : zx_prop_by_db. +#[export] +Hint Extern 0 (?x ⟷ ?y ∝[?c] ?z ⟷ ?y) => + apply (compose_prop_by_compat_l x z y) : zx_prop_by_db. +#[export] +Hint Extern 0 (?x ↕ ?y ∝[?c] ?x ↕ ?z) => + apply (stack_prop_by_compat_r x y z) : zx_prop_by_db. +#[export] +Hint Extern 0 (?x ↕ ?y ∝[?c] ?z ↕ ?y) => + apply (stack_prop_by_compat_l x z y) : zx_prop_by_db. + +Lemma eq_sym_iff {A} (a b : A) : a = b <-> b = a. +Proof. easy. Qed. + +Lemma proportional_by_trans_iff_l {n m} (zx0 zx1 zx2 : ZX n m) c d : + zx0 ∝[c] zx1 -> (zx0 ∝[d] zx2 <-> zx1 ∝[d / c] zx2). +Proof. + unfold proportional_by. + intros [-> Hc]. + rewrite Mscale_inv by auto. + distribute_scale. + apply ZifyClasses.and_morph; [now rewrite Cmult_comm|]. + rewrite Cdiv_nonzero_iff_r; + intuition auto. +Qed. + +Lemma proportional_by_trans_iff_r {n m} (zx0 zx1 zx2 : ZX n m) c d : + zx1 ∝[c] zx2 -> (zx0 ∝[d] zx1 <-> zx0 ∝[d * c] zx2). +Proof. + unfold proportional_by. + intros [-> Hc]. + distribute_scale. + apply ZifyClasses.and_morph; [reflexivity|]. + rewrite Cmult_nonzero_iff; + intuition auto. +Qed. + +Lemma proportional_by_sym {n m} {zx0 zx1 : ZX n m} {c} : + zx0 ∝[c] zx1 -> zx1 ∝[/c] zx0. +Proof. + intros [Heq Hc]. + split. + - rewrite <- Mscale_inv by auto. + easy. + - rewrite Cinv_eq_0_iff. + apply Hc. +Qed. + +Lemma proportional_by_sym_iff {n m} {zx0 zx1 : ZX n m} {c} : + zx0 ∝[c] zx1 <-> zx1 ∝[/c] zx0. +Proof. + split; [apply proportional_by_sym|]. + intros H%proportional_by_sym. + rewrite Cinv_inv in H. + exact H. +Qed. + +Lemma proportional_by_sym_div_iff {n m} {zx0 zx1 : ZX n m} {c d} : + zx0 ∝[c / d] zx1 <-> zx1 ∝[d / c] zx0. +Proof. + rewrite proportional_by_sym_iff, Cinv_div. + reflexivity. +Qed. + + + + + +(** Taken from stdpp: + +The tactic [eunify x y] succeeds if [x] and [y] can be unified, and fails +otherwise. If it succeeds, it will instantiate necessary evars in [x] and [y]. + +Contrary to Coq's standard [unify] tactic, which uses [constr] for the arguments +[x] and [y], [eunify] uses [open_constr] so that one can use holes (i.e., [_]s). +For example, it allows one to write [eunify x (S _)], which will test if [x] +unifies a successor. *) +Tactic Notation "eunify" uconstr(x) uconstr(y) := + unify x y. + +(** Given a term [dom], an open term [tgt], and a tactic [test], + attempt to find a subterm of [dom] that unifies with [tgt]. + May fill evars of [tgt]. If such a subterm is found, + return a function mapping a term [x] with the type of [tgt] to + the term replacing the matched subterm of [dom] with [x]. + [test] is used to filter matched subterms: when a subterm [y] is + found to match [tgt], [test] is called with argument [y]. If [test] + raises an error, this match is discarded and another tried. + *) +Ltac epat_func_test dom tgt test := + let rec epat dom tgt := + match dom with + | ?x => + let _ := lazymatch goal with _ => + (* idtac "1:" x tgt; *) + eunify x tgt; test x + (* ;idtac "PASS" *) end in + let T := type of dom in + constr:(fun a : T => a) + | ?f ?x => + let r := epat x tgt in + (* let _ := match goal with _ => + (* idtac "2:" f x tgt; *) + eunify x tgt; + test x + (* ;idtac "PASS" *) end in *) + constr:(fun t => f (r t)) + | ?f ?x => + let r := epat f tgt in + (* let _ := match goal with _ => idtac "3:" r x end in *) + constr:((fun t => r t x)) + end in + epat dom tgt. + +(** Given a term [dom] and an open term [tgt], attempt to find a + subterm of [dom] that unifies with [tgt]. May fill evars of [tgt]. + If such a subterm is found, return a function mapping a term [x] + with the type of [tgt] to the term replacing the matched subterm + of [dom] with [x]. See [epat_func_test] for a version that filters + matched subterms. *) +Ltac epat_func dom tgt := + let r := epat_func_test dom tgt ltac:(fun k => idtac) in + let r' := eval cbn beta in r in + constr:(r'). + +(** Given a lemma statement [lem], give an [open_constr] which + fills in all dependent arguments before the first non-dependent + argument with [evar]s. + For example, think of [lem] as having type + [forall (x : A) (y : B) ..., Q x y ... -> ... -> P x y ...]. + In this example, it would return a term (lem _ _ ...) of type + [Q ?[x] ?[y] ... -> ... -> P ?[x] ?[y] ...]. + NB that any depending arguments after [Q] would not be filled. +*) +Ltac fill_lem_args_dep lem := + match type of lem with + | ?A -> ?B => constr:(lem) + | forall a : ?A, _ => + let lapp := open_constr:(lem _) in + let r := fill_lem_args_dep lapp in + constr:(r) + | ?T => constr:(lem) + end. + +(** Given a lemma statement [lem], give an [open_constr] + which fills in all arguments with [evar]s. + For example, think of [lem] as having type + [forall (x : A) (y : B) ..., Q x y ... -> + ... -> forall ... -> ... -> P x y ...]) + In that case, it would return a term (lem _ _ ...) of type + [P ?[x] ?[y] ...], having filled in [Q] and all other arguments. +*) +Ltac fill_lem_args lem := + match type of lem with + | forall a : ?A, _ => + let lapp := open_constr:(lem _) in + let r := fill_lem_args lapp in + constr:(r) + | ?T => constr:(lem) + end. + + +(** Given a [constr] [H] of type [rwsrc ∝[c] rwtgt], rewrites [H] + in a goal [LHS ∝[d] RHS]. It matches topdown, trying first to match + [rwsrc] with a subterm of [LHS], then of [RHS]. Given a match, + it reconstructs a statement reducing the goal to a goal replacing + the subterm with [rwtgt] (and necessarily changing the constant [d]) + using [auto with zx_prop_by_db]. *) +Ltac zxrw_one H := + match type of H with + | ?rwsrc ∝[ ?rwfac ] ?rwtgt => + let Hrw := fresh "Hrw" in + match goal with + | |- ?zxL ∝[ ?fac ] ?zxR => + let Lpat := eval pattern rwsrc in zxL in + lazymatch Lpat with + | (fun _ => ?P) _ => let r := constr:(P) in fail + | (fun x => @?P x) _ => + let rwt := eval cbn beta in (P rwsrc ∝[rwfac] P rwtgt) in + assert (Hrw : rwt) by auto 100 using H with zx_prop_by_db nocore; + apply <- (proportional_by_trans_iff_l _ _ zxR rwfac fac Hrw); + clear Hrw + end + | |- ?zxL ∝[ ?fac ] ?zxR => + let Rpat := eval pattern rwsrc in zxR in + lazymatch Rpat with + | (fun _ => ?P) _ => let r := constr:(P) in fail + | (fun x => @?P x) _ => + let rwt := eval cbn beta in (P rwsrc ∝[rwfac] P rwtgt) in + assert (Hrw : rwt) by auto 100 using H with zx_prop_by_db nocore; + apply <- (proportional_by_trans_iff_r zxL _ _ rwfac fac Hrw); + clear Hrw + end + end + end. + +(** Given an [open_constr] [H] of type [rwsrc ∝[c] rwtgt], possibly + containing [evar] holes, rewrites [H] in a goal [LHS ∝[d] RHS]. + It matches topdown, trying first to match [rwsrc] with a subterm + of [LHS], then of [RHS]. Given a match, it reconstructs a statement + reducing the goal to a goal replacing the subterm with [rwtgt] (and + necessarily changing the constant [d]) using [auto with zx_prop_by_db]. *) +Ltac zxrw_one_open H := + lazymatch type of H with + | ?rwsrc ∝[ ?rwfac ] ?rwtgt => + let Hrw := fresh "Hrw" in + match goal with + | |- ?zxL ∝[ ?fac ] ?zxR => + let Lpat := epat_func zxL rwsrc in + let P := Lpat in + let rwtbase := open_constr:(P rwsrc ∝[_] P rwtgt) in + let rwt := eval cbn beta in rwtbase in + assert (Hrw : rwt) by eauto 100 using H with zx_prop_by_db nocore; + apply <- (proportional_by_trans_iff_l _ _ zxR _ fac Hrw); + clear Hrw + | |- ?zxL ∝[ ?fac ] ?zxR => + let Rpat := epat_func zxR rwsrc in + let P := Rpat in + let rwtbase := open_constr:(P rwsrc ∝[_] P rwtgt) in + let rwt := eval cbn beta in rwtbase in + assert (Hrw : rwt) by eauto 100 using H with zx_prop_by_db nocore; + apply <- (proportional_by_trans_iff_r zxL _ _ _ fac Hrw); + clear Hrw + end + end. + +Lemma proportional_by_refl_iff {n m} (zx0 zx1 : ZX n m) c : + c = C1 -> + zx0 ∝[c] zx1 <-> zx0 ∝= zx1. +Proof. + intros ->. + now rewrite proportional_by_1_defn. +Qed. + +(** The tactic used by [zxrefl] to solve the [c = 1] side-condition, + by default [try (now C_field)]. + Redefine ([Ltac zxrefl_tac ::= ...]) to change behavior. *) +Ltac zxrefl_tac := try (now C_field). + +(** On a goal of type [LHS ∝[c] RHS], replaces it with two goals, + [c = 1] and [LHS ∝= RHS]. It attempts to solve the first with + [zxrefl_tac] (by default, [try (now C_field)]) and attempts to + solve the second with reflexivity. *) +Ltac zxrefl := + apply proportional_by_refl_iff; + [(repeat match goal with + | H : _ ∝[_] _ |- _ => destruct H as [? ?] + end); zxrefl_tac + | try reflexivity]. + +(** On a goal of type [LHS ∝[c] RHS], replace this by symmetry with + [RHS ∝[d] LHS], where [d] is chosen somewhat intelligently. + Specifically, if [c = / c0] then we take [d = c0], + if [c = c0 / c1] then we take [d = c1 / c0], and + otherwise we take [d = / c]. *) +Ltac zxsymmetry := + lazymatch goal with + | |- proportional_by (Cinv _) _ _ => refine (proportional_by_sym _) + | |- proportional_by (Cdiv _ _) _ _ => + refine (proj1 proportional_by_sym_div_iff _) + | |- proportional_by _ _ _ => + refine (proj2 proportional_by_sym_iff _) + | |- _ => fail 0 "Goal is not of form '_ ∝[_] _'" + end. + +(** Given a hypothesis [H] of type [LHS ∝[c] RHS], replace this + by symmetry with [RHS ∝[d] LHS], where [d] is chosen + somewhat intelligently. + Specifically, if [c = / c0] then we take [d = c0], + if [c = c0 / c1] then we take [d = c1 / c0], and + otherwise we take [d = / c]. *) +Ltac zxsymmetry_in H := + lazymatch type of H with + | proportional_by (Cinv _) _ _ => + apply (proj2 proportional_by_sym_iff) in H + | proportional_by (Cdiv _ _) _ _ => + apply (proj1 proportional_by_sym_div_iff) in H + | proportional_by _ _ _ => + apply (proj2 proportional_by_sym_iff) in H + | _ => fail 0 "Hypothesis is not of form '_ ∝[_] _'" + end. + +(** Apply symmetry to the hypothesis [H] using [zxsymmetry_in]. + See [zxsymmetry_in] documentation for details. *) +Tactic Notation "zxsymmetry" "in" hyp(H) := + zxsymmetry_in H. + +(** Apply symmetry to the goal using [zxsymmetry]. See + [zxsymmetry] documentation for details. *) +Tactic Notation "zxsymmetry" := + zxsymmetry. + +(** Prepare a lemma [H] to be rewritten with by filling + all arguments with holes, and failing if [H] is not + seen to be of type [_ ∝[_] _] (after arguments are filled). *) +Ltac zxrw_prep H := + lazymatch type of H with + | _ ∝[_] _ => open_constr:(H) + | forall _, _ => zxrw_prep open_constr:(H _) + | ?T => fail 0 "Couldn't see lemma of type '" T + "' as a lemma of shape '_ ∝[_] _'" + end. + +(** Given a lemma [H : forall (...), rwsrc ∝[d] rwtgt], rewrite [H] + left-to-right in a goal of type [LHS ∝[c] RHS] using [zxrw_one_open], + having first checked it has the correct type and filled its arguments + with [evar] holes using [zxrw_prep]. *) +Tactic Notation "zxrewrite" open_constr(H) := + let H' := zxrw_prep H in + zxrw_one_open H'. + +(** Given a lemma [H : forall (...), rwsrc ∝[d] rwtgt], rewrite [H] + right-to-left in a goal of type [LHS ∝[c] RHS] using [zxrw_one_open], + having first checked it has the correct type and filled its arguments + with [evar] holes using [zxrw_prep]. *) +Tactic Notation "zxrewrite" "<-" open_constr(H) := + let H' := zxrw_prep H in + zxrw_one_open (proportional_by_sym H). + + + + + + + + + + + + + Definition proportional {n m} - (zx_0 : ZX n m) (zx_1 : ZX n m) := zx_0 ≡ zx_1 by ZX_semantics. + (zx_0 : ZX n m) (zx_1 : ZX n m) := exists c, zx_0 ∝[c] zx_1. Notation "zx0 ∝ zx1" := (proportional zx0 zx1) (at level 70) : ZX_scope. (* \propto *) +(** On a goal [exists c : C, ?P /\ c <> 0], give [c] as witness and try to + solve the [c <> 0] side-condition. For instance, [prop_exists_nonzero c] + on a goal [zx0 ∝ zx1] reduces the goal to [⟦zx0⟧ = c .* ⟦zx1⟧], + along with [c <> 0] if this is not solved automatically. *) Ltac prop_exists_nonzero c := - exists c; split; try apply nonzero_div_nonzero; try nonzero. -Ltac prep_proportional := unfold proportional; intros; split; [split; lia | ]. + exists c; split; [|repeat (apply nonzero_div_nonzero + + apply Cmult_neq_0); try nonzero; auto]. + +(** On a goal [zx0 ∝ zx1], replace this goal with + [⟦zx0⟧ = c .* ⟦zx1⟧] and try to solve that goal by brute force. + Specifically, simplify with [Msimpl] and unfolding Z/X semantics, + then use [solve_matrix] to brute-force a solution, and finally + [autorewrite with Cexp_db; lca] to solve any remaining goals. *) Ltac solve_prop c := prop_exists_nonzero c; simpl; Msimpl; unfold X_semantics; unfold Z_semantics; simpl; solve_matrix; autorewrite with Cexp_db; lca. - -Lemma proportional_general_refl : forall T n m eval (t : T), - @proportional_general T n m T n m eval eval t t. -Proof. prop_exists_nonzero 1; intros; lma. Qed. - -Lemma proportional_general_symm : - forall T_0 n_0 m_0 T_1 n_1 m_1 eval_0 eval_1 (t0 : T_0) (t1: T_1), - @proportional_general T_0 n_0 m_0 T_1 n_1 m_1 eval_0 eval_1 t0 t1 -> - @proportional_general T_1 n_1 m_1 T_0 n_0 m_0 eval_1 eval_0 t1 t0. +Lemma proportional_of_by_1 {n m} (zx0 zx1 : ZX n m) : zx0 ∝= zx1 -> + zx0 ∝ zx1. Proof. - intros. - destruct H. - exists (/x). - destruct H. - split. - - rewrite H. - Msimpl. - rewrite Mscale_assoc. - rewrite Cinv_l; try lma. - apply H0. - - apply nonzero_div_nonzero. - apply H0. -Qed. - -Lemma proportional_general_trans : - forall T_0 n_0 m_0 eval_0 (t0 : T_0) - T_1 n_1 m_1 eval_1 (t1 : T_1) - T_2 n_2 m_2 eval_2 (t2 : T_2), - @proportional_general T_0 n_0 m_0 T_1 n_1 m_1 eval_0 eval_1 t0 t1 -> - @proportional_general T_1 n_1 m_1 T_2 n_2 m_2 eval_1 eval_2 t1 t2 -> - @proportional_general T_0 n_0 m_0 T_2 n_2 m_2 eval_0 eval_2 t0 t2. -Proof. - intros. - destruct H. - destruct H. - destruct H0. - destruct H0. - exists (x * x0). - split. - - rewrite <- Mscale_assoc. - rewrite <- H0. - rewrite H. - reflexivity. - - apply Cmult_neq_0; try assumption. + intros H%proportional_by_1_defn. + now exists 1. Qed. +(** Reduces a goal [zx0 ∝ zx1] to [zx0 ∝= zx1]. Acts somewhat like + a refined version of [prop_exists_nonzero C1]. *) +Ltac zxprop_by_1 := + apply proportional_of_by_1. + Lemma proportional_refl : forall {n m} (zx : ZX n m), zx ∝ zx. -Proof. intros; apply proportional_general_refl. Qed. +Proof. intros; zxprop_by_1; reflexivity. Qed. Lemma proportional_symm : forall {n m} (zx_0 : ZX n m) (zx_1 : ZX n m), zx_0 ∝ zx_1 -> zx_1 ∝ zx_0. -Proof. intros; apply proportional_general_symm; apply H. Qed. +Proof. + intros * (c & Hzx & Hc). + prop_exists_nonzero (/ c). + rewrite <- Mscale_inv by auto. + easy. +Qed. Lemma proportional_trans : forall {n m} (zx0 : ZX n m) (zx1 : ZX n m) (zx2 : ZX n m), zx0 ∝ zx1 -> zx1 ∝ zx2 -> zx0 ∝ zx2. Proof. - intros. - apply (proportional_general_trans _ _ _ _ _ _ n m ZX_semantics zx1); - assumption. + intros * (c & Hzx01 & Hc) (d & Hzx12 & Hd). + prop_exists_nonzero (c * d). + rewrite Hzx01, Hzx12. + now distribute_scale. Qed. Add Parametric Relation (n m : nat) : (ZX n m) (proportional) @@ -100,6 +719,47 @@ Add Parametric Relation (n m : nat) : (ZX n m) (proportional) transitivity proved by proportional_trans as zx_prop_equiv_rel. +#[export] +Instance proportional_by_subrel n m c : + subrelation (@proportional_by n m c) (@proportional n m). +Proof. + intros zx0 zx1 H. + now exists c. +Qed. + + + +Add Parametric Morphism (n m : nat) (c : C) : (@proportional n m) with signature + proportional_by c ==> proportional_by_1 ==> iff as + proportional_proper_by_l. +Proof. + intros ? ? H0%proportional_by_subrel ? ? + H1%proportional_by_1_defn%proportional_by_subrel. + now rewrite H0, H1. +Qed. + +Add Parametric Morphism (n m : nat) (c : C) : (@proportional n m) with signature + proportional_by_1 ==> proportional_by c ==> iff as + proportional_proper_by_r. +Proof. + intros ? ? H0%proportional_by_1_defn%proportional_by_subrel ? ? + H1%proportional_by_subrel. + now rewrite H0, H1. +Qed. + +Add Parametric Morphism (n m : nat) : (@proportional n m) with signature + proportional_by_1 ==> proportional_by_1 ==> iff as + proportional_proper_by_1. +Proof. + intros ? ? H0%proportional_by_1_defn%proportional_by_subrel ? ? + H1%proportional_by_1_defn%proportional_by_subrel. + now rewrite H0, H1. +Qed. + + + + + Lemma stack_compat : forall n0 m0 n1 m1, forall (zx0 : ZX n0 m0) (zx2 : ZX n0 m0), zx0 ∝ zx2 -> @@ -107,10 +767,10 @@ Lemma stack_compat : zx0 ↕ zx1 ∝ zx2 ↕ zx3. Proof. intros n0 m0 n1 m1 zx0 zx2 [x [Hzx0 Hx]] zx1 zx3 [x0 [Hzx1 Hx0]]. - prop_exists_nonzero (x * x0); [ | (apply Cmult_neq_0; auto)]. + prop_exists_nonzero (x * x0). simpl. rewrite Hzx0, Hzx1. - lma. + now distribute_scale. Qed. Add Parametric Morphism (n0 m0 n1 m1 : nat) : Stack @@ -161,13 +821,13 @@ Add Parametric Morphism (n : nat) : (n_stack1 n) Proof. apply n_stack1_compat. Qed. Lemma compose_compat : - forall n m o, + forall {n m} o, forall (zx0 : ZX n m) (zx2 : ZX n m), zx0 ∝ zx2 -> forall (zx1 : ZX m o) (zx3 : ZX m o), zx1 ∝ zx3 -> zx0 ⟷ zx1 ∝ zx2 ⟷ zx3. Proof. intros n m o zx0 zx2 [x [Hzx0 Hx]] zx1 zx3 [x0 [Hzx1 Hx0]]. - prop_exists_nonzero (x * x0); [ | (apply Cmult_neq_0; auto)]. + prop_exists_nonzero (x * x0). simpl. rewrite Hzx0, Hzx1. rewrite Mscale_mult_dist_r. @@ -182,7 +842,7 @@ Add Parametric Morphism (n o m : nat) : Compose Proof. apply compose_compat; assumption. Qed. Lemma cast_compat : - forall n m n' m' prfn0 prfm0, + forall {n m} n' m' prfn0 prfm0, forall (zx0 : ZX n m) (zx1 : ZX n m), zx0 ∝ zx1 -> cast n' m' prfn0 prfm0 zx0 ∝ cast n' m' prfn0 prfm0 zx1. Proof. @@ -197,7 +857,7 @@ Add Parametric Morphism (n m : nat) {n' m' : nat} {prfn prfm} : (@cast n m n' m' Proof. apply cast_compat. Qed. Lemma transpose_compat : - forall n m, + forall {n m}, forall zx0 zx1 : ZX n m, zx0 ∝ zx1 -> (zx0⊤) ∝ (zx1⊤). Proof. @@ -216,7 +876,7 @@ Add Parametric Morphism (n m : nat) : transpose Proof. apply transpose_compat. Qed. Lemma adjoint_compat : - forall n m, + forall {n m}, forall (zx0 : ZX n m) (zx1 : ZX n m), zx0 ∝ zx1 -> (zx0 †) ∝ (zx1 †). Proof. @@ -232,18 +892,24 @@ Add Parametric Morphism (n m : nat) : (@adjoint n m) with signature (@proportional n m) ==> proportional as adj_mor. Proof. apply adjoint_compat. Qed. -Lemma colorswap_is_bihadamard : forall n m (zx : ZX n m), - ⊙ zx ∝ (n ↑ □) ⟷ (zx ⟷ (m ↑ □)). +Lemma colorswap_is_bihadamard : forall {n m} (zx : ZX n m), + ⊙ zx ∝= (n ↑ □) ⟷ (zx ⟷ (m ↑ □)). Proof. - prop_exists_nonzero 1. - Msimpl. - simpl. + intros n m zx. + unfold proportional_by_1. + cbn [ZX_semantics]. rewrite 2 n_stack1_n_kron. - simpl. rewrite semantics_colorswap_comm. easy. Qed. +Lemma colorswap_is_bihadamard_gen : forall {n m} (zx : ZX n m), + ⊙ zx ∝ (n ↑ □) ⟷ (zx ⟷ (m ↑ □)). +Proof. + intros n m zx. + now rewrite colorswap_is_bihadamard. +Qed. + Lemma colorswap_compat : forall nIn nOut, forall zx0 zx1 : ZX nIn nOut, zx0 ∝ zx1 -> @@ -263,143 +929,250 @@ Proof. apply colorswap_compat. Qed. Theorem sem_eq_prop : forall {n m} (zx0 : ZX n m) (zx1 : ZX n m), ⟦ zx0 ⟧ = ⟦ zx1 ⟧ -> zx0 ∝ zx1. Proof. - intros. - prop_exists_nonzero 1. - rewrite H; lma. + now intros n m zx0 zx1 ->%proportional_by_1_defn. Qed. (* Useful Lemmas *) -Lemma nstack1_transpose : forall n (zx : ZX 1 1), - (n ↑ zx)⊤ ∝ n ↑ (zx ⊤). +Lemma transpose_involutive_eq : forall {n m} (zx : ZX n m), + zx ⊤ ⊤ = zx. +Proof. + intros n m zx. + induction zx; [reflexivity.. | |]; + cbn; rewrite IHzx1, IHzx2; reflexivity. +Qed. + +Lemma adjoint_involutive_eq : forall {n m} (zx : ZX n m), + zx † † = zx. Proof. intros. - induction n. - - easy. - - simpl. - rewrite IHn. - reflexivity. + induction zx; [reflexivity.. | | | |]; + [cbn; now rewrite Ropp_involutive.. | |]; + cbn; now f_equal. Qed. -Lemma transpose_involutive : forall n m (zx : ZX n m), - zx ⊤ ⊤ ∝ zx. +Lemma colorswap_involutive_eq {n m} (zx : ZX n m) : + (⊙ ⊙ zx) = zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - repeat rewrite semantics_transpose_comm. - rewrite transpose_involutive. - lma. + induction zx; [reflexivity..| |]; + cbn; rewrite IHzx1, IHzx2; reflexivity. +Qed. + +Lemma transpose_involutive : forall {n m} (zx : ZX n m), + zx ⊤ ⊤ ∝= zx. +Proof. + intros n m zx. + now rewrite transpose_involutive_eq. +Qed. + +Lemma adjoint_involutive : forall {n m} (zx : ZX n m), + zx † † ∝= zx. +Proof. + intros n m zx. + now rewrite adjoint_involutive_eq. Qed. -Lemma adjoint_involutive : forall n m (zx : ZX n m), - zx † † ∝ zx. +Lemma colorswap_involutive {n m} (zx : ZX n m) : + (⊙ ⊙ zx) ∝= zx. Proof. + now rewrite colorswap_involutive_eq. +Qed. + +Lemma colorswap_zx : forall {n m} (zx0 zx1 : ZX n m), + ⊙ zx0 = ⊙ zx1 -> zx0 = zx1. +Proof. intros. - prop_exists_nonzero 1. - simpl. - repeat rewrite semantics_adjoint_comm. - rewrite adjoint_involutive. - lma. + rewrite <- (colorswap_involutive_eq zx0). + rewrite H. + apply colorswap_involutive_eq. +Qed. + +Lemma colorswap_diagrams_eq : forall {n m} (zx0 zx1 : ZX n m), + ⊙ zx0 ∝= ⊙ zx1 -> zx0 ∝= zx1. +Proof. + intros. + rewrite <- colorswap_involutive. + rewrite H. + apply colorswap_involutive. Qed. -Lemma colorswap_involutive : forall n m (zx : ZX n m), - (⊙ ⊙ zx) ∝ zx. +Lemma colorswap_diagrams_by : forall {n m} (zx0 zx1 : ZX n m) c, + ⊙ zx0 ∝[c] ⊙ zx1 -> zx0 ∝[c] zx1. Proof. intros. - induction zx; try (simpl; easy). - all: simpl; rewrite IHzx1, IHzx2; easy. + rewrite <- colorswap_involutive. + zxrewrite H. + rewrite colorswap_involutive. + zxrefl. Qed. -Lemma colorswap_diagrams : forall n m (zx0 zx1 : ZX n m), +Lemma colorswap_diagrams : forall {n m} (zx0 zx1 : ZX n m), ⊙ zx0 ∝ ⊙ zx1 -> zx0 ∝ zx1. Proof. intros. rewrite <- colorswap_involutive. rewrite H. - apply colorswap_involutive. + now rewrite colorswap_involutive. +Qed. + +Lemma transpose_zx : forall {n m} (zx0 zx1 : ZX n m), + zx0 ⊤ = zx1 ⊤ -> zx0 = zx1. +Proof. + intros. + rewrite <- (transpose_involutive_eq zx0). + rewrite H. + now rewrite transpose_involutive_eq. +Qed. + +Lemma transpose_diagrams_eq : forall {n m} (zx0 zx1 : ZX n m), + zx0 ⊤ ∝= zx1 ⊤ -> zx0 ∝= zx1. +Proof. + intros. + rewrite <- transpose_involutive. + rewrite H. + now rewrite transpose_involutive. +Qed. + +Lemma transpose_diagrams_by : forall {n m} (zx0 zx1 : ZX n m) c, + zx0 ⊤ ∝[c] zx1 ⊤ -> zx0 ∝[c] zx1. +Proof. + intros. + rewrite <- transpose_involutive. + zxrewrite H. + rewrite transpose_involutive. + zxrefl. Qed. -Lemma transpose_diagrams : forall n m (zx0 zx1 : ZX n m), +Lemma transpose_diagrams : forall {n m} (zx0 zx1 : ZX n m), zx0 ⊤ ∝ zx1 ⊤ -> zx0 ∝ zx1. Proof. - intros n m zx0 zx1 [x [Hzx Hx]]. - prop_exists_nonzero x; try assumption. - apply transpose_matrices. - rewrite Mscale_trans. - repeat rewrite <- semantics_transpose_comm. - apply Hzx. + intros. + rewrite <- transpose_involutive. + rewrite H. + now rewrite transpose_involutive. +Qed. + +Lemma adjoint_zx : forall {n m} (zx0 zx1 : ZX n m), + zx0 † = zx1 † -> zx0 = zx1. +Proof. + intros. + rewrite <- (adjoint_involutive_eq zx0). + rewrite H. + now rewrite adjoint_involutive_eq. +Qed. + +Lemma adjoint_diagrams_eq : forall {n m} (zx0 zx1 : ZX n m), + zx0 † ∝= zx1 † -> zx0 ∝= zx1. +Proof. + intros. + rewrite <- adjoint_involutive. + rewrite H. + now rewrite adjoint_involutive. +Qed. + +Lemma adjoint_diagrams_by : forall {n m} (zx0 zx1 : ZX n m) c, + zx0 † ∝[c ^*] zx1 † -> zx0 ∝[c] zx1. +Proof. + intros. + rewrite <- adjoint_involutive. + zxrewrite H. + rewrite adjoint_involutive. + zxrefl. + enough (c <> 0) by C_field. + rewrite <- (Cconj_involutive c). + now apply Cconj_neq_0. Qed. -Lemma adjoint_diagrams : forall n m (zx0 zx1 : ZX n m), +Lemma adjoint_diagrams : forall {n m} (zx0 zx1 : ZX n m), zx0 † ∝ zx1 † -> zx0 ∝ zx1. Proof. - intros n m zx0 zx1 [x [Hzx Hx]]. - prop_exists_nonzero (x ^*)%C. - apply adjoint_matrices. - rewrite Mscale_adj. - repeat rewrite <- semantics_adjoint_comm. - rewrite Cconj_involutive. - apply Hzx. - apply Cconj_neq_0. - assumption. + intros. + rewrite <- adjoint_involutive. + rewrite H. + now rewrite adjoint_involutive. +Qed. + +Lemma colorswap_adjoint_commute : forall {n m} (zx : ZX n m), + ⊙ (zx †) = (⊙ zx) †. +Proof. + intros. + induction zx; [reflexivity.. | |]; + cbn; now f_equal. Qed. -Lemma colorswap_adjoint_commute : forall n m (zx : ZX n m), - ⊙ (zx †) ∝ (⊙ zx) †. +Lemma transpose_adjoint_commute : forall {n m} (zx : ZX n m), + (zx †) ⊤ = (zx ⊤) †. Proof. intros. - induction zx; try easy. - all: simpl; rewrite IHzx1, IHzx2; easy. + induction zx; [reflexivity.. | |]; + cbn; now f_equal. Qed. -Lemma transpose_adjoint_commute : forall n m (zx : ZX n m), - (zx †) ⊤ ∝ (zx ⊤) †. +Lemma colorswap_transpose_commute : forall {n m} (zx : ZX n m), + ⊙ (zx ⊤) = (⊙ zx) ⊤. Proof. intros. - induction zx; try easy. - all: simpl; rewrite IHzx1, IHzx2; easy. + induction zx; [reflexivity.. | |]; + cbn; now f_equal. +Qed. + + +Lemma wire_transpose : Wire ⊤ = Wire. +Proof. + reflexivity. +Qed. + +Lemma box_transpose : Box ⊤ = Box. +Proof. + reflexivity. Qed. -Lemma colorswap_transpose_commute : forall n m (zx : ZX n m), - ⊙ (zx ⊤) ∝ (⊙ zx) ⊤. +Lemma nstack1_transpose : forall {n} (zx : ZX 1 1), + (n ↑ zx)⊤ = n ↑ (zx ⊤). Proof. intros. - induction zx; try easy. - all: simpl; rewrite IHzx1, IHzx2; easy. + induction n. + - easy. + - simpl. + rewrite IHn. + reflexivity. Qed. +Lemma nstack_transpose {n m} k (zx : ZX n m) : + (k ⇑ zx) ⊤ = k ⇑ (zx ⊤). +Proof. + induction k; [reflexivity|]. + cbn; now rewrite IHk. +Qed. -Lemma transpose_wire : Wire ⊤ ∝ Wire. +Lemma n_wire_transpose n : (n_wire n) ⊤ = n_wire n. Proof. - prop_exists_nonzero 1. - simpl; lma. + apply nstack1_transpose. +Qed. + +Lemma nbox_tranpose n : (n_box n) ⊤ = n_box n. +Proof. + apply nstack1_transpose. Qed. + + Lemma Z_spider_1_1_fusion : forall {nIn nOut} α β, - (Z nIn 1 α) ⟷ (Z 1 nOut β) ∝ + (Z nIn 1 α) ⟷ (Z 1 nOut β) ∝= Z nIn nOut (α + β). Proof. - prop_exists_nonzero 1. - Msimpl. + intros nIn nOut α β. + unfold proportional_by_1. apply Z_spider_1_1_fusion_eq. Qed. Lemma X_spider_1_1_fusion : forall {nIn nOut} α β, - (X nIn 1 α) ⟷ (X 1 nOut β) ∝ + (X nIn 1 α) ⟷ (X 1 nOut β) ∝= X nIn nOut (α + β). Proof. - intros. - apply colorswap_diagrams. + intros nIn nOut α β. + apply colorswap_diagrams_eq. simpl. 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. \ No newline at end of file +Qed. \ No newline at end of file diff --git a/src/CoreData/QlibTemp.v b/src/CoreData/QlibTemp.v index 10eac0d..ce85cae 100644 --- a/src/CoreData/QlibTemp.v +++ b/src/CoreData/QlibTemp.v @@ -1,485 +1,55 @@ From QuantumLib Require Import Matrix. From QuantumLib Require Import Quantum. -(* @nocheck name *) -Lemma Mscale_inv : forall {n m} (A B : Matrix n m) c, c <> C0 -> c .* A = B <-> A = (/ c) .* B. -Proof. - intros. - split; intro H0; [rewrite <- H0 | rewrite H0]; - rewrite Mscale_assoc. - - rewrite Cinv_l; [ lma | assumption]. - - rewrite Cinv_r; [ lma | assumption]. -Qed. - -(* @nocheck name *) -Lemma Ropp_lt_0 : forall x : R, x < 0 -> 0 < -x. -Proof. - intros. - rewrite <- Ropp_0. - apply Ropp_lt_contravar. - easy. -Qed. - -(* @nocheck name *) -Definition Rsqrt (x : R) :C := -match Rcase_abs x with -| left a => Ci * Rsqrt {| nonneg := - x; cond_nonneg := Rlt_le 0 (-x)%R (Ropp_lt_0 x a) |} -| right a => C1 * Rsqrt {| nonneg := x; cond_nonneg := Rge_le x R0 a |} -end. - -(* @nocheck name *) -(* *) -Lemma INR_pi_exp : forall (r : nat), - Cexp (INR r * PI) = 1 \/ Cexp (INR r * PI) = -1. -Proof. - intros. - dependent induction r. - - simpl. - rewrite Rmult_0_l. - left. - apply Cexp_0. - - rewrite S_O_plus_INR. - rewrite Rmult_plus_distr_r. - rewrite Rmult_1_l. - rewrite Rplus_comm. - rewrite Cexp_plus_PI. - destruct IHr. - + rewrite H; right; lca. - + rewrite H; left; lca. -Qed. - -Lemma transpose_matrices : forall {n m} (A B : Matrix n m), - A ⊤ = B ⊤ -> A = B. -Proof. - intros. - rewrite <- transpose_involutive. - rewrite <- H. - rewrite transpose_involutive. - easy. -Qed. - -Lemma adjoint_matrices : forall {n m} (A B : Matrix n m), - A † = B † -> A = B. -Proof. - intros. - rewrite <- adjoint_involutive. - rewrite <- H. - rewrite adjoint_involutive. - easy. -Qed. - - -Lemma kron_id_dist_r : forall {n m o} p (A : Matrix n m) (B : Matrix m o), -WF_Matrix A -> WF_Matrix B -> (A × B) ⊗ (I p) = (A ⊗ (I p)) × (B ⊗ (I p)). -Proof. - intros. - rewrite <- (Mmult_1_l _ _ (I p)). - rewrite kron_mixed_product. - Msimpl. - easy. - auto with wf_db. -Qed. - -Lemma kron_id_dist_l : forall {n m o} p (A : Matrix n m) (B : Matrix m o), -WF_Matrix A -> WF_Matrix B -> (I p) ⊗ (A × B) = ((I p) ⊗ A) × ((I p) ⊗ B). -Proof. - intros. - rewrite <- (Mmult_1_l _ _ (I p)). - rewrite kron_mixed_product. - Msimpl. - easy. - auto with wf_db. -Qed. - -Lemma swap_transpose : swap ⊤%M = swap. -Proof. lma. Qed. - -Lemma swap_spec' : swap = ((ket 0 × bra 0) ⊗ (ket 0 × bra 0) .+ (ket 0 × bra 1) ⊗ (ket 1 × bra 0) - .+ (ket 1 × bra 0) ⊗ (ket 0 × bra 1) .+ (ket 1 × bra 1) ⊗ (ket 1 × bra 1)). -Proof. - solve_matrix. -Qed. - -Lemma xbasis_plus_spec : ∣+⟩ = / √ 2 .* (∣0⟩ .+ ∣1⟩). -Proof. solve_matrix. Qed. - -Lemma xbasis_minus_spec : ∣-⟩ = / √ 2 .* (∣0⟩ .+ (- 1) .* (∣1⟩)). -Proof. solve_matrix. Qed. - -Definition braminus := / √ 2 .* (⟨0∣ .+ (-1 .* ⟨1∣)). -Definition braplus := / √ 2 .* (⟨0∣ .+ ⟨1∣). - -Notation "⟨+∣" := braplus. -Notation "⟨-∣" := braminus. - -Lemma WF_braplus : WF_Matrix (⟨+∣). -Proof. unfold braplus; auto with wf_db. Qed. - -Lemma WF_braminus : WF_Matrix (⟨-∣). -Proof. unfold braminus; auto with wf_db. Qed. - -Lemma braplus_transpose_ketplus : - ⟨+∣⊤ = ∣+⟩. -Proof. unfold braplus; lma. Qed. - -Lemma braminus_transpose_ketminus : - ⟨-∣⊤ = ∣-⟩. -Proof. unfold braminus; lma. Qed. - -(* @nocheck name *) -(* PI is captialized in Coq R *) -Lemma Cexp_2_PI : forall a, Cexp (INR a * 2 * PI) = 1. -Proof. - intros. - induction a. - - simpl. - rewrite 2 Rmult_0_l. - rewrite Cexp_0. - easy. - - rewrite S_INR. - rewrite 2 Rmult_plus_distr_r. - rewrite Rmult_1_l. - rewrite double. - rewrite <- Rplus_assoc. - rewrite 2 Cexp_plus_PI. - rewrite IHa. - lca. -Qed. - -#[export] Hint Resolve - WF_braplus - WF_braminus : wf_db. - -#[export] Hint Rewrite - Mscale_kron_dist_l - Mscale_kron_dist_r - Mscale_mult_dist_l - Mscale_mult_dist_r - Mscale_assoc : scalar_move_db. - -#[export] Hint Rewrite <- Mscale_plus_distr_l : scalar_move_db. -#[export] Hint Rewrite <- Mscale_plus_distr_r : scalar_move_db. - -(* @nocheck name *) -Definition Csqrt (z : C) : C := - match z with - | (a, b) => sqrt ((Cmod z + a) / 2) + Ci * (b / Rabs b) * sqrt((Cmod z - a) / 2) - 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. +Lemma Cdiv_0_l c : 0 / c = 0. +Proof. apply Cmult_0_l. Qed. (* @nocheck name *) (* Conventional name *) -Lemma Mmult1plus : - ⟨1∣ × ∣+⟩ = / (√2)%R .* I 1. +Lemma Cdiv_nonzero_iff (c d : C) : + d / c <> 0 <-> c <> 0 /\ d <> 0. Proof. - unfold xbasis_plus. - rewrite Mscale_mult_dist_r. - rewrite Mmult_plus_distr_l. - rewrite Mmult10. - rewrite Mmult11. - lma. + rewrite Cdiv_integral_iff. + tauto. Qed. (* @nocheck name *) (* Conventional name *) -Lemma Mmultminus0 : - ⟨-∣ × ∣0⟩ = / (√2)%R .* I 1. +Lemma Cdiv_nonzero_iff_r (c d : C) : c <> 0 -> + d / c <> 0 <-> d <> 0. Proof. - unfold braminus. - rewrite Mscale_mult_dist_l. - rewrite Mmult_plus_distr_r. - rewrite Mmult00. - rewrite Mscale_mult_dist_l. - rewrite Mmult10. - lma. + intros Hc. + rewrite Cdiv_nonzero_iff. + tauto. Qed. (* @nocheck name *) (* Conventional name *) -Lemma Mmult0minus : - ⟨0∣ × ∣-⟩ = / (√2)%R .* I 1. +Lemma Cmult_nonzero_iff (c d : C) : + c * d <> 0 <-> c <> 0 /\ d <> 0. Proof. - unfold xbasis_minus. - rewrite Mscale_mult_dist_r. - rewrite Mmult_plus_distr_l. - rewrite Mmult00. - rewrite Mscale_mult_dist_r. - rewrite Mmult01. - lma. + rewrite Cmult_integral_iff. + tauto. Qed. (* @nocheck name *) (* Conventional name *) -Lemma Mmultminus1 : - ⟨-∣ × ∣1⟩ = - / (√2)%R .* I 1. +Lemma Cinv_div (c d : C) : + / (c / d) = d / c. Proof. - unfold braminus. - rewrite Mscale_mult_dist_l. - rewrite Mmult_plus_distr_r. - rewrite Mmult01. - rewrite Mscale_mult_dist_l. - rewrite Mmult11. - lma. + unfold Cdiv. + rewrite Cinv_mult_distr, Cinv_inv. + apply Cmult_comm. 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. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_plus_minus : ∣+⟩ .+ ∣-⟩ = (√2)%R .* ∣0⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. - C_field. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_plus_minus_opp : ∣+⟩ .+ -1 .* ∣-⟩ = (√2)%R .* ∣1⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. - C_field_simplify. - lca. - C_field. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_minus_plus : ∣-⟩ .+ ∣+⟩ = (√2)%R .* ∣0⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. - C_field. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_minus_opp_plus : -1 .* ∣-⟩ .+ ∣+⟩ = (√2)%R .* ∣1⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. - C_field_simplify. - lca. - C_field. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_0_1 : ∣0⟩ .+ ∣1⟩ = (√2)%R .* ∣+⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_0_1_opp : ∣0⟩ .+ -1 .* ∣1⟩ = (√2)%R .* ∣-⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. - C_field_simplify. - lca. - C_field. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_1_0 : ∣1⟩ .+ ∣0⟩ = (√2)%R .* ∣+⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. -Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Mplus_1_opp_0 : -1 .* ∣1⟩ .+ ∣0⟩ = (√2)%R .* ∣-⟩. -Proof. - unfold xbasis_plus. - unfold xbasis_minus. - solve_matrix. - C_field_simplify. - lca. - C_field. -Qed. - -Lemma σz_decomposition : σz = ∣0⟩⟨0∣ .+ -1 .* ∣1⟩⟨1∣. -Proof. solve_matrix. Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Cexp_spec : forall α, Cexp α = cos α + Ci * sin α. -Proof. intros; lca. Qed. - -(* @nocheck name *) -(* Conventional name *) -Lemma Cexp_minus : forall θ, - Cexp θ + Cexp (-θ) = 2 * cos θ. +Lemma Cdiv_div (b c d : C) : + b / (c / d) = b * d / c. Proof. - intros. - unfold Cexp. - rewrite cos_neg. - rewrite sin_neg. - lca. + unfold Cdiv at 1. + rewrite Cinv_div. + apply Cmult_assoc. Qed. \ No newline at end of file diff --git a/src/CoreData/SemanticCore.v b/src/CoreData/SemanticCore.v index 418ed36..e8658c5 100644 --- a/src/CoreData/SemanticCore.v +++ b/src/CoreData/SemanticCore.v @@ -152,6 +152,8 @@ Definition X_dirac_semantics (n m : nat) (α : R) := Arguments Z_dirac_semantics n m α /. Arguments X_dirac_semantics n m α /. +(** Simplify by unfolding [dirac_spider_semantics] and [bra_ket_mn], + then [simplf; Msimpl]. *) Ltac unfold_dirac_spider := simpl; unfold dirac_spider_semantics, bra_ket_mn; try (simpl; Msimpl). diff --git a/src/CoreData/ZXCore.v b/src/CoreData/ZXCore.v index 8eedd7f..200f8fc 100644 --- a/src/CoreData/ZXCore.v +++ b/src/CoreData/ZXCore.v @@ -56,7 +56,7 @@ matrices and one based on dirac notation. *) (* @nocheck name *) -Reserved Notation "⟦ zx ⟧" (at level 68). (* = is 70, need to be below *) +Reserved Notation "⟦ zx ⟧" (at level 0, zx at level 200). (* = is 70, need to be below *) Fixpoint ZX_semantics {n m} (zx : ZX n m) : Matrix (2 ^ m) (2 ^ n) := match zx with @@ -99,7 +99,14 @@ Proof. apply cast_semantics. Qed. -Tactic Notation "simpl_cast_semantics" := try repeat rewrite cast_semantics; try repeat (rewrite cast_semantics_dim; unfold cast_semantics_dim_eqn). +(** Replace [⟦ cast n m prf1 prf2 zx ⟧] in the goal with [⟦ zx ⟧]. + NB this may make the goal no longer definitionally dimensionally + consistent, as the size of [⟦ zx ⟧] need not be trivially equal to + the size of [⟦ cast n m prf1 prf2 zx ⟧]. In some cases, this may even + escape the abilities of [restore_dims] and require manual intervention. *) +Ltac simpl_cast_semantics := + try repeat rewrite cast_semantics; + try repeat (rewrite cast_semantics_dim; unfold cast_semantics_dim_eqn). (* @nocheck name *) Fixpoint ZX_dirac_sem {n m} (zx : ZX n m) : @@ -173,18 +180,17 @@ Proof. apply WF_ZX. Qed. -(* Definition n_wire := fun n => n ↑ Wire. *) +Definition n_wire := fun n => n ↑ Wire. Definition n_box := fun n => n ↑ Box. -Notation "'n_wire' n" := (n ↑ —) (at level 35). - Lemma n_wire_semantics {n} : ⟦ n_wire n ⟧ = I (2^n). Proof. induction n; auto. simpl. + unfold n_wire in IHn. rewrite IHn. rewrite id_kron. - auto. + reflexivity. Qed. Lemma n_box_semantics {n} : ⟦ n_box n ⟧ = n ⨂ hadamard. @@ -194,7 +200,7 @@ Proof. unfold n_box in IHn. rewrite IHn. rewrite <- kron_n_assoc by auto with wf_db. - auto. + reflexivity. Qed. #[export] Hint Rewrite @n_wire_semantics @n_box_semantics : zx_sem_db. @@ -217,13 +223,6 @@ Fixpoint transpose {nIn nOut} (zx : ZX nIn nOut) : ZX nOut nIn := end where "zx ⊤" := (transpose zx) : ZX_scope. -Lemma transpose_involutive_eq : forall {nIn nOut} (zx : ZX nIn nOut), - zx = (zx ⊤)⊤. -Proof. - intros; induction zx; try auto. - 1,2: simpl; rewrite <- IHzx1, <- IHzx2; try rewrite eq_sym_involutive; auto. -Qed. - (* Negating the angles of a diagram, complex conjugate *) Reserved Notation "zx ⊼" (at level 0). (* \barwedge *) @@ -277,6 +276,21 @@ Proof. restore_dims; rewrite Mmult_adjoint; reflexivity. Qed. +Lemma conjugate_decomp {n m} (zx : ZX n m) : + zx ⊼ = zx † ⊤. +Proof. + induction zx; [reflexivity.. | |]; + unfold adjoint in *; cbn; congruence. +Qed. + +Lemma semantics_conjugate_comm {nIn nOut} : forall (zx : ZX nIn nOut), + ⟦ zx ⊼ ⟧ = (⟦ zx ⟧) †%M ⊤%M. +Proof. + intros zx. + rewrite conjugate_decomp. + now rewrite semantics_transpose_comm, semantics_adjoint_comm. +Qed. + Opaque adjoint. Reserved Notation "⊙ zx" (at level 0). (* \odot *) diff --git a/src/CoreRules/CapCupRules.v b/src/CoreRules/CapCupRules.v index e18863a..99dc874 100644 --- a/src/CoreRules/CapCupRules.v +++ b/src/CoreRules/CapCupRules.v @@ -6,55 +6,45 @@ Require Import StackRules. Require Import SwapRules. Require Import CoreAutomation. -Lemma cup_Z : ⊃ ∝ Z 2 0 0. +Lemma cup_Z : ⊃ ∝= Z 2 0 0. Proof. - prop_exists_nonzero 1. - Msimpl; simpl. - solve_matrix. - autorewrite with Cexp_db; easy. + lma'. + now rewrite Cexp_0. Qed. -Lemma cap_Z : ⊂ ∝ Z 0 2 0. +Lemma cap_Z : ⊂ ∝= Z 0 2 0. Proof. - prop_exists_nonzero 1. - Msimpl; simpl. - solve_matrix. - autorewrite with Cexp_db; easy. + lma'. + now rewrite Cexp_0. Qed. -Lemma cup_X : ⊃ ∝ X 2 0 0. +Lemma cup_X : ⊃ ∝= X 2 0 0. Proof. colorswap_of cup_Z. Qed. -Lemma cap_X : ⊂ ∝ X 0 2 0. +Lemma cap_X : ⊂ ∝= X 0 2 0. Proof. colorswap_of cap_Z. Qed. -Lemma n_cup_0_empty : n_cup 0 ∝ ⦰. +Lemma n_cup_0_empty : n_cup 0 ∝= ⦰. Proof. - unfold n_cup. - repeat (simpl; - cleanup_zx; - simpl_casts). - easy. + lma'. Qed. -Lemma n_cup_1_cup : n_cup 1 ∝ ⊃. +Lemma n_cup_1_cup : n_cup 1 ∝= ⊃. Proof. unfold n_cup. - simpl. - simpl_casts. - simpl. - cleanup_zx. - simpl_casts. + cbn. + auto_cast_eqn (rewrite stack_empty_r). + rewrite 2!cast_id_eq. + rewrite wire_removal_l. bundle_wires. - cleanup_zx. - easy. + now rewrite 2!nwire_removal_l. Qed. Opaque n_cup. -Lemma n_cap_0_empty : n_cap 0 ∝ ⦰. +Lemma n_cap_0_empty : n_cap 0 ∝= ⦰. Proof. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. rewrite n_cup_0_empty. easy. @@ -73,7 +63,8 @@ Qed. Global Open Scope ZX_scope. Lemma n_cup_unswapped_grow_l : forall n prfn prfm, - n_cup_unswapped (S n) ∝ cast _ _ prfn prfm (n_wire n ↕ ⊃ ↕ n_wire n) ⟷ n_cup_unswapped n. + n_cup_unswapped (S n) ∝= cast _ _ prfn prfm (n_wire n ↕ ⊃ ↕ n_wire n) ⟷ + n_cup_unswapped n. Proof. intros. induction n. @@ -91,19 +82,19 @@ Proof. rewrite stack_wire_distribute_l. rewrite stack_wire_distribute_r. bundle_wires. - erewrite <- (@cast_n_wire (n + 1) (1 + n)). + erewrite <- (@cast_n_wire (n + 1) (S n)). rewrite <- ComposeRules.compose_assoc. - apply compose_simplify; [ | easy]. + apply compose_simplify_eq; [ | easy]. erewrite (cast_compose_mid (S (n + S n))). rewrite cast_compose_distribute. repeat rewrite cast_contract. - apply compose_simplify; [ | apply cast_simplify; easy]. + apply compose_simplify_eq; [ | apply cast_simplify_eq; easy]. simpl_casts. rewrite 2 stack_assoc. simpl_casts. rewrite 3 stack_assoc_back. simpl_casts. - erewrite <- (@cast_n_wire (n + 1) (1 + n)) at 2. + erewrite <- (@cast_n_wire (n + 1) (S n)) at 2. rewrite cast_stack_r. simpl. rewrite (stack_assoc (— ↕ n_wire n ↕ ⊃) (n_wire n) —). @@ -114,28 +105,27 @@ 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. +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. +Lemma n_cup_unswapped_colorswap : forall n, + ⊙ (n_cup_unswapped n) = n_cup_unswapped n. Proof. intros. induction n; [ easy | ]. simpl. - apply compose_simplify; [ | easy ]. + f_equal. rewrite cast_colorswap. + apply cast_simplify_zx. simpl. rewrite IHn. easy. Qed. -Lemma n_cup_colorswap : forall n, ⊙ (n_cup n) ∝ n_cup n. +Lemma n_cup_colorswap : forall n, ⊙ (n_cup n) = n_cup n. Proof. intros. Local Transparent n_cup. @@ -147,7 +137,7 @@ Local Transparent n_cup. easy. Qed. -Lemma n_cap_unswapped_colorswap : forall n, ⊙ (n_cap_unswapped n) ∝ n_cap_unswapped n. +Lemma n_cap_unswapped_colorswap : forall n, ⊙ (n_cap_unswapped n) = n_cap_unswapped n. Proof. intros. unfold n_cap_unswapped. @@ -156,7 +146,7 @@ Proof. easy. Qed. -Lemma n_cap_colorswap : forall n, ⊙ (n_cap n) ∝ n_cap n. +Lemma n_cap_colorswap : forall n, ⊙ (n_cap n) = n_cap n. Proof. intros. unfold n_cap. @@ -172,26 +162,22 @@ Qed. (fun n => @n_cap_unswapped_colorswap n) : colorswap_db. -Lemma n_cup_unswapped_transpose : forall n, (n_cup_unswapped n)⊤ ∝ n_cap_unswapped n. +Lemma n_cup_unswapped_transpose : forall n, (n_cup_unswapped n)⊤ = n_cap_unswapped n. Proof. - intros. - unfold n_cap_unswapped. - easy. + reflexivity. Qed. -Lemma n_cap_unswapped_transpose : forall n, (n_cap_unswapped n)⊤ ∝ n_cup_unswapped n. +Lemma n_cap_unswapped_transpose : forall n, (n_cap_unswapped n)⊤ = n_cup_unswapped n. Proof. intros. unfold n_cap_unswapped. - rewrite Proportional.transpose_involutive. + rewrite Proportional.transpose_involutive_eq. easy. Qed. -Lemma n_cup_transpose : forall n, (n_cup n)⊤ ∝ n_cap n. +Lemma n_cup_transpose : forall n, (n_cup n)⊤ = n_cap n. Proof. - intros. - unfold n_cap. - easy. + reflexivity. Qed. Lemma n_cap_transpose : forall n, (n_cap n)⊤ ∝ n_cup n. diff --git a/src/CoreRules/CastRules.v b/src/CoreRules/CastRules.v index 5b9fe62..ad4ef57 100644 --- a/src/CoreRules/CastRules.v +++ b/src/CoreRules/CastRules.v @@ -4,14 +4,45 @@ Require Import SpiderInduction. Open Scope ZX_scope. -Lemma cast_id : -forall {n m} prfn prfm (zx : ZX n m), - cast n m prfn prfm zx ∝ zx. +Lemma cast_id_eq {n m} prfn prfm (zx : ZX n m) : + cast n m prfn prfm zx = zx. +Proof. + rewrite (UIP_nat m _ _ eq_refl), (UIP_nat _ _ _ eq_refl). + reflexivity. +Qed. + +Lemma cast_id : forall {n m} prfn prfm (zx : ZX n m), + cast n m prfn prfm zx ∝= zx. +Proof. + intros. + now rewrite cast_id_eq. +Qed. + +Lemma cast_simplify_zx : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m), + zx0 = zx1 -> + cast n' m' prfn0 prfm0 zx0 = cast n' m' prfn1 prfm1 zx1. Proof. intros; subst. - prop_exists_nonzero 1. - rewrite cast_semantics. - simpl; lma. + f_equal; apply UIP_nat. +Qed. + +Lemma cast_simplify_eq : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m), + zx0 ∝= zx1 -> + cast n' m' prfn0 prfm0 zx0 ∝= cast n' m' prfn1 prfm1 zx1. +Proof. + intros. + now subst; rewrite 2!cast_id. +Qed. + +Lemma cast_simplify_by : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m) c, + zx0 ∝[c] zx1 -> + cast n' m' prfn0 prfm0 zx0 ∝[c] cast n' m' prfn1 prfm1 zx1. +Proof. + intros. + now subst; rewrite 2!cast_id. Qed. Lemma cast_simplify : @@ -20,72 +51,176 @@ Lemma cast_simplify : cast n' m' prfn0 prfm0 zx0 ∝ cast n' m' prfn1 prfm1 zx1. Proof. intros. - destruct H; destruct H. - prop_exists_nonzero x; - simpl_cast_semantics; - congruence. + subst. + now rewrite 2!cast_id. +Qed. + +Lemma cast_simplify_zx_rev : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m), + cast n' m' prfn0 prfm0 zx0 = cast n' m' prfn1 prfm1 zx1 -> + zx0 = zx1. +Proof. + intros. + now subst; rewrite 2!cast_id_eq in *. +Qed. + +Lemma cast_simplify_eq_rev : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m), + cast n' m' prfn0 prfm0 zx0 ∝= cast n' m' prfn1 prfm1 zx1 -> + zx0 ∝= zx1. +Proof. + intros. + now subst; rewrite 2!cast_id in *. Qed. -Tactic Notation "cast_irrelevance" := - apply cast_simplify; try easy. +Lemma cast_simplify_by_rev : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m) c, + cast n' m' prfn0 prfm0 zx0 ∝[c] cast n' m' prfn1 prfm1 zx1 -> + zx0 ∝[c] zx1. +Proof. + intros. + now subst; rewrite 2!cast_id_eq in *. +Qed. + +Lemma cast_simplify_rev : + forall {n n' m m'} prfn0 prfm0 prfn1 prfm1 (zx0 zx1 : ZX n m), + cast n' m' prfn0 prfm0 zx0 ∝ cast n' m' prfn1 prfm1 zx1 -> + zx0 ∝ zx1. +Proof. + intros. + now subst; rewrite 2!cast_id in *. +Qed. -Tactic Notation "auto_cast_eqn" tactic3(tac) := unshelve tac; try lia; shelve_unifiable. +(** On a goal [$ n', m' ::: zx0 $ (R) $ n', m' ::: zx1 $] where + [zx0] and [zx1] have the same dimensions, replace the goal + with [zx0 (R) zx1]. + Here, [(R)] is one of [=], [∝=], [∝[c]], and [∝]. *) +Ltac cast_irrelevance := + first [apply cast_simplify + | apply cast_simplify_by + | apply cast_simplify_eq + | apply cast_simplify_zx]; try easy. + +(** Given a hypothesis [H : $ n', m' ::: zx0 $ (R) $ n', m' ::: zx1 $] where + [zx0] and [zx1] have the same dimensions, + replace the type of [H] with [zx0 (R) zx1]. + Here, [(R)] is one of [=], [∝=], [∝[c]], and [∝]. *) +Ltac cast_irrelevance_in H := + first [apply cast_simplify in H + | apply cast_simplify_by in H + | apply cast_simplify_eq in H + | apply cast_simplify_zx in H]. + +(** Run a tactic [tac], solving as many side-conditions as possible with [lia] + and shelving any others. *) +Ltac auto_cast_eqn tac := + unshelve tac; try lia; shelve_unifiable. + +(** Run a tactic [tac], solving as many side-conditions as possible with [lia] + and shelving any others. *) +Tactic Notation "auto_cast_eqn" tactic3(tac) := + auto_cast_eqn tac. #[export] Hint Rewrite @cast_id : cast_simpl_db. -Tactic Notation "simpl_casts" := auto_cast_eqn (autorewrite with cast_simpl_db); repeat cast_irrelevance. -Tactic Notation "simpl_casts_in" hyp(H) := auto_cast_eqn (autorewrite with cast_simpl_db in H); repeat (apply cast_simplify in H). +(** Simplify casts in the goal by [autorewrite with cast_simpl_db], + solving as many side conditions as possible with [lia], finally + removing as many outer casts as possible with [cast_irrelevance]. + NB if [cast_simpl_db] is not maintained carefully, this tactic may + leave unsolvable side-conditions. *) +Ltac simpl_casts := + auto_cast_eqn (autorewrite with cast_simpl_db); repeat cast_irrelevance. + +(** Simplify casts in [H] by [autorewrite with cast_simpl_db], + solving as many side conditions as possible with [lia], finally + removing as many outer casts as possible with [cast_irrelevance_in]. + NB if [cast_simpl_db] is not maintained carefully, this tactic may + leave unsolvable side-conditions. *) +Tactic Notation "simpl_casts_in" hyp(H) := + auto_cast_eqn (autorewrite with cast_simpl_db in H); + cast_irrelevance_in H. + + +Lemma cast_stack_l_eq {nTop nTop' mTop mTop' nBot mBot} + prfnTop prfmTop prfn prfm (zxTop : ZX nTop mTop) (zxBot : ZX nBot mBot) : + (cast nTop' mTop' prfnTop prfmTop zxTop) ↕ zxBot = + cast (nTop' + nBot) (mTop' + mBot) prfn prfm (zxTop ↕ zxBot). +Proof. + now subst; rewrite !cast_id_eq. +Qed. Lemma cast_stack_l : forall {nTop nTop' mTop mTop' nBot mBot} prfnTop prfmTop prfn prfm (zxTop : ZX nTop mTop) (zxBot : ZX nBot mBot), - (cast nTop' mTop' prfnTop prfmTop zxTop) ↕ zxBot ∝ + (cast nTop' mTop' prfnTop prfmTop zxTop) ↕ zxBot ∝= cast (nTop' + nBot) (mTop' + mBot) prfn prfm (zxTop ↕ zxBot). Proof. intros. - subst. - simpl_casts. - reflexivity. + now subst; rewrite !cast_id_eq. +Qed. + +Lemma cast_stack_r_eq : forall {nTop mTop nBot nBot' mBot mBot'} prfnBot prfmBot prfn prfm + (zxTop : ZX nTop mTop) (zxBot : ZX nBot mBot), + zxTop ↕ (cast nBot' mBot' prfnBot prfmBot zxBot) = + cast (nTop + nBot') (mTop + mBot') prfn prfm (zxTop ↕ zxBot). +Proof. + intros. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_stack_r : forall {nTop mTop nBot nBot' mBot mBot'} prfnBot prfmBot prfn prfm (zxTop : ZX nTop mTop) (zxBot : ZX nBot mBot), - zxTop ↕ (cast nBot' mBot' prfnBot prfmBot zxBot) ∝ + zxTop ↕ (cast nBot' mBot' prfnBot prfmBot zxBot) ∝= cast (nTop + nBot') (mTop + mBot') prfn prfm (zxTop ↕ zxBot). Proof. intros. - subst. - simpl_casts. - reflexivity. + now subst; rewrite !cast_id_eq. +Qed. + +Lemma cast_stack_distribute_eq : + forall {n n' m m' o o' p p'} prfn prfm prfo prfp prfno prfmp + (zx0 : ZX n m) (zx1 : ZX o p), + cast (n' + o') (m' + p') prfno prfmp (zx0 ↕ zx1) = + cast n' m' prfn prfm zx0 ↕ cast o' p' prfo prfp zx1. +Proof. + intros. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_stack_distribute : forall {n n' m m' o o' p p'} prfn prfm prfo prfp prfno prfmp (zx0 : ZX n m) (zx1 : ZX o p), - cast (n' + o') (m' + p') prfno prfmp (zx0 ↕ zx1) ∝ + cast (n' + o') (m' + p') prfno prfmp (zx0 ↕ zx1) ∝= cast n' m' prfn prfm zx0 ↕ cast o' p' prfo prfp zx1. Proof. intros. - subst. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq. Qed. #[export] Hint Rewrite @cast_stack_l @cast_stack_r : cast_simpl_db. +Lemma cast_contract_eq : + forall {n0 m0 n1 m1 n2 m2} prfn01 prfm01 prfn12 prfm12 prfn prfm (zx : ZX n0 m0), + cast n2 m2 prfn12 prfm12 + (cast n1 m1 prfn01 prfm01 + zx) = + cast n2 m2 prfn prfm zx. +Proof. + intros. + now subst; rewrite !cast_id_eq. +Qed. + + Lemma cast_contract : forall {n0 m0 n1 m1 n2 m2} prfn01 prfm01 prfn12 prfm12 prfn prfm (zx : ZX n0 m0), cast n2 m2 prfn12 prfm12 (cast n1 m1 prfn01 prfm01 - zx) ∝ + zx) ∝= cast n2 m2 prfn prfm zx. Proof. - intros; subst. - prop_exists_nonzero 1. - simpl. - simpl_cast_semantics. - lma. + intros. + now subst; rewrite !cast_id_eq. Qed. @@ -97,36 +232,41 @@ Lemma cast_symm : zx0 ∝ cast n0 m0 prfn' prfm' zx1. Proof. intros. - split; intros. - - subst. - simpl_casts. - rewrite cast_id in H. - easy. - - subst. - simpl_casts. - rewrite cast_id in H. - easy. + now subst; rewrite !cast_id_eq. Qed. +Lemma cast_contract_l_eq : forall {n m n0 m0 n1 m1} prfn0 prfm0 prfn1 prfm1 prfn prfm + (zx0 : ZX n0 m0) (zx1 : ZX n1 m1), + cast n m prfn0 prfm0 zx0 ∝= cast n m prfn1 prfm1 zx1 <-> + cast n1 m1 prfn prfm zx0 ∝= zx1. +Proof. + intros. + now subst; rewrite !cast_id_eq. +Qed. + +Lemma cast_contract_l_by : forall {n m n0 m0 n1 m1} prfn0 prfm0 prfn1 prfm1 prfn prfm + (zx0 : ZX n0 m0) (zx1 : ZX n1 m1) c, + cast n m prfn0 prfm0 zx0 ∝[c] cast n m prfn1 prfm1 zx1 <-> + cast n1 m1 prfn prfm zx0 + ∝[c] zx1. +Proof. + intros. + now subst; rewrite !cast_id_eq. +Qed. + Lemma cast_contract_l : forall {n m n0 m0 n1 m1} prfn0 prfm0 prfn1 prfm1 prfn prfm (zx0 : ZX n0 m0) (zx1 : ZX n1 m1), cast n m prfn0 prfm0 zx0 ∝ cast n m prfn1 prfm1 zx1 <-> cast n1 m1 prfn prfm zx0 ∝ zx1. Proof. - intros; split; intros. - - auto_cast_eqn (rewrite <- cast_symm in H). - simpl_casts_in H. - rewrite <- H. - cast_irrelevance. - - auto_cast_eqn (rewrite <- cast_symm). - simpl_casts. - rewrite <- H. - cast_irrelevance. + intros. + now subst; rewrite !cast_id_eq. Qed. -#[export] Hint Rewrite @cast_contract_l : cast_simpl_db. +#[export] Hint Rewrite @cast_contract_l_eq @cast_contract_l_by + @cast_contract_l : cast_simpl_db. Lemma cast_contract_r : forall {n m n0 m0 n1 m1} prfn0 prfm0 prfn1 prfm1 prfn prfm @@ -134,94 +274,74 @@ Lemma cast_contract_r : forall {n m n0 m0 n1 m1} prfn0 prfm0 prfn1 prfm1 prfn pr cast n m prfn0 prfm0 zx0 ∝ cast n m prfn1 prfm1 zx1 <-> zx0 ∝ cast n0 m0 prfn prfm zx1. Proof. - intros; split; intros. - - simpl_casts_in H. - rewrite <- H. - simpl_casts. - easy. - - simpl_casts. - auto_cast_eqn (rewrite cast_symm). - rewrite H. - cast_irrelevance. + intros. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_compose_distribute : 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' o' prfn prfo (zx0 ⟷ zx1) = cast n' m prfn eq_refl zx0 ⟷ cast m o' eq_refl prfo zx1. Proof. intros. - subst. - simpl_casts. - reflexivity. + now subst; rewrite !cast_id_eq. 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 ∝ + cast n' m' prfn prfm zx0 ⟷ zx1 = cast n' o prfn eq_refl (zx0 ⟷ cast m o (eq_sym prfm) eq_refl zx1). Proof. intros. - subst. - simpl_casts. - reflexivity. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_compose_r : forall {n m m' o o'} prfm prfo (zx0 : ZX n m') (zx1 : ZX m o), - zx0 ⟷ cast m' o' prfm prfo zx1 ∝ + zx0 ⟷ cast m' o' prfm prfo zx1 = cast n o' eq_refl prfo (cast n m eq_refl (eq_sym prfm) zx0 ⟷ zx1). Proof. - intros. subst. simpl_casts. reflexivity. + intros. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_compose_mid : forall {n m o} m' prfm prfm' (zx0 : ZX n m) (zx1 : ZX m o), - zx0 ⟷ zx1 ∝ cast n m' eq_refl prfm zx0 ⟷ cast m' o prfm' eq_refl zx1. + zx0 ⟷ zx1 = cast n m' eq_refl prfm zx0 ⟷ cast m' o prfm' eq_refl zx1. Proof. intros. - subst. - simpl_casts. - reflexivity. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_compose_mid_contract : forall {n m o} n' m' o' prfn prfn' prfm prfm' prfo 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. + 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. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_compose_partial_contract_r : forall {n m o} n' m' o' o'' prfn prfm prfo prfo' prfo'' prfo''' (zx0 : ZX n m') (zx1 : ZX m o), - cast n' o' prfn prfo (zx0 ⟷ cast m' o' prfm prfo' zx1) ∝ cast n' o' prfn prfo'' (zx0 ⟷ cast m' o'' prfm prfo''' zx1). + cast n' o' prfn prfo (zx0 ⟷ cast m' o' prfm prfo' zx1) = cast n' o' prfn prfo'' (zx0 ⟷ cast m' o'' prfm prfo''' zx1). Proof. intros. - subst. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_compose_partial_contract_l : forall {n m o} n' n'' m' o' prfn prfn' prfn'' prfn''' prfm prfo (zx0 : ZX n m) (zx1 : ZX m' o), - cast n' o' prfn prfo (cast n' m' prfn' prfm zx0 ⟷ zx1) ∝ cast n' o' prfn'' prfo (cast n'' m' prfn''' prfm zx0 ⟷ zx1). + cast n' o' prfn prfo (cast n' m' prfn' prfm zx0 ⟷ zx1) = cast n' o' prfn'' prfo (cast n'' m' prfn''' prfm zx0 ⟷ zx1). Proof. intros. - subst. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq. Qed. Lemma change_cast : forall {n m} n' m' n'' m'' {prfn prfm prfn' prfm' prfn'' prfm''} (zx : ZX n m), - cast n' m' prfn prfm zx ∝ + cast n' m' prfn prfm zx = cast n' m' prfn' prfm' (cast n'' m'' prfn'' prfm'' zx). Proof. intros. - subst. - repeat rewrite cast_id. - easy. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_backwards : @@ -230,9 +350,34 @@ Lemma cast_backwards : cast n0 m0 prfn' prfm' zx1 ∝ zx0. Proof. intros. - split; symmetry; subst; - simpl_casts; [rewrite H | rewrite <- H]; - simpl_casts; easy. + now subst; rewrite !cast_id_eq. +Qed. + +Lemma cast_zx : + forall {n m} n' m' prfn prfm (zx0 zx1 : ZX n m), + cast n' m' prfn prfm zx0 = cast n' m' prfn prfm zx1 -> + zx0 = zx1. +Proof. + intros. + now subst; rewrite !cast_id_eq in *. +Qed. + +Lemma cast_diagrams_eq : + forall {n m} n' m' prfn prfm (zx0 zx1 : ZX n m), + cast n' m' prfn prfm zx0 ∝= cast n' m' prfn prfm zx1 -> + zx0 ∝= zx1. +Proof. + intros. + now subst; rewrite !cast_id_eq in *. +Qed. + +Lemma cast_diagrams_by : + forall {n m} n' m' prfn prfm (zx0 zx1 : ZX n m) c, + cast n' m' prfn prfm zx0 ∝[c] cast n' m' prfn prfm zx1 -> + zx0 ∝[c] zx1. +Proof. + intros. + now subst; rewrite !cast_id_eq in *. Qed. Lemma cast_diagrams : @@ -241,46 +386,36 @@ Lemma cast_diagrams : zx0 ∝ zx1. Proof. intros. - subst. - repeat rewrite cast_id in H. - easy. + now subst; rewrite !cast_id_eq in *. Qed. Lemma cast_transpose : forall {n m n' m'} prfn prfm (zx : ZX n m), - (cast n' m' prfn prfm zx) ⊤ ∝ cast m' n' prfm prfn (zx ⊤). + (cast n' m' prfn prfm zx) ⊤ = cast m' n' prfm prfn (zx ⊤). Proof. intros. - destruct prfn, prfm. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq in *. Qed. Lemma cast_conj : forall {n m n' m'} prfn prfm (zx : ZX n m), - (cast n' m' prfn prfm zx) ⊼ ∝ cast n' m' prfn prfm (zx ⊼). + (cast n' m' prfn prfm zx) ⊼ = cast n' m' prfn prfm (zx ⊼). Proof. intros. - destruct prfn, prfm. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq in *. Qed. Lemma cast_adj : forall {n m n' m'} prfn prfm (zx : ZX n m), - (cast n' m' prfn prfm zx) † ∝ cast m' n' prfm prfn (zx †). + (cast n' m' prfn prfm zx) † = cast m' n' prfm prfn (zx †). Proof. intros. - subst. - simpl. - easy. + now subst; rewrite !cast_id_eq in *. Qed. Lemma cast_colorswap : forall {n m n' m'} prfn prfm (zx : ZX n m), - ⊙ (cast n' m' prfn prfm zx) ∝ cast n' m' prfn prfm (⊙ zx). + ⊙ (cast n' m' prfn prfm zx) = cast n' m' prfn prfm (⊙ zx). Proof. intros. - destruct prfn, prfm. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq in *. Qed. #[export] Hint Rewrite @@ -289,59 +424,54 @@ Qed. @cast_adj @cast_colorswap : cast_simpl_db. -Lemma cast_fn : forall {n n' m m'} prfn prfm (f : forall n m : nat, ZX n m), cast n' m' prfn prfm (f n m) ∝ f n' m'. -Proof. +Lemma cast_fn : forall {n n' m m'} prfn prfm (f : forall n m : nat, ZX n m), + cast n' m' prfn prfm (f n m) = f n' m'. +Proof. intros. - destruct prfn, prfm. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq. Qed. -Lemma cast_fn_eq_dim : forall {n n'} prfn prfn' (f : forall n : nat, ZX n n), cast n' n' prfn prfn' (f n) ∝ f n'. -Proof. +Lemma cast_fn_eq_dim : forall {n n'} prfn prfn' (f : forall n : nat, ZX n n), + cast n' n' prfn prfn' (f n) = f n'. +Proof. intros. - destruct prfn. - simpl_casts. - easy. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_Z : forall {n n' m m'} prfn prfm α, - cast n' m' prfn prfm (Z n m α) ∝ Z n' m' α. + cast n' m' prfn prfm (Z n m α) = Z n' m' α. Proof. intros. - rewrite (cast_fn prfn prfm (fun n m => Z n m α)). - easy. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_X : forall {n n' m m'} prfn prfm α, - cast n' m' prfn prfm (X n m α) ∝ X n' m' α. + cast n' m' prfn prfm (X n m α) = X n' m' α. Proof. intros. - rewrite (cast_fn prfn prfm (fun n m => X n m α)). - easy. + now subst; rewrite !cast_id_eq. Qed. #[export] Hint Rewrite @cast_Z @cast_X: cast_simpl_db. Lemma cast_n_stack1 : forall {n n'} prfn prfm (zx : ZX 1 1), - cast n' n' prfn prfm (n ↑ zx) ∝ n' ↑ zx. + cast n' n' prfn prfm (n ↑ zx) = n' ↑ zx. Proof. intros. - rewrite (cast_fn_eq_dim prfn prfm (fun n => n_stack1 n zx)). - easy. + now subst; rewrite !cast_id_eq. Qed. Lemma cast_n_wire : forall {n n'} prfn prfm, - cast n' n' prfn prfm (n_wire n) ∝ n_wire n'. + cast n' n' prfn prfm (n_wire n) = n_wire n'. Proof. intros. apply cast_n_stack1. Qed. Lemma cast_n_box : forall {n n'} prfn prfm, - cast n' n' prfn prfm (n_box n) ∝ n_box n'. + cast n' n' prfn prfm (n_box n) = n_box n'. Proof. intros. apply cast_n_stack1. diff --git a/src/CoreRules/ComposeRules.v b/src/CoreRules/ComposeRules.v index b2bbdfb..e817ae2 100644 --- a/src/CoreRules/ComposeRules.v +++ b/src/CoreRules/ComposeRules.v @@ -5,14 +5,11 @@ Require Import SpiderInduction. Local Open Scope ZX_scope. Lemma compose_assoc : forall {n m0 m1 o} (zx1 : ZX n m0) (zx2 : ZX m0 m1) (zx3 : ZX m1 o), - zx1 ⟷ zx2 ⟷ zx3 ∝ zx1 ⟷ (zx2 ⟷ zx3). + zx1 ⟷ zx2 ⟷ zx3 ∝= zx1 ⟷ (zx2 ⟷ zx3). Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - rewrite Mmult_assoc. - lma. + symmetry. + exact (Mmult_assoc _ _ _). Qed. (* Distributivity *) @@ -20,94 +17,89 @@ Qed. Lemma stack_compose_distr : forall {n1 m1 o2 n3 m2 o4} (zx1 : ZX n1 m1) (zx2 : ZX m1 o2) (zx3 : ZX n3 m2) (zx4 : ZX m2 o4), - (zx1 ⟷ zx2) ↕ (zx3 ⟷ zx4) ∝ (zx1 ↕ zx3) ⟷ (zx2 ↕ zx4). + (zx1 ⟷ zx2) ↕ (zx3 ⟷ zx4) ∝= (zx1 ↕ zx3) ⟷ (zx2 ↕ zx4). Proof. intros. - prop_exists_nonzero 1. - Msimpl. - simpl. - show_dimensions. - repeat rewrite Nat.pow_add_r. - rewrite kron_mixed_product. - reflexivity. + symmetry. + unfold proportional_by_1. + cbn. + restore_dims. + exact (kron_mixed_product _ _ _ _). +Qed. + +Lemma compose_simplify_eq : forall {n m o} + (zx1 zx3 : ZX n m) (zx2 zx4 : ZX m o), + zx1 ∝= zx3 -> zx2 ∝= zx4 -> zx1 ⟷ zx2 ∝= zx3 ⟷ zx4. +Proof. + now intros * -> ->. Qed. Lemma compose_simplify : forall {n m o} (zx1 zx3 : ZX n m) (zx2 zx4 : ZX m o), zx1 ∝ zx3 -> zx2 ∝ zx4 -> zx1 ⟷ zx2 ∝ zx3 ⟷ zx4. Proof. - intros. - rewrite H, H0. - easy. + now intros * -> ->. Qed. -Lemma compose_transpose : forall {n m o} (zx1 : ZX n m) (zx2 : ZX m o), (zx1 ⟷ zx2) ⊤ ∝ (zx2⊤ ⟷ zx1⊤). +Lemma compose_transpose_eq : forall {n m o} (zx1 : ZX n m) (zx2 : ZX m o), + (zx1 ⟷ zx2) ⊤ = (zx2⊤ ⟷ zx1⊤). +Proof. + reflexivity. +Qed. + +Lemma compose_transpose : forall {n m o} (zx1 : ZX n m) (zx2 : ZX m o), + (zx1 ⟷ zx2) ⊤ ∝= (zx2⊤ ⟷ zx1⊤). Proof. - intros. - prop_exists_nonzero 1. - simpl. - lma. + reflexivity. Qed. (* Empty diagram removal *) Lemma compose_empty_r : forall {nIn} (zx : ZX nIn 0), - zx ⟷ ⦰ ∝ zx. + zx ⟷ ⦰ ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - reflexivity. + apply (Mmult_1_l _ _). + auto_wf. Qed. Lemma compose_empty_l : forall {nOut} (zx : ZX 0 nOut), - ⦰ ⟷ zx ∝ zx. + ⦰ ⟷ zx ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - reflexivity. + apply (Mmult_1_r _ _). + auto_wf. Qed. -Lemma nwire_removal_l: forall {n nOut} (zx : ZX n nOut), (n ↑ —) ⟷ zx ∝ zx. +Lemma nwire_removal_l: forall {n nOut} (zx : ZX n nOut), + n_wire n ⟷ zx ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - rewrite n_wire_semantics. - Msimpl. - reflexivity. + unfold proportional_by_1. + cbn. + now rewrite n_wire_semantics, Mmult_1_r by auto_wf. Qed. -Lemma wire_removal_l : forall {nOut} (zx : ZX 1 nOut), — ⟷ zx ∝ zx. +Lemma nwire_removal_r: forall {n nIn} (zx : ZX nIn n), zx ⟷ n_wire n ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - reflexivity. + unfold proportional_by_1. + cbn. + now rewrite n_wire_semantics, Mmult_1_l by auto_wf. Qed. -Lemma wire_removal_r : forall {nIn} (zx : ZX nIn 1), zx ⟷ — ∝ zx. +Lemma wire_removal_l : forall {nOut} (zx : ZX 1 nOut), — ⟷ zx ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - reflexivity. + apply (Mmult_1_r _ _). + auto_wf. Qed. -Lemma nwire_removal_r: forall {n nIn} (zx : ZX nIn n), zx ⟷ (n ↑ —) ∝ zx. +Lemma wire_removal_r : forall {nIn} (zx : ZX nIn 1), zx ⟷ — ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - replace (n ↑ —) with (n_wire n) by easy. - rewrite n_wire_semantics. - Msimpl. - reflexivity. -Qed. + apply (Mmult_1_l _ _). + auto_wf. +Qed. \ No newline at end of file diff --git a/src/CoreRules/CoreAutomation.v b/src/CoreRules/CoreAutomation.v index f9483c9..04ec146 100644 --- a/src/CoreRules/CoreAutomation.v +++ b/src/CoreRules/CoreAutomation.v @@ -4,25 +4,10 @@ Require Import StackRules. Require Import WireRules. Require Import StackComposeRules. -Ltac wire_to_n_wire_safe_aux zx := - match zx with - | ?n ↑ — => idtac (* Guards from recursively unfolding n_wire into (n ↑ (n_wire 1)) *) - | ?n ↑ ?zx => wire_to_n_wire_safe_aux zx - | ?zx1 ↕ ?zx2 => wire_to_n_wire_safe_aux zx1; wire_to_n_wire_safe_aux zx2 - | ?zx1 ⟷ ?zx2 => wire_to_n_wire_safe_aux zx1; wire_to_n_wire_safe_aux zx2 - | — => rewrite wire_to_n_wire - | cast _ _ _ _ ?zx => wire_to_n_wire_safe_aux zx - | _ => idtac - end. - -Ltac wire_to_n_wire_safe := -match goal with - | [ |- ?zx1 ∝ ?zx2] => try (wire_to_n_wire_safe_aux zx1); try (wire_to_n_wire_safe_aux zx2); repeat rewrite n_stack_n_wire_1_n_wire -end. - -Tactic Notation "bundle_wires" := wire_to_n_wire_safe; (* change wires to n_wires *) - repeat rewrite n_wire_stack; (* stack n_wire *) - repeat rewrite <- wire_to_n_wire. (* restore *) +(** Combine stacks of [n_wire] and [—] ([Wire]), restoring + [n_wire 1] to [—] at the end. *) +Ltac bundle_wires := + rewrite ?wire_to_n_wire, ?n_wire_stack, <- 1?wire_to_n_wire. #[export] Hint Rewrite (fun n => @compose_empty_l n) @@ -39,26 +24,61 @@ 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. -Tactic Notation "cleanup_zx" := auto_cast_eqn (autorewrite with cleanup_zx_db). + +(** Simplify the goal by [autorewrite with cleanup_zx_db], solving + as many side-conditions as possible with [lia]. *) +Ltac cleanup_zx := auto_cast_eqn (autorewrite with cleanup_zx_db). #[export] Hint Rewrite (fun n m o p => @cast_colorswap n m o p) (fun n => @n_wire_colorswap n) - (fun n => @n_stack1_colorswap n) - (fun n m o => @n_stack_colorswap n m o) + (fun n => @nstack1_colorswap n) + (fun n m o => @nstack_colorswap n m o) : colorswap_db. #[export] Hint Rewrite (fun n m o p => @cast_transpose n m o p) (fun n => @n_wire_transpose n) - (fun n => @n_stack1_transpose n) - (fun n => @n_stack_transpose n) + (fun n => @nstack1_transpose n) + (fun n => @nstack_transpose n) : transpose_db. #[export] Hint Rewrite (fun n m o p => @cast_adj n m o p) : adjoint_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. +(** Solve the goal by showing it is the transpose of the term/lemma [H]. + Specifically, transposes the goal, e.g. by applying [transpose_digrams], + simplifies by [autorewrite with transpose_db] and [simpl], and applies [H]. *) +Ltac transpose_of H := + intros; + first [apply transpose_diagrams + | apply transpose_diagrams_by + | apply transpose_diagrams_eq + | apply transpose_zx]; + repeat (simpl; autorewrite with transpose_db); + apply H. + +(** Solve the goal by showing it is the adjoint of the term [H]. + Specifically, adjoints the goal, e.g. by applying [adjoint_digrams], + simplifies by [autorewrite with adjoint_db] and [simpl], and applies [H]. *) +Ltac adjoint_of H := + intros; + first [apply adjoint_diagrams + | apply adjoint_diagrams_by + | apply adjoint_diagrams_eq + | apply adjoint_zx]; + repeat (simpl; autorewrite with adjoint_db); + apply H. + +(** Solve the goal by showing it is the colorswap of the term [H]. + Specifically, colorswaps the goal, e.g. by applying [colorswap_digrams], + simplifies by [autorewrite with colorswap_db] and [simpl], and applies [H]. *) +Ltac colorswap_of H := + intros; + first [apply colorswap_diagrams + | apply colorswap_diagrams_by + | apply colorswap_diagrams_eq + | apply colorswap_zx]; + repeat (simpl; autorewrite with colorswap_db); + apply H. diff --git a/src/CoreRules/SpiderInduction.v b/src/CoreRules/SpiderInduction.v index 6ed8d68..f3bdd02 100644 --- a/src/CoreRules/SpiderInduction.v +++ b/src/CoreRules/SpiderInduction.v @@ -13,6 +13,8 @@ Open Scope ZX_scope. Cmult_1_l : cleanup_C_db. +(** Abbreviates [autorewrite with cleanup_C_db], which contains the most basic + simplification lemmas for multiplication and addition of complex numbers. *) Ltac cleanup_C := autorewrite with cleanup_C_db. (* The first part that is necessary to prove spider edge count induction is the @@ -20,66 +22,37 @@ Ltac cleanup_C := autorewrite with cleanup_C_db. the others follow through transposes *) Lemma grow_Z_left_2_1 : forall {n} α, - Z (S (S n)) 1 α ∝ + Z (S (S n)) 1 α ∝= (Z 2 1 0 ↕ n_wire n) ⟷ Z (S n) 1 α. Proof. assert ( pow2Pos : forall n, exists m, (2^n = S m)%nat ). - { induction n; - [ simpl; exists 0%nat; reflexivity | - destruct IHn; simpl; rewrite H; exists (S (x + x)); lia ]. } + { intros n. + enough (2 ^ n <> O)%nat. + + destruct (2 ^ n)%nat; [easy | eexists; easy]. + + apply Modulus.pow2_nonzero. } assert ( eqb_succ_f : forall j, (j =? S j)%nat = false ). - { induction j; auto. } + { intros. Modulus.bdestructΩ'. } assert ( div_1_comp : forall i, ((S (i + i) / S i) = 1)%nat). { intros. - replace (S (i + i))%nat with (2 * (S i) - 1)%nat by lia. - assert (S i <> 0)%nat by easy. - assert (2 * S i - 1 < S i * 2)%nat by lia. - specialize (Nat.div_lt_upper_bound (2 * S i - 1) (S i) (2) H H0). - intros. - assert (0 < S i <= 2 * S i - 1)%nat by lia. - specialize (Nat.div_str_pos (2 * S i - 1) (S i) H2). - intros. - destruct((2 * S i - 1) / S i)%nat. - - contradict H3; lia. - - destruct n; auto. - contradict H1; lia. } + rewrite Kronecker.div_eq_iff; lia. } assert ( div_3_comp : forall i, ((S (S (S (i + i + (i + i)))) / S i) = 3)%nat). { intros. - replace (S (S (S (i + i + (i + i)))))%nat with (4 * (S i) - 1)%nat by lia. - assert (S i <> 0)%nat by easy. - assert (4 * S i - 1 < S i * 4)%nat by lia. - specialize (Nat.div_lt_upper_bound (4 * S i - 1) (S i) (4) H H0). - intros. - assert (S i * 3 <= 4 * S i - 1)%nat by lia. - specialize (Nat.div_le_lower_bound (4 * S i - 1) (S i) 3 H H2). - intros. - destruct ((4 * S i - 1) / S i)%nat; [ contradict H3; lia | ]; - destruct n; [ contradict H3; lia | ]; - destruct n; [ contradict H3; lia | ]; - destruct n; [ auto | contradict H1; lia ]. } + rewrite Kronecker.div_eq_iff; lia. } assert ( mod_2_comp : forall i, ((S (i + i)) mod (S i) = i)%nat ). { intros. rewrite plus_n_Sm. - rewrite Nat.add_mod by lia. - rewrite Nat.mod_same by lia. - rewrite Nat.add_0_r. - rewrite Nat.mod_mod by lia. + rewrite Modulus.mod_add_n_r. apply Nat.mod_small; lia. } assert ( mod_4_comp : forall i, ((S (S (S (i + i + (i + i))))) mod (S i) = i)%nat ). { intros. replace (S (S (S (i + i + (i + i))))) - with ((S i) + ((S i) + ((S i) + i)))%nat by lia. - repeat (rewrite Nat.add_mod by lia; - rewrite Nat.mod_same by lia; - rewrite Nat.add_0_l). - repeat rewrite Nat.mod_mod by lia. + with (i + S i + S i + S i)%nat by lia. + rewrite !Modulus.mod_add_n_r. apply Nat.mod_small; lia. } intros. - simpl. - prop_exists_nonzero 1. - Msimpl. + unfold proportional_by_1. simpl. rewrite n_wire_semantics. unfold Mmult. @@ -178,7 +151,9 @@ Proof. * destruct (S (S y) / (S (S m)))%nat eqn:E; try lca. rewrite Nat.div_small_iff in E by auto. rewrite (Nat.mod_small (S (S y))) by auto. - repeat rewrite Nat.mod_0_l by auto. + cbn. + rewrite Nat.sub_diag. + cbn. lca. * lca. * lca. @@ -195,27 +170,28 @@ Proof. with ((Z_Spider (S (S n))%nat 1 α)⊤) by reflexivity. rewrite grow_Z_left_2_1. simpl. - rewrite nstack1_transpose. - rewrite transpose_wire. + rewrite n_wire_transpose. reflexivity. Qed. Lemma grow_Z_right_bot_1_2_base : forall α, - Z 1 3 α ∝ Z 1 2 α ⟷ (— ↕ Z 1 2 0). + Z 1 3 α ∝= Z 1 2 α ⟷ (— ↕ Z 1 2 0). Proof. - intros. prop_exists_nonzero 1. simpl; Msimpl. unfold Z_semantics. - gridify. - solve_matrix. + intros. + unfold proportional_by_1. + lma'. + unfold Z_semantics, kron; + cbn. rewrite Cexp_0. lca. Qed. Lemma Z_wrap_over_top_right_base : forall n α, - (— ↕ Z n 2 α) ⟷ (Cap ↕ —) ∝ Z (S n) 1 α. + (— ↕ Z n 2 α) ⟷ (Cap ↕ —) ∝= Z (S n) 1 α. Proof. intros. - prop_exists_nonzero 1. - simpl; Msimpl. + unfold proportional_by_1. + cbn. unfold Z_semantics, kron, Mmult. prep_matrix_equality. replace (2 ^ S n)%nat with (2 ^ n + 2 ^ n)%nat by (simpl; lia). @@ -326,11 +302,11 @@ Proof. Qed. Lemma Z_wrap_over_top_right_0 : forall n α, - (— ↕ Z n 1 α) ⟷ Cap ∝ Z (S n) 0 α. + (— ↕ Z n 1 α) ⟷ Cap ∝= Z (S n) 0 α. Proof. intros. - prop_exists_nonzero 1. - simpl; Msimpl. + unfold proportional_by_1. + cbn. unfold Z_semantics, kron, Mmult. prep_matrix_equality. replace (2 ^ S n)%nat with (2 ^ n + 2 ^ n)%nat by (simpl; lia). @@ -451,12 +427,15 @@ Proof. Qed. Lemma Z_wrap_over_top_left_0 : forall n α, - Cup ⟷ (— ↕ Z 1 n α) ∝ Z 0 (S n) α. + Cup ⟷ (— ↕ Z 1 n α) ∝= Z 0 (S n) α. Proof. intros. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. apply Z_wrap_over_top_right_0. Qed. +(** Inducts on [n] and specializes the case where [n = 1]. Useful for + induction on spiders where both the [n = 0] and [n = 1] cases are + special, whereas normal induction has only [n = 0] as base case. *) Ltac spider_induction n := induction n; [ | destruct n ]. diff --git a/src/CoreRules/StackComposeRules.v b/src/CoreRules/StackComposeRules.v index d1bbb4c..f07f36c 100644 --- a/src/CoreRules/StackComposeRules.v +++ b/src/CoreRules/StackComposeRules.v @@ -8,88 +8,74 @@ Require Export ComposeRules. Local Open Scope ZX_scope. Lemma nwire_stack_compose_topleft : forall {topIn botIn topOut botOut} (zx0 : ZX botIn botOut) (zx1 : ZX topIn topOut), -((n_wire topIn) ↕ zx0) ⟷ (zx1 ↕ (n_wire botOut)) ∝ -(zx1 ↕ zx0). + ((n_wire topIn) ↕ zx0) ⟷ (zx1 ↕ (n_wire botOut)) ∝= + (zx1 ↕ zx0). Proof. intros. - prop_exists_nonzero 1. - simpl. - repeat rewrite n_wire_semantics. - Msimpl. - easy. + unfold proportional_by_1. + cbn. + rewrite 2!n_wire_semantics. + restore_dims. + rewrite kron_mixed_product. + now Msimpl. Qed. Lemma nwire_stack_compose_botleft : forall {topIn botIn topOut botOut} (zx0 : ZX botIn botOut) (zx1 : ZX topIn topOut), -(zx0 ↕ (n_wire topIn)) ⟷ ((n_wire botOut) ↕ zx1) ∝ -(zx0 ↕ zx1). + (zx0 ↕ (n_wire topIn)) ⟷ ((n_wire botOut) ↕ zx1) ∝= + (zx0 ↕ zx1). Proof. intros. - prop_exists_nonzero 1. - simpl. - repeat rewrite n_wire_semantics. - Msimpl. - easy. + unfold proportional_by_1. + cbn. + rewrite 2!n_wire_semantics. + restore_dims. + rewrite kron_mixed_product. + now Msimpl. Qed. -Lemma push_out_top : forall {nIn nOut nOutAppendix} (appendix : ZX 0 nOutAppendix) (zx : ZX nIn nOut), - appendix ↕ zx ∝ zx ⟷ (appendix ↕ (n_wire nOut)). +Lemma push_out_top : forall {nIn nOut nOutAppendix} + (appendix : ZX 0 nOutAppendix) (zx : ZX nIn nOut), + appendix ↕ zx ∝= zx ⟷ (appendix ↕ (n_wire nOut)). Proof. intros. rewrite <- (stack_empty_l zx) at 2. - replace ⦰ with (n_wire 0) by easy. rewrite (nwire_stack_compose_topleft zx appendix). easy. Qed. -Lemma push_out_bot : forall {nIn nOut nOutAppendix} (appendix : ZX 0 nOutAppendix) (zx : ZX nIn nOut) prfn prfm, - zx ↕ appendix ∝ (cast _ _ prfn prfm zx) ⟷ ((n_wire nOut) ↕ appendix). +Lemma push_out_bot : forall {nIn nOut nOutAppendix} + (appendix : ZX 0 nOutAppendix) (zx : ZX nIn nOut) prfn prfm, + zx ↕ appendix ∝= (cast _ _ prfn prfm zx) ⟷ ((n_wire nOut) ↕ appendix). Proof. intros. - auto_cast_eqn (rewrite (stack_empty_r_rev ($ _, _ ::: zx $))). - replace ⦰ with (n_wire 0) by easy. - prop_exists_nonzero 1. - simpl. - simpl_cast_semantics. - simpl. - simpl_cast_semantics. - restore_dims. - rewrite kron_mixed_product. - rewrite n_wire_semantics. - Msimpl. - easy. + rewrite <- stack_empty_r. + now rewrite <- stack_compose_distr, compose_empty_l, nwire_removal_r. Qed. -Lemma pull_out_top : forall {nIn nOut nInAppendix} (appendix : ZX nInAppendix 0) (zx : ZX nIn nOut), - appendix ↕ zx ∝ (appendix ↕ (n_wire nIn)) ⟷ zx. +Lemma pull_out_top : forall {nIn nOut nInAppendix} + (appendix : ZX nInAppendix 0) (zx : ZX nIn nOut), + appendix ↕ zx ∝= (appendix ↕ (n_wire nIn)) ⟷ zx. Proof. intros. rewrite <- (stack_empty_l zx) at 2. - replace ⦰ with (n_wire 0) by easy. rewrite (nwire_stack_compose_botleft appendix zx). easy. Qed. -Lemma pull_out_bot : forall {nIn nOut nInAppendix} (appendix : ZX nInAppendix 0) (zx : ZX nIn nOut) prfn prfm, - zx ↕ appendix ∝ ((n_wire nIn) ↕ appendix) ⟷ (cast _ _ prfn prfm zx). +Lemma pull_out_bot : forall {nIn nOut nInAppendix} + (appendix : ZX nInAppendix 0) (zx : ZX nIn nOut) prfn prfm, + zx ↕ appendix ∝= ((n_wire nIn) ↕ appendix) ⟷ (cast _ _ prfn prfm zx). Proof. intros. - auto_cast_eqn (rewrite (stack_empty_r_rev ($ _, _ ::: zx $))). - replace ⦰ with (n_wire 0) by easy. - prop_exists_nonzero 1. - simpl. - simpl_cast_semantics. - simpl. - simpl_cast_semantics. - restore_dims. - rewrite kron_mixed_product. - rewrite n_wire_semantics. - Msimpl. - easy. + rewrite <- stack_empty_r. + rewrite <- stack_compose_distr. + now rewrite nwire_removal_l, compose_empty_r. Qed. -Lemma disconnected_stack_compose_l : forall {n m} (zxIn : ZX n 0) (zxOut : ZX 0 m) prfn prfm, - zxIn ↕ zxOut ∝ cast _ _ prfn prfm (zxIn ⟷ zxOut). +Lemma disconnected_stack_compose_l : forall {n m} + (zxIn : ZX n 0) (zxOut : ZX 0 m) prfn prfm, + zxIn ↕ zxOut ∝= cast _ _ prfn prfm (zxIn ⟷ zxOut). Proof. intros. rewrite <- (compose_empty_l zxOut) at 1. @@ -103,7 +89,7 @@ Proof. Qed. Lemma disconnected_stack_compose_r : forall {n m} (zxIn : ZX n 0) (zxOut : ZX 0 m) prfn prfm, - zxOut ↕ zxIn ∝ cast _ _ prfn prfm (zxIn ⟷ zxOut). + zxOut ↕ zxIn ∝= cast _ _ prfn prfm (zxIn ⟷ zxOut). Proof. intros. rewrite <- (compose_empty_l zxOut) at 1. diff --git a/src/CoreRules/StackRules.v b/src/CoreRules/StackRules.v index 8cc8e57..3ccf261 100644 --- a/src/CoreRules/StackRules.v +++ b/src/CoreRules/StackRules.v @@ -4,107 +4,90 @@ Require Import SpiderInduction. Local Open Scope ZX_scope. -Lemma stack_semantics {n m o p} : forall (zx0 : ZX n m) (zx1 : ZX o p), - ⟦ zx0 ↕ zx1 ⟧ = ⟦ zx0 ⟧ ⊗ ⟦ zx1 ⟧. -Proof. easy. Qed. - -Lemma compose_semantics {n m o} : forall (zx0 : ZX n m) (zx1 : ZX m o), -⟦ zx0 ⟷ zx1 ⟧ = @Mmult (2 ^ n) (2 ^ m) (2 ^ o) (⟦ zx1 ⟧) (⟦ zx0 ⟧). -Proof. easy. Qed. - Lemma stack_assoc : forall {n0 n1 n2 m0 m1 m2} (zx0 : ZX n0 m0) (zx1 : ZX n1 m1) (zx2 : ZX n2 m2) prfn prfm, - (zx0 ↕ zx1) ↕ zx2 ∝ + (zx0 ↕ zx1) ↕ zx2 ∝= cast _ _ prfn prfm (zx0 ↕ (zx1 ↕ zx2)). -Proof. +Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - rewrite (@cast_semantics (n0 + (n1 + n2)) _ ((n0 + n1) + n2)%nat). - rewrite kron_assoc; auto with wf_db. + unfold proportional_by_1. + simpl_cast_semantics. + cbn. + restore_dims. + now rewrite kron_assoc by auto_wf. Qed. Lemma stack_assoc_back : forall {n0 n1 n2 m0 m1 m2} (zx0 : ZX n0 m0) (zx1 : ZX n1 m1) (zx2 : ZX n2 m2) prfn prfm, - zx0 ↕ (zx1 ↕ zx2) ∝ + zx0 ↕ (zx1 ↕ zx2) ∝= cast (n0 + (n1 + n2)) (m0 + (m1 + m2)) prfn prfm ((zx0 ↕ zx1) ↕ zx2). -Proof. +Proof. intros. - rewrite <- cast_symm. - rewrite <- stack_assoc. - easy. -Unshelve. -all: lia. + unfold proportional_by_1. + simpl_cast_semantics. + cbn. + restore_dims. + now rewrite kron_assoc by auto_wf. Qed. Lemma stack_empty_l : forall {nIn nOut} (zx : ZX nIn nOut), - ⦰ ↕ zx ∝ zx. + ⦰ ↕ zx ∝= zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - rewrite kron_1_l; try auto with wf_db. - lma. + unfold proportional_by_1. + cbn. + restore_dims. + now rewrite kron_1_l by auto_wf. Qed. Lemma stack_empty_r : forall {n m : nat} (zx : ZX n m) prfn prfm, - zx ↕ ⦰ ∝ + zx ↕ ⦰ ∝= cast (n + 0) (m + 0) prfn prfm zx. Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. - rewrite (@cast_semantics n m (n + 0) (m + 0)). - reflexivity. + unfold proportional_by_1. + simpl_cast_semantics. + cbn. + restore_dims. + now rewrite kron_1_r by auto_wf. Qed. -Lemma stack_empty_r_rev : forall {n m : nat} (zx : ZX n m) prfn prfm, - zx ∝ +Lemma stack_empty_r_back : forall {n m : nat} (zx : ZX n m) prfn prfm, + zx ∝= cast _ _ prfn prfm (zx ↕ ⦰). Proof. intros. - prop_exists_nonzero 1. - simpl. - Msimpl. + unfold proportional_by_1. simpl_cast_semantics. - simpl. - Msimpl. - reflexivity. + cbn. + restore_dims. + now rewrite kron_1_r by auto_wf. Qed. -Lemma stack_simplify : forall {n1 m1 n2 m2} +Lemma stack_simplify_eq : forall {n1 m1 n2 m2} (zx1 zx3 : ZX n1 m1) (zx2 zx4 : ZX n2 m2), - zx1 ∝ zx3 -> zx2 ∝ zx4 -> zx1 ↕ zx2 ∝ zx3 ↕ zx4. + zx1 ∝= zx3 -> zx2 ∝= zx4 -> zx1 ↕ zx2 ∝= zx3 ↕ zx4. Proof. - intros. - rewrite H, H0. - easy. + now intros * -> ->. Qed. -Lemma stack_transpose : forall {n1 m1 n2 m2} (zx1 : ZX n1 m1) (zx2 : ZX n2 m2), (zx1 ↕ zx2) ⊤ ∝ (zx1⊤ ↕ zx2⊤). +Lemma stack_simplify : forall {n1 m1 n2 m2} + (zx1 zx3 : ZX n1 m1) (zx2 zx4 : ZX n2 m2), + zx1 ∝ zx3 -> zx2 ∝ zx4 -> zx1 ↕ zx2 ∝ zx3 ↕ zx4. Proof. - intros. - prop_exists_nonzero 1. - simpl. - lma. + now intros * -> ->. Qed. -Lemma n_stack1_transpose : forall n (zx : ZX 1 1), (n ↑ zx)⊤ ∝ (n ↑ zx⊤). +Lemma stack_transpose : forall {n1 m1 n2 m2} (zx1 : ZX n1 m1) (zx2 : ZX n2 m2), + (zx1 ↕ zx2) ⊤ = (zx1⊤ ↕ zx2⊤). Proof. - intros. - induction n. - - easy. - - simpl. - rewrite IHn. - easy. + reflexivity. Qed. -Lemma n_stack1_colorswap : forall n (zx : ZX 1 1), ⊙(n ↑ zx) ∝ (n ↑ (⊙ zx)). +Lemma nstack1_colorswap : forall n (zx : ZX 1 1), ⊙(n ↑ zx) = (n ↑ (⊙ zx)). Proof. intros. induction n. @@ -114,17 +97,17 @@ Proof. easy. Qed. -Lemma n_stack_transpose : forall n (zx : ZX 1 1), (n ⇑ zx)⊤ ∝ (n ⇑ zx⊤). +Lemma nstack_transpose : forall k {n m} (zx : ZX n m), (k ⇑ zx)⊤ = (k ⇑ zx⊤). Proof. intros. - induction n. + induction k. - easy. - simpl. - rewrite IHn. + rewrite IHk. easy. Qed. -Lemma n_stack_colorswap : forall n {n' m'} (zx : ZX n' m'), ⊙(n ⇑ zx) ∝ (n ⇑ (⊙ zx)). +Lemma nstack_colorswap : forall n {n' m'} (zx : ZX n' m'), ⊙(n ⇑ zx) = (n ⇑ (⊙ zx)). Proof. intros. induction n. @@ -134,74 +117,102 @@ Proof. easy. Qed. -Lemma n_stack1_l : forall n (zx : ZX 1 1), - (S n) ↑ zx ∝ zx ↕ (n ↑ zx). +Lemma n_stack1_succ_l : forall n (zx : ZX 1 1), + (S n) ↑ zx = zx ↕ (n ↑ zx). Proof. easy. Qed. -Lemma n_stack1_r : forall n (zx : ZX 1 1) prfn prfm, - (S n) ↑ zx ∝ +Lemma n_stack1_succ_r : forall n (zx : ZX 1 1) prfn prfm, + (S n) ↑ zx ∝= cast (S n) (S n) prfn prfm ((n ↑ zx) ↕ zx). Proof. -induction n. -- intros. - simpl. - simpl_casts. - rewrite stack_empty_l, stack_empty_r. - simpl_casts. - easy. -- intros. - rewrite n_stack1_l. - rewrite IHn at 1. - rewrite cast_stack_r. - simpl. - simpl_casts. - rewrite stack_assoc_back. - simpl_casts. - easy. + intros. + induction n. + - cbn. + now rewrite stack_empty_r, 2!cast_id_eq, stack_empty_l. + - rewrite n_stack1_succ_l. + rewrite IHn at 1. + rewrite cast_stack_r. + simpl. + simpl_casts. + rewrite stack_assoc_back. + simpl_casts. + easy. Unshelve. all: lia. Qed. Lemma stack_wire_distribute_l : forall {n m o} (zx0 : ZX n m) (zx1 : ZX m o), - — ↕ (zx0 ⟷ zx1) ∝ (— ↕ zx0) ⟷ (— ↕ zx1). + — ↕ (zx0 ⟷ zx1) ∝= (— ↕ zx0) ⟷ (— ↕ zx1). Proof. intros. - prop_exists_nonzero 1. + unfold proportional_by_1. simpl; Msimpl; easy. Qed. Lemma stack_wire_distribute_r : forall {n m o} (zx0 : ZX n m) (zx1 : ZX m o), - (zx0 ⟷ zx1) ↕ — ∝ (zx0 ↕ —) ⟷ (zx1 ↕ —). + (zx0 ⟷ zx1) ↕ — ∝= (zx0 ↕ —) ⟷ (zx1 ↕ —). Proof. intros. - prop_exists_nonzero 1. + unfold proportional_by_1. simpl; Msimpl; easy. Qed. Lemma stack_nwire_distribute_l : forall {n m o p} (zx0 : ZX n m) (zx1 : ZX m o), - n_wire p ↕ (zx0 ⟷ zx1) ∝ (n_wire p ↕ zx0) ⟷ (n_wire p ↕ zx1). + n_wire p ↕ (zx0 ⟷ zx1) ∝= (n_wire p ↕ zx0) ⟷ (n_wire p ↕ zx1). +Proof. + intros. + unfold proportional_by_1. + cbn; rewrite n_wire_semantics; Msimpl; reflexivity. +Qed. + +Lemma stack_nwire_distribute_r : forall {n m o p} (zx0 : ZX n m) (zx1 : ZX m o), + (zx0 ⟷ zx1) ↕ n_wire p ∝= (zx0 ↕ n_wire p) ⟷ (zx1 ↕ n_wire p). Proof. intros. induction p. - - repeat rewrite stack_empty_l. easy. - - rewrite n_stack1_l. - rewrite (stack_assoc — (n_wire p) zx0). - rewrite (stack_assoc — (n_wire p) zx1). + - repeat rewrite stack_empty_r. + eapply (cast_diagrams_eq n o). + repeat rewrite cast_contract. + rewrite cast_id. + rewrite cast_compose_distribute. simpl_casts. - rewrite <- (stack_wire_distribute_l (n_wire p ↕ zx0) (n_wire p ↕ zx1)). - rewrite <- IHp. - rewrite stack_assoc_back. + erewrite (cast_compose_mid m _ _ ($ n, m + 0 ::: zx0 $)). simpl_casts. easy. -Unshelve. -all: lia. + Unshelve. + all: lia. + - unfold n_wire. + rewrite n_stack1_succ_r. + repeat rewrite cast_stack_r. + eapply (cast_diagrams_eq (n + (p + 1)) (o + (p + 1))). + rewrite cast_contract. + rewrite cast_id. + rewrite cast_compose_distribute. + simpl_casts. + erewrite (cast_compose_mid (m + (p + 1)) _ _ + ($ n + (p + 1), m + (S p) ::: zx0 ↕ (n_wire p ↕ —)$)). + simpl_casts. + rewrite 3 stack_assoc_back. + eapply (cast_diagrams_eq (n + p + 1) (o + p + 1)). + rewrite cast_contract. + rewrite cast_id. + rewrite cast_compose_distribute. + rewrite 2 cast_contract. + erewrite (cast_compose_mid (m + p + 1) _ _ + ($ n + p + 1, m + (p + 1) ::: zx0 ↕ n_wire p ↕ — $)). + simpl_casts. + rewrite <- stack_wire_distribute_r. + rewrite <- IHp. + easy. + Unshelve. + all: lia. Qed. (* Lemma n_wire_collapse_r : forall {n0 n1 m1} (zx0 : ZX n0 0) (zx1 : ZX n1 m1), (zx0 ↕ n_wire n1) ⟷ zx1 ∝ zx0 ↕ zx1. *) Lemma nstack1_split : forall n m (zx : ZX 1 1), - (n + m) ↑ zx ∝ + (n + m) ↑ zx ∝= (n ↑ zx) ↕ (m ↑ zx). Proof. intros. @@ -217,7 +228,7 @@ all: lia. Qed. Lemma nstack_split : forall n m {nIn mOut} (zx : ZX nIn mOut) prfn prfm, - (n + m) ⇑ zx ∝ + (n + m) ⇑ zx ∝= cast _ _ prfn prfm ((n ⇑ zx) ↕ (m ⇑ zx)). Proof. intros. @@ -235,7 +246,7 @@ Unshelve. all: lia. Qed. -Lemma nstack1_1 : forall zx, 1 ↑ zx ∝ zx. +Lemma nstack1_1 : forall zx, 1 ↑ zx ∝= zx. Proof. intros. simpl. @@ -246,5 +257,5 @@ Unshelve. all: lia. Qed. -Lemma nstack1_0 : forall zx, 0 ↑ zx ∝ ⦰. +Lemma nstack1_0 : forall zx, 0 ↑ zx = ⦰. Proof. easy. Qed. \ No newline at end of file diff --git a/src/CoreRules/SwapRules.v b/src/CoreRules/SwapRules.v index ffb85fe..f1f6a07 100644 --- a/src/CoreRules/SwapRules.v +++ b/src/CoreRules/SwapRules.v @@ -6,12 +6,15 @@ Require Import CastRules. Lemma swap_compose : - ⨉ ⟷ ⨉ ∝ n_wire 2. -Proof. solve_prop 1. Qed. + ⨉ ⟷ ⨉ ∝= n_wire 2. +Proof. + lma'. +Qed. Global Hint Rewrite swap_compose : cleanup_zx_db. -Lemma top_wire_to_bottom_ind : forall n, top_wire_to_bottom (S (S n)) = @Mmult _ (2 ^ (S (S n))) _ ((I 2) ⊗ top_wire_to_bottom (S n)) (swap ⊗ (I (2 ^ n))). +Lemma top_wire_to_bottom_ind : forall n, top_wire_to_bottom (S (S n)) = + @Mmult _ (2 ^ (S (S n))) _ ((I 2) ⊗ top_wire_to_bottom (S n)) (swap ⊗ (I (2 ^ n))). Proof. intros. induction n. @@ -41,9 +44,10 @@ Proof. destruct n; [ easy | ]. induction n. - easy. - - simpl. + - cbn. simpl in IHn. rewrite <- IHn. + fold (n_wire n). rewrite n_wire_semantics. rewrite kron_n_I. rewrite 2 id_kron. @@ -75,28 +79,30 @@ Qed. Lemma swap_spec' : swap = ((ket 0 × bra 0) ⊗ (ket 0 × bra 0) .+ (ket 0 × bra 1) ⊗ (ket 1 × bra 0) .+ (ket 1 × bra 0) ⊗ (ket 0 × bra 1) .+ (ket 1 × bra 1) ⊗ (ket 1 × bra 1)). Proof. - solve_matrix. + prep_matrix_equivalence. + by_cell; lazy; lca. Qed. Lemma top_to_bottom_grow_l : forall n, - top_to_bottom (S (S n)) ∝ (⨉ ↕ n_wire n) ⟷ (— ↕ top_to_bottom (S n)). -Proof. easy. Qed. + top_to_bottom (S (S n)) = (⨉ ↕ n_wire n) ⟷ (— ↕ top_to_bottom (S n)). +Proof. reflexivity. Qed. Lemma top_to_bottom_grow_r : forall n prf prf', - top_to_bottom (S (S n)) ∝ cast _ _ prf' prf' (top_to_bottom (S n) ↕ —) ⟷ (cast _ _ prf prf (n_wire n ↕ ⨉)). + top_to_bottom (S (S n)) ∝= + cast _ _ prf' prf' (top_to_bottom (S n) ↕ —) ⟷ + (cast _ _ prf prf (n_wire n ↕ ⨉)). Proof. intros. induction n. - + simpl; cleanup_zx; simpl_casts. + + cbn. + rewrite stack_empty_r, stack_empty_l, !cast_id_eq. bundle_wires. - cleanup_zx. - easy. + now rewrite nwire_removal_l, nwire_removal_r. + simpl. simpl in IHn. - rewrite IHn at 1. - simpl_casts. + rewrite IHn at 1. rewrite (stack_assoc — (n_wire n) ⨉). - simpl_casts. + rewrite cast_id_eq. erewrite (@cast_stack_distribute _ 1 _ 1 _ _ _ _ _ _ _ _ _ _ — (n_wire n ↕ ⨉)). @@ -110,37 +116,41 @@ Proof. rewrite cast_compose_distribute. rewrite stack_wire_distribute_l. rewrite <- compose_assoc. - apply compose_simplify; [ | easy ]. + apply compose_simplify_eq; [ | easy ]. bundle_wires. repeat rewrite cast_id. symmetry. erewrite (cast_compose_mid (S (S (S n)))). simpl_casts. - apply compose_simplify; [ | rewrite (stack_assoc_back — (top_to_bottom_helper n) —); simpl_casts; easy ]. - eapply (cast_diagrams (2 + (1 + n)) (2 + (1 + n))). + apply compose_simplify_eq; + [ | rewrite (stack_assoc_back — (top_to_bottom_helper n) —), !cast_id_eq; + cast_irrelevance ]. + eapply (cast_diagrams_eq (2 + (1 + n)) (2 + (1 + n))). rewrite cast_contract. rewrite (stack_assoc ⨉ (n_wire n) —). rewrite cast_contract. rewrite cast_stack_distribute. bundle_wires. rewrite cast_n_wire. - simpl_casts. - easy. + now rewrite !cast_id_eq. Unshelve. all: lia. Qed. Lemma offset_swaps_comm_top_left : - ⨉ ↕ — ⟷ (— ↕ ⨉) ∝ + ⨉ ↕ — ⟷ (— ↕ ⨉) ∝= — ↕ ⨉ ⟷ (⨉ ↕ —) ⟷ (— ↕ ⨉) ⟷ (⨉ ↕ —). Proof. (* solve_prop 1. Qed. *) Admitted. Lemma offset_swaps_comm_bot_right : - — ↕ ⨉ ⟷ (⨉ ↕ —) ∝ + — ↕ ⨉ ⟷ (⨉ ↕ —) ∝= ⨉ ↕ — ⟷ (— ↕ ⨉) ⟷ (⨉ ↕ —) ⟷ (— ↕ ⨉). Proof. (* solve_prop 1. Qed. *) Admitted. -Lemma bottom_wire_to_top_ind : forall n, bottom_wire_to_top (S (S n)) = @Mmult _ (2 ^ (S (S n))) _ (swap ⊗ (I (2 ^ n))) ((I 2) ⊗ bottom_wire_to_top (S n)). +Lemma bottom_wire_to_top_ind : forall n, + bottom_wire_to_top (S (S n)) = + @Mmult _ (2 ^ (S (S n))) _ (swap ⊗ (I (2 ^ n))) + ((I 2) ⊗ bottom_wire_to_top (S n)). Proof. intros. apply transpose_matrices. @@ -161,7 +171,7 @@ Proof. Qed. Lemma bottom_to_top_grow_r : forall n, - bottom_to_top (S (S n)) ∝ (— ↕ bottom_to_top (S n)) ⟷ (⨉ ↕ n_wire n). + bottom_to_top (S (S n)) = (— ↕ bottom_to_top (S n)) ⟷ (⨉ ↕ n_wire n). Proof. intros. unfold bottom_to_top. @@ -172,17 +182,15 @@ Qed. Lemma bottom_to_top_grow_l : forall n prf prf', - bottom_to_top (S (S n)) ∝ cast _ _ prf' prf'((cast _ _ prf prf (n_wire n ↕ ⨉)) ⟷ (bottom_to_top (S n) ↕ —)). + bottom_to_top (S (S n)) ∝= cast _ _ prf' prf'((cast _ _ prf prf (n_wire n ↕ ⨉)) ⟷ (bottom_to_top (S n) ↕ —)). Proof. intros. - apply transpose_diagrams. -Opaque top_to_bottom. - simpl. + apply transpose_diagrams_eq. unfold bottom_to_top. rewrite cast_transpose. - simpl. + cbn -[top_to_bottom]. repeat rewrite cast_transpose. - simpl. + cbn -[top_to_bottom]. rewrite n_wire_transpose. repeat rewrite Proportional.transpose_involutive. rewrite top_to_bottom_grow_r. @@ -190,31 +198,30 @@ Opaque top_to_bottom. simpl_casts. erewrite (cast_compose_mid (S (n + 1))). simpl_casts. - apply compose_simplify; cast_irrelevance. + apply compose_simplify_eq; cast_irrelevance. Unshelve. all: lia. Qed. -Transparent top_to_bottom. -Lemma top_to_bottom_transpose : forall n, (top_to_bottom n)⊤ ∝ bottom_to_top n. +Lemma top_to_bottom_transpose : forall n, (top_to_bottom n)⊤ = bottom_to_top n. Proof. - intros. - unfold bottom_to_top. - easy. + reflexivity. Qed. -Lemma bottom_to_top_transpose : forall n, (bottom_to_top n)⊤ ∝ top_to_bottom n. +Lemma bottom_to_top_transpose : forall n, (bottom_to_top n)⊤ = top_to_bottom n. Proof. intros. unfold bottom_to_top. - rewrite Proportional.transpose_involutive. + rewrite Proportional.transpose_involutive_eq. easy. Qed. -Lemma a_swap_grow : forall n, a_swap (S (S (S n))) ∝ (⨉ ↕ n_wire (S n)) ⟷ (— ↕ a_swap (S (S n))) ⟷ (⨉ ↕ n_wire (S n)). +Lemma a_swap_grow : forall n, a_swap (S (S (S n))) ∝= + (⨉ ↕ n_wire (S n)) ⟷ (— ↕ a_swap (S (S n))) ⟷ (⨉ ↕ n_wire (S n)). Proof. intros. - remember (⨉ ↕ n_wire S n ⟷ (— ↕ a_swap (S (S n))) ⟷ (⨉ ↕ n_wire S n)) as right_side. + remember (⨉ ↕ n_wire (S n) ⟷ (— ↕ a_swap (S (S n))) ⟷ (⨉ ↕ n_wire (S n))) + as right_side. unfold a_swap at 1. rewrite bottom_to_top_grow_r. rewrite top_to_bottom_grow_l. @@ -249,6 +256,7 @@ Proof. repeat rewrite compose_assoc. rewrite (nwire_stack_compose_botleft ⨉ (top_to_bottom_helper n)). rewrite <- (nwire_stack_compose_topleft (top_to_bottom_helper n) ⨉). + unfold n_wire. simpl. rewrite stack_empty_r. simpl_casts. @@ -256,19 +264,19 @@ Proof. simpl_casts. rewrite Heqright_side. repeat rewrite compose_assoc. - apply compose_simplify; [ easy | ]. + apply compose_simplify_eq; [ easy | ]. repeat rewrite <- compose_assoc. - apply compose_simplify; [ | easy ]. + apply compose_simplify_eq; [ | easy ]. simpl. rewrite <- 2 stack_wire_distribute_l. - apply stack_simplify; [ easy | ]. + apply stack_simplify_eq; [ easy | ]. rewrite <- bottom_to_top_grow_r. easy. Unshelve. all: lia. Qed. -Lemma a_swap_2_is_swap : a_swap 2 ∝ ⨉. +Lemma a_swap_2_is_swap : a_swap 2 ∝= ⨉. Proof. unfold a_swap. unfold bottom_to_top. @@ -282,16 +290,19 @@ Qed. Lemma a_swap_3_order_indep : - I 2 ⊗ swap × (swap ⊗ I 2) × (I 2 ⊗ swap) = (swap ⊗ I 2) × (I 2 ⊗ swap) × (swap ⊗ I 2). + I 2 ⊗ swap × (swap ⊗ I 2) × (I 2 ⊗ swap) = + (swap ⊗ I 2) × (I 2 ⊗ swap) × (swap ⊗ I 2). Proof. (* solve_matrix *) (* Commented out for performance*) Admitted. -Lemma a_swap_semantics_ind : forall n, a_swap_semantics (S (S (S n))) = swap ⊗ (I (2 ^ (S n))) × (I 2 ⊗ a_swap_semantics (S (S n))) × (swap ⊗ (I (2 ^ (S n)))). +Lemma a_swap_semantics_ind : forall n, a_swap_semantics (S (S (S n))) = + swap ⊗ (I (2 ^ (S n))) × (I 2 ⊗ a_swap_semantics (S (S n))) × (swap ⊗ (I (2 ^ (S n)))). Proof. intros. rewrite <- 2 a_swap_correct. simpl. + fold (n_wire n). repeat rewrite kron_id_dist_l by shelve. restore_dims. rewrite <- 2 (kron_assoc (I 2) (I 2) (_)) by shelve. @@ -344,16 +355,15 @@ all: try (apply WF_kron; try lia; replace (2 ^ n + (2 ^ n + 0))%nat with (2 ^ (S Qed. Lemma a_swap_transpose : forall n, - (a_swap n) ⊤ ∝ a_swap n. + (a_swap n) ⊤ ∝= a_swap n. Proof. intros. - strong induction n. + induction n using strong_induction. destruct n; [ easy | ]. destruct n; [ simpl; cleanup_zx; simpl_casts; easy | ]. destruct n; [ rewrite a_swap_2_is_swap; easy | ]. rewrite a_swap_grow. -Local Opaque a_swap. - simpl. + cbn -[a_swap]. repeat rewrite n_wire_transpose. rewrite compose_assoc. rewrite H by lia. @@ -364,7 +374,7 @@ Qed. Opaque a_swap a_swap_semantics. (* For n_swap proofs we don't want a_swap to unfold, instead we use lemmata from above*) -Lemma n_swap_2_is_swap : n_swap 2 ∝ ⨉. +Lemma n_swap_2_is_swap : n_swap 2 ∝= ⨉. Proof. intros. simpl. @@ -377,7 +387,7 @@ Proof. easy. Qed. -Lemma n_swap_1_is_wire : n_swap 1 ∝ —. +Lemma n_swap_1_is_wire : n_swap 1 ∝= —. Proof. simpl. cleanup_zx. @@ -386,18 +396,17 @@ Proof. Qed. Lemma n_swap_grow_l : forall n, - n_swap (S n) ∝ bottom_to_top (S n) ⟷ (— ↕ n_swap n). + n_swap (S n) ∝= bottom_to_top (S n) ⟷ (— ↕ n_swap n). Proof. induction n. - simpl. cleanup_zx. easy. - - simpl. - easy. + - reflexivity. Qed. Lemma n_swap_grow_r : forall n, - n_swap (S n) ∝ (— ↕ n_swap n) ⟷ top_to_bottom (S n). + n_swap (S n) ∝= (— ↕ n_swap n) ⟷ top_to_bottom (S n). Proof. induction n. - simpl. @@ -425,13 +434,14 @@ Proof. rewrite (stack_assoc_back — — (n_swap _)). cleanup_zx. simpl_casts. - easy. + bundle_wires. + reflexivity. Unshelve. all: lia. Qed. Lemma n_swap_transpose : forall n, - (n_swap n) ⊤ ∝ n_swap n. + (n_swap n) ⊤ ∝= n_swap n. Proof. induction n; try easy. - simpl. @@ -451,7 +461,7 @@ Qed. : transpose_db. Lemma top_to_bottom_colorswap : forall n, - ⊙ (top_to_bottom n) ∝ top_to_bottom n. + ⊙ (top_to_bottom n) = top_to_bottom n. Proof. destruct n; [ easy | ]. induction n. @@ -464,7 +474,7 @@ Proof. Qed. Lemma bottom_to_top_colorswap : forall n, - ⊙ (bottom_to_top n) ∝ bottom_to_top n. + ⊙ (bottom_to_top n) = bottom_to_top n. Proof. destruct n; [easy | ]. induction n. @@ -481,7 +491,7 @@ Proof. Qed. Lemma a_swap_colorswap : forall n, - ⊙ (a_swap n) ∝ a_swap n. + ⊙ (a_swap n) = a_swap n. Proof. induction n. - easy. @@ -493,7 +503,7 @@ Proof. Qed. Lemma n_swap_colorswap : forall n, - ⊙ (n_swap n) ∝ n_swap n. + ⊙ (n_swap n) = n_swap n. Proof. induction n. - easy. @@ -510,42 +520,19 @@ Qed. (fun n => @n_swap_colorswap n) : colorswap_db. -Lemma swap_pullthrough_top_right_Z_1_1 : forall α, (Z 1 1 α) ↕ — ⟷ ⨉ ∝ ⨉ ⟷ (— ↕ (Z 1 1 α)). -Proof. intros. solve_prop 1. Qed. +Lemma swap_pullthrough_top_right_Z_1_1 : forall α, + (Z 1 1 α) ↕ — ⟷ ⨉ ∝= ⨉ ⟷ (— ↕ (Z 1 1 α)). +Proof. intros. lma'. Qed. -Lemma swap_pullthrough_top_right_Z : forall n α prfn prfm, ((Z (S n) 1 α) ↕ —) ⟷ ⨉ ∝ cast _ _ prfn prfm (n_swap _ ⟷ (— ↕ (Z (S n) 1 α))). +Lemma swap_pullthrough_top_right_Z : forall n α prfn prfm, + ((Z (S n) 1 α) ↕ —) ⟷ ⨉ ∝= + cast _ _ prfn prfm (n_swap _ ⟷ (— ↕ (Z (S n) 1 α))). Proof. - intro n. - induction n; intros. - - simpl_casts. - cleanup_zx. - rewrite n_swap_2_is_swap. - rewrite swap_pullthrough_top_right_Z_1_1. - easy. - - rewrite SpiderInduction.grow_Z_left_2_1 at 1. - rewrite stack_wire_distribute_r. - rewrite compose_assoc. - rewrite IHn. - simpl_casts. - rewrite n_swap_grow_l. - rewrite compose_assoc. - rewrite (cast_compose_mid_contract _ (S (S n))). - simpl_casts. - rewrite (stack_assoc (Z 2 1 _) (n_wire n) —). - bundle_wires. - rewrite bottom_to_top_grow_r. - simpl_casts. - rewrite (cast_compose_mid (S (S n))). - erewrite <- (@cast_n_wire (S n)). - rewrite cast_stack_r. - rewrite cast_contract. - simpl_casts. - erewrite (cast_compose_mid_contract _ (S (S n)) _ _ _ _ _ _ _ (— ↕ bottom_to_top (S n)) (⨉ ↕ n_wire n)). - simpl_casts. Abort. -Lemma swap_pullthrough_top_right_X_1_1 : forall α, (X 1 1 α) ↕ — ⟷ ⨉ ∝ ⨉ ⟷ (— ↕ (X 1 1 α)). +Lemma swap_pullthrough_top_right_X_1_1 : forall α, + (X 1 1 α) ↕ — ⟷ ⨉ ∝= ⨉ ⟷ (— ↕ (X 1 1 α)). Proof. intros. colorswap_of swap_pullthrough_top_right_Z_1_1. Qed. diff --git a/src/CoreRules/WireRules.v b/src/CoreRules/WireRules.v index 1ae874b..d0c4776 100644 --- a/src/CoreRules/WireRules.v +++ b/src/CoreRules/WireRules.v @@ -4,177 +4,94 @@ Require Import CastRules. Local Open Scope ZX_scope. -Lemma Z_0_is_wire : Z 1 1 0 ∝ —. +Lemma Z_0_is_wire : Z 1 1 0 ∝= —. Proof. - intros. - prop_exists_nonzero 1. - simpl. - unfold Z_semantics. - autorewrite with Cexp_db. - solve_matrix. - assert (forall x y, (x =? 0) && (y =? 0) = (x =? y) && (x <=? 0))%nat. - { - intros. - bdestruct (x0 <=? 0). - - apply Nat.le_0_r in H; subst. - rewrite Nat.eqb_refl, andb_true_r, andb_true_l. - destruct y0; easy. - - rewrite andb_false_r. - destruct x0; easy. - } - rewrite H. - easy. + lma'. + now rewrite Cexp_0. Qed. -Lemma Z_2_0_0_is_cap : Z 2 0 0 ∝ ⊃. +Lemma Z_2_0_0_is_cap : Z 2 0 0 ∝= ⊃. Proof. - prop_exists_nonzero 1. - simpl. - solve_matrix. - apply Cexp_0. + lma'. + now rewrite Cexp_0. Qed. -Lemma Z_0_2_0_is_cup : Z 0 2 0 ∝ ⊂. +Lemma Z_0_2_0_is_cup : Z 0 2 0 ∝= ⊂. Proof. - prop_exists_nonzero 1. - simpl. - solve_matrix. - apply Cexp_0. + lma'. + now rewrite Cexp_0. Qed. Lemma yank_r : - (⊂ ↕ —) ⟷ (— ↕ ⊃) ∝ —. + (⊂ ↕ —) ⟷ (— ↕ ⊃) ∝= —. Proof. - prop_exists_nonzero 1. - simpl. - solve_matrix. + lma'. Qed. Lemma yank_l : - (— ↕ ⊂) ⟷ (⊃ ↕ —) ∝ —. + (— ↕ ⊂) ⟷ (⊃ ↕ —) ∝= —. Proof. - prop_exists_nonzero 1. - simpl. - solve_matrix. + lma'. Qed. -Lemma n_wire_stack : forall n m, n_wire n ↕ n_wire m ∝ n_wire (n + m). -Proof. - prop_exists_nonzero 1. - simpl. - rewrite 3 n_wire_semantics, id_kron. - Msimpl. - rewrite Nat.pow_add_r. - easy. +Lemma n_wire_stack : forall n m, + n_wire n ↕ n_wire m ∝= n_wire (n + m). +Proof. + intros n m. + unfold proportional_by_1. + cbn. + rewrite 3!n_wire_semantics. + rewrite id_kron. + now unify_pows_two. Qed. -Lemma X_0_is_wire : X 1 1 0 ∝ —. +Lemma X_0_is_wire : X 1 1 0 ∝= —. Proof. - apply colorswap_diagrams. + apply colorswap_diagrams_eq. simpl. apply Z_0_is_wire. Qed. -Lemma stack_nwire_distribute_r : forall {n m o p} (zx0 : ZX n m) (zx1 : ZX m o), -(zx0 ⟷ zx1) ↕ n_wire p ∝ (zx0 ↕ n_wire p) ⟷ (zx1 ↕ n_wire p). -Proof. - intros. - induction p. - - repeat rewrite stack_empty_r. - eapply (cast_diagrams n o). - repeat rewrite cast_contract. - rewrite cast_id. - rewrite cast_compose_distribute. - simpl_casts. - erewrite (cast_compose_mid m _ _ ($ n, m + 0 ::: zx0 $)). - simpl_casts. - easy. - Unshelve. - all: lia. - - rewrite n_stack1_r. - repeat rewrite cast_stack_r. - eapply (cast_diagrams (n + (p + 1)) (o + (p + 1))). - rewrite cast_contract. - rewrite cast_id. - rewrite cast_compose_distribute. - simpl_casts. - erewrite (cast_compose_mid (m + (p + 1)) _ _ - ($ n + (p + 1), m + (S p) ::: zx0 ↕ (n_wire p ↕ —)$)). - simpl_casts. - rewrite 3 stack_assoc_back. - eapply (cast_diagrams (n + p + 1) (o + p + 1)). - rewrite cast_contract. - rewrite cast_id. - rewrite cast_compose_distribute. - rewrite 2 cast_contract. - erewrite (cast_compose_mid (m + p + 1) _ _ - ($ n + p + 1, m + (p + 1) ::: zx0 ↕ n_wire p ↕ — $)). - simpl_casts. - rewrite <- stack_wire_distribute_r. - rewrite <- IHp. - easy. - Unshelve. - all: lia. -Qed. - Lemma wire_to_n_wire : - — ∝ n_wire 1. + — ∝= n_wire 1. Proof. - simpl. - auto_cast_eqn (rewrite stack_empty_r). - simpl_casts. - easy. + symmetry. + apply nstack1_1. Qed. -Lemma wire_transpose : —⊤ ∝ —. -Proof. easy. Qed. - -Lemma n_wire_transpose : forall n, (n_wire n)⊤ = n_wire n. -Proof. - intros. - induction n. - - easy. - - simpl. - rewrite IHn. - easy. -Qed. +Lemma wire_transpose : —⊤ = —. +Proof. reflexivity. Qed. Lemma n_wire_colorswap : forall n, ⊙ (n_wire n) = n_wire n. Proof. intros. - induction n. - - easy. - - simpl. - rewrite IHn. - easy. + apply nstack1_colorswap. Qed. -Lemma wire_loop : — ∝ (⊂ ↕ —) ⟷ (— ↕ ⨉) ⟷ (⊃ ↕ —). +Lemma wire_loop : — ∝= (⊂ ↕ —) ⟷ (— ↕ ⨉) ⟷ (⊃ ↕ —). Proof. - prop_exists_nonzero 1. - Msimpl; simpl. - solve_matrix. + unfold proportional_by_1. + prep_matrix_equivalence. + cbn. + rewrite 2!Kronecker.kron_I_r, Kronecker.kron_I_l. + by_cell; cbn; lca. Qed. -Lemma n_stack_n_wire_1_n_wire : forall n, n ↑ (n_wire 1) ∝ n_wire n. +Lemma n_stack_n_wire_1_n_wire : forall n, n ↑ (n_wire 1) ∝= n_wire n. Proof. - intros. rewrite <- wire_to_n_wire. easy. + intros. rewrite <- wire_to_n_wire. reflexivity. Qed. -Lemma n_wire_grow_r : forall n prfn prfm, n_wire (S n) ∝ cast _ _ prfn prfm (n_wire n ↕ —). +Lemma n_wire_grow_r : forall n prfn prfm, n_wire (S n) ∝= + cast _ _ prfn prfm (n_wire n ↕ —). Proof. intros. - rewrite wire_to_n_wire at 3. + rewrite wire_to_n_wire. rewrite n_wire_stack. - rewrite (@cast_n_wire (n + 1) (S n) prfn prfm). - easy. + now rewrite cast_n_wire. Qed. -Lemma box_compose : □ ⟷ □ ∝ —. +Lemma box_compose : □ ⟷ □ ∝= —. Proof. - prop_exists_nonzero 1. - Msimpl. - simpl. - rewrite MmultHH. - easy. + apply MmultHH. Qed. \ No newline at end of file diff --git a/src/CoreRules/XRules.v b/src/CoreRules/XRules.v index 7a7749d..3d31e56 100644 --- a/src/CoreRules/XRules.v +++ b/src/CoreRules/XRules.v @@ -6,145 +6,145 @@ Require Import SwapRules. Require Import ZRules. Lemma grow_X_top_left : forall (nIn nOut : nat) α, - X (S (S nIn)) nOut α ∝ + X (S (S nIn)) nOut α ∝= (X 2 1 0) ↕ (n_wire nIn) ⟷ (X (S nIn) nOut α). Proof. intros. colorswap_of grow_Z_top_left. Qed. Lemma grow_X_top_right : forall (nIn nOut : nat) α, - X nIn (S (S nOut)) α ∝ + X nIn (S (S nOut)) α ∝= (X nIn (S nOut) α) ⟷ ((X_Spider 1 2 0) ↕ (n_wire nOut)). Proof. intros. colorswap_of grow_Z_top_right. Qed. Lemma grow_X_bot_left : forall n {m o α}, - X (n + m) o α ∝ + X (n + m) o α ∝= (n_wire n ↕ X m 1 0) ⟷ X (n + 1) o α. Proof. intros. colorswap_of (@grow_Z_bot_left n m o α). Qed. Lemma grow_X_bot_right : forall {n m} o {α}, - X n (m + o) α ∝ + X n (m + o) α ∝= X n (m + 1) α ⟷ (n_wire m ↕ X 1 o 0). Proof. intros. colorswap_of (@grow_Z_bot_right n m o α). Qed. Lemma X_rot_l : forall n m α β, - X (S n) m (α + β) ∝ X 1 1 α ↕ n_wire n ⟷ X (S n) m β. + X (S n) m (α + β) ∝= X 1 1 α ↕ n_wire n ⟷ X (S n) m β. Proof. intros. colorswap_of Z_rot_l. Qed. Lemma X_rot_r : forall n m α β, - X n (S m) (α + β) ∝ X n (S m) α ⟷ (X 1 1 β ↕ n_wire m). + X n (S m) (α + β) ∝= X n (S m) α ⟷ (X 1 1 β ↕ n_wire m). Proof. intros. colorswap_of Z_rot_r. Qed. -Lemma X_add_r_base_rot : forall {n} m o {α}, X n (m + o) α ∝ X n 2 α ⟷ (X 1 m 0 ↕ X 1 o 0). +Lemma X_add_r_base_rot : forall {n} m o {α}, X n (m + o) α ∝= X n 2 α ⟷ (X 1 m 0 ↕ X 1 o 0). Proof. intros. colorswap_of (@Z_add_r_base_rot n). Qed. -Lemma X_add_l_base_rot : forall {n} m o {α}, X (n + m) o α ∝ (X n 1 0 ↕ X m 1 0) ⟷ X 2 o α. +Lemma X_add_l_base_rot : forall {n} m o {α}, X (n + m) o α ∝= (X n 1 0 ↕ X m 1 0) ⟷ X 2 o α. Proof. intros. colorswap_of (@Z_add_l_base_rot n). Qed. Lemma X_appendix_rot_l : forall n m α β, - X n m (α + β) ∝ (X 0 1 α ↕ n_wire n) ⟷ X (S n) m β. + X n m (α + β) ∝= (X 0 1 α ↕ n_wire n) ⟷ X (S n) m β. Proof. intros. colorswap_of Z_appendix_rot_l. Qed. Lemma X_appendix_rot_r : forall n m α β, - X n m (β + α) ∝ X n (S m) α ⟷ (X 1 0 β ↕ n_wire m). + X n m (β + α) ∝= X n (S m) α ⟷ (X 1 0 β ↕ n_wire m). Proof. intros. colorswap_of Z_appendix_rot_r. Qed. Lemma X_wrap_over_top_left : forall n m α, - X (S n) m α ∝ (Wire ↕ X n (S m) α) ⟷ (Cap ↕ n_wire m). + X (S n) m α ∝= (Wire ↕ X n (S m) α) ⟷ (Cap ↕ n_wire m). Proof. intros. colorswap_of Z_wrap_over_top_left. Qed. Lemma X_wrap_over_top_right : forall n m α, - X n (S m) α ∝ (Cup ↕ n_wire n) ⟷ (Wire ↕ X (S n) m α). + X n (S m) α ∝= (Cup ↕ n_wire n) ⟷ (Wire ↕ X (S n) m α). Proof. intros. colorswap_of Z_wrap_over_top_right. Qed. Lemma X_add_r : forall {n} m o {α β γ}, - X n (m + o) (α + β + γ) ∝ X n 2 β ⟷ (X 1 m α ↕ X 1 o γ). + X n (m + o) (α + β + γ) ∝= X n 2 β ⟷ (X 1 m α ↕ X 1 o γ). Proof. intros. colorswap_of (@Z_add_r n). Qed. Lemma X_add_l : forall n m {o α β γ}, - X (n + m) o (α + β + γ) ∝ (X n 1 α ↕ X m 1 γ) ⟷ X 2 o β. + X (n + m) o (α + β + γ) ∝= (X n 1 α ↕ X m 1 γ) ⟷ X 2 o β. Proof. intros. colorswap_of (@Z_add_l n m o). Qed. Lemma X_1_2_1_fusion : forall α β, - (X 1 2 α ⟷ X 2 1 β) ∝ (X 1 1 (α + β)). + (X 1 2 α ⟷ X 2 1 β) ∝= (X 1 1 (α + β)). Proof. intros. colorswap_of (Z_1_2_1_fusion). Qed. Lemma X_absolute_fusion : forall {n m o} α β, - (X n (S m) α ⟷ X (S m) o β) ∝ + (X n (S m) α ⟷ X (S m) o β) ∝= X n o (α + β). Proof. intros. colorswap_of (@Z_absolute_fusion n m o). Qed. Lemma dominated_X_spider_fusion_top_right : forall n m0 m1 o α β, - (X n (S m0) α ↕ n_wire m1 ⟷ X (S m0 + m1) o β) ∝ + (X n (S m0) α ↕ n_wire m1 ⟷ X (S m0 + m1) o β) ∝= X (n + m1) o (α + β). Proof. intros. colorswap_of dominated_Z_spider_fusion_top_right. Qed. Lemma dominated_X_spider_fusion_top_left : forall m n0 n1 i α β, - X i (S n0 + n1) β ⟷ (X (S n0) m α ↕ n_wire n1) ∝ + X i (S n0 + n1) β ⟷ (X (S n0) m α ↕ n_wire n1) ∝= X i (m + n1) (α + β). Proof. intros. colorswap_of dominated_Z_spider_fusion_top_left. Qed. Lemma dominated_X_spider_fusion_bot_right : forall n m0 m1 o α β, - ((n_wire m1 ↕ (X n (S m0) α)) ⟷ X (m1 + (S m0)) o β) ∝ + ((n_wire m1 ↕ (X n (S m0) α)) ⟷ X (m1 + (S m0)) o β) ∝= X (m1 + n) o (α + β). Proof. intros. colorswap_of dominated_Z_spider_fusion_bot_right. Qed. Lemma dominated_X_spider_fusion_bot_left : forall m n0 n1 i α β, - X i (n1 + S n0) β ⟷ (n_wire n1 ↕ X (S n0) m α) ∝ + X i (n1 + S n0) β ⟷ (n_wire n1 ↕ X (S n0) m α) ∝= X i (n1 + m) (α + β). Proof. intros. colorswap_of dominated_Z_spider_fusion_bot_left. Qed. Lemma X_spider_fusion_top_left_bot_right : forall top mid bot input output α β prfn prfm, X input (top + S mid) α ↕ n_wire bot ⟷ cast (top + (S mid) + bot) (top + output) prfn prfm - (n_wire top ↕ X (S mid + bot) output β) ∝ + (n_wire top ↕ X (S mid + bot) output β) ∝= X (input + bot) (top + output) (α + β). Proof. intros. colorswap_of Z_spider_fusion_top_left_bot_right. Qed. Lemma X_spider_fusion_bot_left_top_right : forall top mid bot input output α β prfn prfm, ((n_wire top ↕ X input (S mid + bot) α) ⟷ cast (top + ((S mid) + bot)) _ prfn prfm - (X (top + (S mid)) output β ↕ n_wire bot)) ∝ + (X (top + (S mid)) output β ↕ n_wire bot)) ∝= X (top + input) (output + bot) (β + α). Proof. intros. colorswap_of Z_spider_fusion_bot_left_top_right. Qed. -Lemma X_self_cap_absorbtion_base : forall {n} α, X n 2%nat α ⟷ ⊃ ∝ X n 0%nat α. +Lemma X_self_cap_absorbtion_base : forall {n} α, X n 2%nat α ⟷ ⊃ ∝= X n 0%nat α. Proof. intros. colorswap_of (@Z_self_cap_absorbtion_base n). Qed. -Lemma X_self_cap_absorbtion_top : forall {n m α}, (X) n (S (S m)) α ⟷ (⊃ ↕ n_wire m) ∝ X n m α. +Lemma X_self_cap_absorbtion_top : forall {n m α}, (X) n (S (S m)) α ⟷ (⊃ ↕ n_wire m) ∝= X n m α. Proof. intros. colorswap_of (@Z_self_cap_absorbtion_top n m). Qed. -Lemma X_self_cup_absorbtion_top : forall {n m α}, ((⊂ ↕ n_wire n) ⟷ X (S (S n)) m α) ∝ (X n m α). +Lemma X_self_cup_absorbtion_top : forall {n m α}, ((⊂ ↕ n_wire n) ⟷ X (S (S n)) m α) ∝= (X n m α). Proof. intros. colorswap_of (@Z_self_cup_absorbtion_top n m). Qed. -Lemma X_self_cap_absorbtion : forall {n m m' α}, X n (m + (S (S m'))) α ⟷ (n_wire m ↕ (⊃ ↕ n_wire m')) ∝ (X n (m + m') α). +Lemma X_self_cap_absorbtion : forall {n m m' α}, X n (m + (S (S m'))) α ⟷ (n_wire m ↕ (⊃ ↕ n_wire m')) ∝= (X n (m + m') α). Proof. intros. colorswap_of (@Z_self_cap_absorbtion n m m'). Qed. -Lemma X_self_cup_absorbtion : forall {n n' m α}, ((n_wire n ↕ (⊂ ↕ n_wire n')) ⟷ X (n + (S (S n'))) m α) ∝ (X (n + n') m α). +Lemma X_self_cup_absorbtion : forall {n n' m α}, ((n_wire n ↕ (⊂ ↕ n_wire n')) ⟷ X (n + (S (S n'))) m α) ∝= (X (n + n') m α). Proof. intros. colorswap_of (@Z_self_cup_absorbtion n n' m). Qed. -Lemma X_self_loop_removal_top : forall {n m α}, X n m α ∝ (⊂ ↕ n_wire n) ⟷ (— ↕ X (S n) (S m) α) ⟷ (⊃ ↕ n_wire m). +Lemma X_self_loop_removal_top : forall {n m α}, X n m α ∝= (⊂ ↕ n_wire n) ⟷ (— ↕ X (S n) (S m) α) ⟷ (⊃ ↕ n_wire m). Proof. intros. colorswap_of (@Z_self_loop_removal_top n m). Qed. -Lemma X_self_swap_absorbtion_right_base : forall {n α}, X n 2 α ⟷ ⨉ ∝ X n 2 α. +Lemma X_self_swap_absorbtion_right_base : forall {n α}, X n 2 α ⟷ ⨉ ∝= X n 2 α. Proof. intros. colorswap_of (@Z_self_swap_absorbtion_right_base n α). Qed. -Lemma X_self_swap_absorbtion_right_top : forall {n m α}, X n (S (S m)) α ⟷ (⨉ ↕ n_wire m) ∝ X n (S (S m)) α. +Lemma X_self_swap_absorbtion_right_top : forall {n m α}, X n (S (S m)) α ⟷ (⨉ ↕ n_wire m) ∝= X n (S (S m)) α. Proof. intros. colorswap_of (@Z_self_swap_absorbtion_right_top n m α). Qed. -Lemma X_self_swap_absorbtion_right : forall {n m m' α}, X n (m' + S (S m)) α ⟷ (n_wire m' ↕ (⨉ ↕ n_wire m)) ∝ X n (m' + S (S m)) α. +Lemma X_self_swap_absorbtion_right : forall {n m m' α}, X n (m' + S (S m)) α ⟷ (n_wire m' ↕ (⨉ ↕ n_wire m)) ∝= X n (m' + S (S m)) α. Proof. intros. colorswap_of (@Z_self_swap_absorbtion_right n m m' α). Qed. -Lemma X_self_swap_absorbtion_left_base : forall {m α}, (⨉ ⟷ X 2 m α) ∝ X 2 m α. +Lemma X_self_swap_absorbtion_left_base : forall {m α}, (⨉ ⟷ X 2 m α) ∝= X 2 m α. Proof. intros. colorswap_of (@Z_self_swap_absorbtion_left_base m α). Qed. -Lemma X_self_swap_absorbtion_left_top : forall {n m α}, ((⨉ ↕ n_wire n) ⟷ X (S (S n)) m α) ∝ X (S (S n)) m α. +Lemma X_self_swap_absorbtion_left_top : forall {n m α}, ((⨉ ↕ n_wire n) ⟷ X (S (S n)) m α) ∝= X (S (S n)) m α. Proof. intros. colorswap_of (@Z_self_swap_absorbtion_left_top n m α). Qed. -Lemma X_self_swap_absorbtion_left : forall {n n' m α}, ((n_wire n' ↕ (⨉ ↕ n_wire n)) ⟷ X (n' + S (S n)) m α) ∝ X (n' + S (S n)) m α. +Lemma X_self_swap_absorbtion_left : forall {n n' m α}, ((n_wire n' ↕ (⨉ ↕ n_wire n)) ⟷ X (n' + S (S n)) m α) ∝= X (n' + S (S n)) m α. Proof. intros. colorswap_of (@Z_self_swap_absorbtion_left n n' m α). Qed. Lemma X_wrap_under_bot_left : forall n m α prfn prfm, - X n (m + 1) α ∝ + X n (m + 1) α ∝= (cast n (n + 1 + 1) prfn prfm (n_wire n ↕ ⊂)) ⟷ @@ -152,7 +152,7 @@ Lemma X_wrap_under_bot_left : forall n m α prfn prfm, Proof. colorswap_of Z_wrap_under_bot_left. Qed. Lemma X_wrap_under_bot_right : forall n m α prfn prfm, - X (n + 1) m α ∝ + X (n + 1) m α ∝= (X n (m + 1) α ↕ —) ⟷ (cast (m + 1 + 1) m prfn @@ -160,43 +160,43 @@ Lemma X_wrap_under_bot_right : forall n m α prfn prfm, (n_wire m ↕ ⊃)). Proof. colorswap_of Z_wrap_under_bot_right. Qed. -Lemma X_self_top_to_bottom_absorbtion_right_base : forall n m α, X n m α ⟷ top_to_bottom m ∝ X n m α. +Lemma X_self_top_to_bottom_absorbtion_right_base : forall n m α, X n m α ⟷ top_to_bottom m ∝= X n m α. Proof. colorswap_of Z_self_top_to_bottom_absorbtion_right_base. Qed. -Lemma X_self_bottom_to_top_absorbtion_right_base : forall n m α, X n m α ⟷ bottom_to_top m ∝ X n m α. +Lemma X_self_bottom_to_top_absorbtion_right_base : forall n m α, X n m α ⟷ bottom_to_top m ∝= X n m α. Proof. colorswap_of Z_self_bottom_to_top_absorbtion_right_base. Qed. -Lemma X_a_swap_absorbtion_right_base : forall n m α, X n m α ⟷ a_swap m ∝ X n m α. +Lemma X_a_swap_absorbtion_right_base : forall n m α, X n m α ⟷ a_swap m ∝= X n m α. Proof. colorswap_of Z_a_swap_absorbtion_right_base. Qed. -Lemma X_n_swap_absorbtion_right_base : forall n m α, X n m α ⟷ n_swap m ∝ X n m α. +Lemma X_n_swap_absorbtion_right_base : forall n m α, X n m α ⟷ n_swap m ∝= X n m α. Proof. colorswap_of Z_n_swap_absorbtion_right_base. Qed. -Lemma X_n_wrap_under_r_base_unswapped : forall n m α, X (n + m) 0 α ∝ (X n m α ↕ n_wire m) ⟷ n_cup_unswapped m. +Lemma X_n_wrap_under_r_base_unswapped : forall n m α, X (n + m) 0 α ∝= (X n m α ↕ n_wire m) ⟷ n_cup_unswapped m. Proof. colorswap_of Z_n_wrap_under_r_base_unswapped. Qed. -Lemma X_n_wrap_under_r_base : forall n m α, X (n + m) 0 α ∝ (X n m α ↕ n_wire m) ⟷ n_cup m. +Lemma X_n_wrap_under_r_base : forall n m α, X (n + m) 0 α ∝= (X n m α ↕ n_wire m) ⟷ n_cup m. Proof. colorswap_of Z_n_wrap_under_r_base. Qed. -Lemma X_n_wrap_over_r_base_unswapped : forall n m α, X (m + n) 0 α ∝ (n_wire m ↕ X n m α) ⟷ n_cup_unswapped m. +Lemma X_n_wrap_over_r_base_unswapped : forall n m α, X (m + n) 0 α ∝= (n_wire m ↕ X n m α) ⟷ n_cup_unswapped m. Proof. colorswap_of Z_n_wrap_over_r_base_unswapped. Qed. -Lemma X_n_wrap_over_r_base : forall n m α, X (m + n) 0 α ∝ (n_wire m ↕ X n m α) ⟷ n_cup m. +Lemma X_n_wrap_over_r_base : forall n m α, X (m + n) 0 α ∝= (n_wire m ↕ X n m α) ⟷ n_cup m. Proof. colorswap_of Z_n_wrap_over_r_base. Qed. -Lemma X_n_wrap_over_l_base_unswapped : forall n m α, X 0 (n + m) α ∝ n_cap_unswapped n ⟷ (n_wire n ↕ X n m α). +Lemma X_n_wrap_over_l_base_unswapped : forall n m α, X 0 (n + m) α ∝= n_cap_unswapped n ⟷ (n_wire n ↕ X n m α). Proof. transpose_of X_n_wrap_over_r_base_unswapped. Qed. -Lemma X_n_wrap_over_l_base : forall n m α, X 0 (n + m) α ∝ n_cap n ⟷ (n_wire n ↕ X n m α). +Lemma X_n_wrap_over_l_base : forall n m α, X 0 (n + m) α ∝= n_cap n ⟷ (n_wire n ↕ X n m α). Proof. transpose_of X_n_wrap_over_r_base. Qed. -Lemma X_n_wrap_under_l_base_unswapped : forall n m α, X 0 (m + n) α ∝ n_cap_unswapped n ⟷ (X n m α ↕ n_wire n). +Lemma X_n_wrap_under_l_base_unswapped : forall n m α, X 0 (m + n) α ∝= n_cap_unswapped n ⟷ (X n m α ↕ n_wire n). Proof. transpose_of X_n_wrap_under_r_base_unswapped. Qed. -Lemma X_n_wrap_under_l_base : forall n m α, X 0 (m + n) α ∝ n_cap n ⟷ (X n m α ↕ n_wire n). +Lemma X_n_wrap_under_l_base : forall n m α, X 0 (m + n) α ∝= n_cap n ⟷ (X n m α ↕ n_wire n). Proof. transpose_of X_n_wrap_under_r_base. Qed. (* @nocheck name *) (* PI is captialized in Coq R *) -Lemma X_2_PI : forall n m a, X n m (INR a * 2 * PI) ∝ X n m 0. +Lemma X_2_PI : forall n m a, X n m (INR a * 2 * PI) ∝= X n m 0. Proof. colorswap_of Z_2_PI. Qed. diff --git a/src/CoreRules/ZRules.v b/src/CoreRules/ZRules.v index 6f6cae1..e23d56c 100644 --- a/src/CoreRules/ZRules.v +++ b/src/CoreRules/ZRules.v @@ -8,7 +8,7 @@ Require Import WireRules. Require Import SpiderInduction. Lemma grow_Z_top_left : forall (nIn nOut : nat) α, - Z (S (S nIn)) nOut α ∝ + Z (S (S nIn)) nOut α ∝= (Z 2 1 0) ↕ (n_wire nIn) ⟷ (Z (S nIn) nOut α). Proof. intros. @@ -24,48 +24,46 @@ Proof. Qed. Lemma grow_Z_top_right : forall (nIn nOut : nat) α, - Z nIn (S (S nOut)) α ∝ + Z nIn (S (S nOut)) α ∝= (Z nIn (S nOut) α) ⟷ ((Z_Spider 1 2 0) ↕ (n_wire nOut)). Proof. intros. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. - rewrite nstack1_transpose. - rewrite transpose_wire. + rewrite n_wire_transpose. apply grow_Z_top_left. Qed. Lemma grow_Z_bot_left : forall n {m o α}, - Z (n + m) o α ∝ + Z (n + m) o α ∝= (n_wire n ↕ Z m 1 0) ⟷ Z (n + 1) o α. Proof. Admitted. Lemma grow_Z_bot_right : forall {n m} o {α}, - Z n (m + o) α ∝ + Z n (m + o) α ∝= Z n (m + 1) α ⟷ (n_wire m ↕ Z 1 o 0). Proof. intros. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. - rewrite nstack1_transpose. - rewrite transpose_wire. + rewrite n_wire_transpose. apply grow_Z_bot_left. Qed. Lemma Z_rot_l : forall n m α β, - Z (S n) m (α + β) ∝ Z 1 1 α ↕ n_wire n ⟷ Z (S n) m β. + Z (S n) m (α + β) ∝= Z 1 1 α ↕ n_wire n ⟷ Z (S n) m β. Proof. assert (Z_rot_passthrough : forall α β, - (Z 1 1 α ↕ — ⟷ Z 2 1 β) ∝ Z 2 1 β ⟷ Z 1 1 α). - { solve_prop 1. } + (Z 1 1 α ↕ — ⟷ Z 2 1 β) ∝= Z 2 1 β ⟷ Z 1 1 α). + { intros; lma'. } induction n; intros. - cleanup_zx. simpl_casts. rewrite Z_spider_1_1_fusion. easy. - - simpl. + - cbn. rewrite (grow_Z_top_left n m β). rewrite <- compose_assoc. auto_cast_eqn (rewrite (stack_assoc_back (Z 1 1 α) —)). @@ -81,30 +79,29 @@ Proof. Qed. Lemma Z_rot_r : forall n m α β, - Z n (S m) (α + β) ∝ Z n (S m) α ⟷ (Z 1 1 β ↕ n_wire m). + Z n (S m) (α + β) ∝= Z n (S m) α ⟷ (Z 1 1 β ↕ n_wire m). Proof. intros. rewrite Rplus_comm. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. - rewrite nstack1_transpose. - rewrite transpose_wire. + rewrite n_wire_transpose. apply Z_rot_l. Qed. Lemma Z_appendix_rot_l : forall n m α β, - Z n m (α + β) ∝ (Z 0 1 α ↕ n_wire n) ⟷ Z (S n) m β. + Z n m (α + β) ∝= (Z 0 1 α ↕ n_wire n) ⟷ Z (S n) m β. Proof. assert (Z_appendix_base : forall α β, - (Z 0 1 α ↕ — ⟷ Z 2 1 β) ∝ Z 1 1 (α + β)). - { solve_prop 1. } + (Z 0 1 α ↕ — ⟷ Z 2 1 β) ∝= Z 1 1 (α + β)). + { intros; lma'. rewrite Cexp_add; lca. } induction n; intros. - cleanup_zx. simpl_casts. rewrite Z_spider_1_1_fusion. easy. - rewrite grow_Z_top_left. - simpl. + cbn. rewrite (stack_assoc_back (Z 0 1 α) —). simpl_casts. rewrite <- compose_assoc. @@ -118,18 +115,17 @@ all: lia. Qed. Lemma Z_appendix_rot_r : forall n m α β, - Z n m (β + α) ∝ Z n (S m) α ⟷ (Z 1 0 β ↕ n_wire m). + Z n m (β + α) ∝= Z n (S m) α ⟷ (Z 1 0 β ↕ n_wire m). Proof. intros. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. - rewrite nstack1_transpose. - rewrite transpose_wire. + rewrite n_wire_transpose. apply Z_appendix_rot_l. Qed. Lemma Z_wrap_over_top_left : forall n m α, - Z (S n) m α ∝ (Wire ↕ Z n (S m) α) ⟷ (Cap ↕ n_wire m). + Z (S n) m α ∝= (Wire ↕ Z n (S m) α) ⟷ (Cap ↕ n_wire m). Proof. induction m. - intros. @@ -188,15 +184,15 @@ all: lia. Qed. Lemma Z_wrap_over_top_right : forall n m α, - Z n (S m) α ∝ (Cup ↕ n_wire n) ⟷ (Wire ↕ Z (S n) m α). + Z n (S m) α ∝= (Cup ↕ n_wire n) ⟷ (Wire ↕ Z (S n) m α). Proof. - intros. apply transpose_diagrams. simpl. - rewrite nstack1_transpose. rewrite transpose_wire. + intros. apply transpose_diagrams_eq. simpl. + rewrite n_wire_transpose. apply Z_wrap_over_top_left. Qed. Lemma Z_add_r : forall {n} m o {α β γ}, - Z n (m + o) (α + β + γ) ∝ Z n 2 β ⟷ (Z 1 m α ↕ Z 1 o γ). + Z n (m + o) (α + β + γ) ∝= Z n 2 β ⟷ (Z 1 m α ↕ Z 1 o γ). Proof. intros. induction m. @@ -217,8 +213,7 @@ Proof. rewrite <- Z_rot_r. rewrite (Z_wrap_over_top_right n 1). simpl. - cleanup_zx. - simpl_casts. + bundle_wires. rewrite compose_assoc. rewrite <- stack_wire_distribute_l. rewrite Z_spider_1_1_fusion. @@ -233,7 +228,7 @@ Proof. rewrite <- IHm. rewrite (stack_assoc (Z 1 2 0) (n_wire m) (n_wire o)). simpl_casts. - rewrite <- nstack1_split. + rewrite n_wire_stack. rewrite <- (grow_Z_top_right n (m + o)). easy. Unshelve. @@ -241,10 +236,11 @@ all: lia. Qed. Lemma Z_add_l : forall n m {o α β γ}, - Z (n + m) o (α + β + γ) ∝ (Z n 1 α ↕ Z m 1 γ) ⟷ Z 2 o β. + Z (n + m) o (α + β + γ) ∝= (Z n 1 α ↕ Z m 1 γ) ⟷ Z 2 o β. Proof. intros. transpose_of (@Z_add_r o n m). Qed. -Lemma Z_add_r_base_rot : forall {n} m o {α}, Z n (m + o) α ∝ Z n 2 α ⟷ (Z 1 m 0 ↕ Z 1 o 0). +Lemma Z_add_r_base_rot : forall {n} m o {α}, Z n (m + o) α ∝= + Z n 2 α ⟷ (Z 1 m 0 ↕ Z 1 o 0). Proof. intros. rewrite <- (@Z_add_r n m o 0 α 0). @@ -252,15 +248,16 @@ Proof. easy. Qed. -Lemma Z_add_l_base_rot : forall {n} m o {α}, Z (n + m) o α ∝ (Z n 1 0 ↕ Z m 1 0) ⟷ Z 2 o α. +Lemma Z_add_l_base_rot : forall {n} m o {α}, Z (n + m) o α ∝= + (Z n 1 0 ↕ Z m 1 0) ⟷ Z 2 o α. Proof. intros. transpose_of (@Z_add_r_base_rot o n m). Qed. Lemma Z_1_2_1_fusion : forall α β, - (Z 1 2 α ⟷ Z 2 1 β) ∝ (Z 1 1 (α + β)). -Proof. solve_prop 1. Qed. + (Z 1 2 α ⟷ Z 2 1 β) ∝= (Z 1 1 (α + β)). +Proof. intros. lma'. rewrite Cexp_add; lca. Qed. Lemma Z_absolute_fusion : forall {n m o} α β, - (Z n (S m) α ⟷ Z (S m) o β) ∝ + (Z n (S m) α ⟷ Z (S m) o β) ∝= Z n o (α + β). Proof. intros. @@ -279,7 +276,7 @@ Proof. Qed. Lemma dominated_Z_spider_fusion_top_right : forall n m0 m1 o α β, - (Z n (S m0) α ↕ n_wire m1 ⟷ Z (S m0 + m1) o β) ∝ + (Z n (S m0) α ↕ n_wire m1 ⟷ Z (S m0 + m1) o β) ∝= Z (n + m1) o (α + β). Proof. intros. @@ -296,7 +293,7 @@ Qed. Lemma dominated_Z_spider_fusion_bot_right : forall n m0 m1 o α β, - ((n_wire m1 ↕ (Z n (S m0) α)) ⟷ Z (m1 + (S m0)) o β) ∝ + ((n_wire m1 ↕ (Z n (S m0) α)) ⟷ Z (m1 + (S m0)) o β) ∝= Z (m1 + n) o (α + β). Proof. intros. @@ -312,19 +309,19 @@ Proof. Qed. Lemma dominated_Z_spider_fusion_top_left : forall m n0 n1 i α β, - Z i (S n0 + n1) β ⟷ (Z (S n0) m α ↕ n_wire n1) ∝ + Z i (S n0 + n1) β ⟷ (Z (S n0) m α ↕ n_wire n1) ∝= Z i (m + n1) (α + β). Proof. intros. transpose_of dominated_Z_spider_fusion_top_right. Qed. Lemma dominated_Z_spider_fusion_bot_left : forall m n0 n1 i α β, - Z i (n1 + S n0) β ⟷ (n_wire n1 ↕ Z (S n0) m α) ∝ + Z i (n1 + S n0) β ⟷ (n_wire n1 ↕ Z (S n0) m α) ∝= Z i (n1 + m) (α + β). Proof. intros. transpose_of dominated_Z_spider_fusion_bot_right. Qed. Lemma Z_spider_fusion_top_left_bot_right : forall top mid bot input output α β prfn prfm, Z input (top + S mid) α ↕ n_wire bot ⟷ cast (top + (S mid) + bot) (top + output) prfn prfm - (n_wire top ↕ Z (S mid + bot) output β) ∝ + (n_wire top ↕ Z (S mid + bot) output β) ∝= Z (input + bot) (top + output) (α + β). Proof. intros. @@ -349,7 +346,7 @@ Proof. rewrite compose_assoc. rewrite <- (stack_compose_distr — (Z 1 top 0) (Z (S input) 1 α ↕ n_wire bot)). cleanup_zx. - rewrite wire_to_n_wire at 4. + rewrite wire_to_n_wire. rewrite <- compose_assoc. rewrite (nwire_stack_compose_botleft (Z (S input) 1 α)). rewrite <- Z_add_l. @@ -359,7 +356,7 @@ Proof. rewrite <- compose_assoc. rewrite (stack_assoc ⊂ (n_wire input)). simpl_casts. - rewrite <- nstack1_split. + rewrite n_wire_stack. rewrite <- (Z_wrap_over_top_right (input + bot)). rewrite (Z_add_r 1%nat output). rewrite compose_assoc. @@ -376,11 +373,11 @@ Qed. Lemma Z_spider_fusion_bot_left_top_right : forall top mid bot input output α β prfn prfm, ((n_wire top ↕ Z input (S mid + bot) α) ⟷ cast (top + ((S mid) + bot)) _ prfn prfm - (Z (top + (S mid)) output β ↕ n_wire bot)) ∝ + (Z (top + (S mid)) output β ↕ n_wire bot)) ∝= Z (top + input) (output + bot) (β + α). Proof. intros. - apply transpose_diagrams. + apply transpose_diagrams_eq. simpl. rewrite <- (Z_spider_fusion_top_left_bot_right top mid bot). autorewrite with transpose_db. @@ -393,33 +390,19 @@ Transparent cast. easy. Qed. -Lemma Z_self_cap_absorbtion_base : forall {n} α, Z n 2%nat α ⟷ ⊃ ∝ Z n 0%nat α. +Lemma Z_self_cap_absorbtion_base : forall {n} α, Z n 2%nat α ⟷ ⊃ ∝= + Z n 0%nat α. Proof. - intros. - prop_exists_nonzero 1. - Msimpl. - simpl. - solve_matrix. - replace ((2 ^ n + (2 ^ n + 0) - 1)%nat) with (2 ^ (S n) - 1)%nat by (simpl; lia). - assert (exists n', 2 ^ S n = (S (S n')))%nat. - { - intros. - induction n. - - exists 0%nat. - easy. - - destruct IHn. - rewrite Nat.pow_succ_r'. - rewrite H. - exists ((2 * x + 2))%nat. - lia. - } - destruct H. - rewrite H. - simpl. - lca. + intros n α. + rewrite <- (Rplus_0_l α). + rewrite <- 2!(@Z_absolute_fusion _ 0). + rewrite compose_assoc. + apply compose_simplify_eq; [reflexivity|]. + lma'. Qed. -Lemma Z_self_cap_absorbtion_top : forall {n m α}, (Z) n (S (S m)) α ⟷ (⊃ ↕ n_wire m) ∝ Z n m α. +Lemma Z_self_cap_absorbtion_top : forall {n m α}, + Z n (S (S m)) α ⟷ (⊃ ↕ n_wire m) ∝= Z n m α. Proof. intros. rewrite (Z_add_r_base_rot 2 m). @@ -431,10 +414,12 @@ Proof. easy. Qed. -Lemma Z_self_cup_absorbtion_top : forall {n m α}, ((⊂ ↕ n_wire n) ⟷ Z (S (S n)) m α) ∝ (Z n m α). +Lemma Z_self_cup_absorbtion_top : forall {n m α}, + ((⊂ ↕ n_wire n) ⟷ Z (S (S n)) m α) ∝= (Z n m α). Proof. intros. transpose_of (@Z_self_cap_absorbtion_top m n). Qed. -Lemma Z_self_cap_absorbtion : forall {n m m' α}, Z n (m + (S (S m'))) α ⟷ (n_wire m ↕ (⊃ ↕ n_wire m')) ∝ (Z n (m + m') α). +Lemma Z_self_cap_absorbtion : forall {n m m' α}, + Z n (m + (S (S m'))) α ⟷ (n_wire m ↕ (⊃ ↕ n_wire m')) ∝= (Z n (m + m') α). Proof. intros. rewrite Z_add_r_base_rot. @@ -446,10 +431,12 @@ Proof. easy. Qed. -Lemma Z_self_cup_absorbtion : forall {n n' m α}, ((n_wire n ↕ (⊂ ↕ n_wire n')) ⟷ Z (n + (S (S n'))) m α) ∝ (Z (n + n') m α). +Lemma Z_self_cup_absorbtion : forall {n n' m α}, + ((n_wire n ↕ (⊂ ↕ n_wire n')) ⟷ Z (n + (S (S n'))) m α) ∝= (Z (n + n') m α). Proof. intros. transpose_of (@Z_self_cap_absorbtion m n n'). Qed. -Lemma Z_self_loop_removal_top : forall {n m α}, Z n m α ∝ (⊂ ↕ n_wire n) ⟷ (— ↕ Z (S n) (S m) α) ⟷ (⊃ ↕ n_wire m). +Lemma Z_self_loop_removal_top : forall {n m α}, + Z n m α ∝= (⊂ ↕ n_wire n) ⟷ (— ↕ Z (S n) (S m) α) ⟷ (⊃ ↕ n_wire m). Proof. intros. rewrite <- Z_wrap_over_top_right. @@ -457,10 +444,18 @@ Proof. easy. Qed. -Lemma Z_self_swap_absorbtion_right_base : forall {n α}, Z n 2 α ⟷ ⨉ ∝ Z n 2 α. -Proof. intros. solve_prop 1. Qed. +Lemma Z_self_swap_absorbtion_right_base : forall {n α}, Z n 2 α ⟷ ⨉ ∝= Z n 2 α. +Proof. + intros n α. + rewrite <- (Rplus_0_l α). + rewrite <- (@Z_absolute_fusion _ 0). + rewrite compose_assoc. + apply compose_simplify_eq; [reflexivity|]. + lma'. +Qed. -Lemma Z_self_swap_absorbtion_right_top : forall {n m α}, Z n (S (S m)) α ⟷ (⨉ ↕ n_wire m) ∝ Z n (S (S m)) α. +Lemma Z_self_swap_absorbtion_right_top : forall {n m α}, + Z n (S (S m)) α ⟷ (⨉ ↕ n_wire m) ∝= Z n (S (S m)) α. Proof. intros. rewrite (Z_add_r_base_rot 2 m) at 1. @@ -472,7 +467,8 @@ Proof. easy. Qed. -Lemma Z_self_swap_absorbtion_right : forall {n m m' α}, Z n (m' + S (S m)) α ⟷ (n_wire m' ↕ (⨉ ↕ n_wire m)) ∝ Z n (m' + S (S m)) α. +Lemma Z_self_swap_absorbtion_right : forall {n m m' α}, + Z n (m' + S (S m)) α ⟷ (n_wire m' ↕ (⨉ ↕ n_wire m)) ∝= Z n (m' + S (S m)) α. Proof. intros. rewrite Z_add_r_base_rot at 1. @@ -484,18 +480,18 @@ Proof. easy. Qed. -Lemma Z_self_swap_absorbtion_left_base : forall {m α}, (⨉ ⟷ Z 2 m α) ∝ Z 2 m α. +Lemma Z_self_swap_absorbtion_left_base : forall {m α}, (⨉ ⟷ Z 2 m α) ∝= Z 2 m α. Proof. intros. transpose_of (@Z_self_swap_absorbtion_right_base m α). Qed. -Lemma Z_self_swap_absorbtion_left_top : forall {n m α}, ((⨉ ↕ n_wire n) ⟷ Z (S (S n)) m α) ∝ Z (S (S n)) m α. +Lemma Z_self_swap_absorbtion_left_top : forall {n m α}, ((⨉ ↕ n_wire n) ⟷ Z (S (S n)) m α) ∝= Z (S (S n)) m α. Proof. intros. transpose_of (@Z_self_swap_absorbtion_right_top m n α). Qed. -Lemma Z_self_swap_absorbtion_left : forall {n n' m α}, ((n_wire n' ↕ (⨉ ↕ n_wire n)) ⟷ Z (n' + S (S n)) m α) ∝ Z (n' + S (S n)) m α. +Lemma Z_self_swap_absorbtion_left : forall {n n' m α}, ((n_wire n' ↕ (⨉ ↕ n_wire n)) ⟷ Z (n' + S (S n)) m α) ∝= Z (n' + S (S n)) m α. Proof. intros. transpose_of (@Z_self_swap_absorbtion_right m n n' α). Qed. Lemma Z_wrap_under_bot_left : forall n m α prfn prfm, - Z n (m + 1) α ∝ + Z n (m + 1) α ∝= (cast n (n + 1 + 1) prfn prfm (n_wire n ↕ ⊂)) ⟷ @@ -508,7 +504,7 @@ Proof. rewrite stack_assoc. rewrite <- compose_assoc. simpl. - eapply (cast_diagrams (n + 0) (m + 1)). + eapply (cast_diagrams_eq (n + 0) (m + 1)). repeat rewrite cast_compose_distribute. simpl_casts. erewrite (@cast_compose_mid (n + 0) (n + 1 + 1) 3 (n + 2) _ _ ($ n + 0, n + 1 + 1 ::: n_wire n ↕ ⊂ $)). @@ -523,7 +519,7 @@ Proof. rewrite <- (nwire_removal_l (Z 0 2 0)). rewrite stack_compose_distr. rewrite compose_assoc. - rewrite wire_to_n_wire at 3. + rewrite wire_to_n_wire. specialize (Z_spider_fusion_bot_left_top_right 1 0 1 0 m 0 α); intros. specialize (H eq_refl eq_refl). @@ -541,7 +537,7 @@ all: lia. Qed. Lemma Z_wrap_under_bot_right : forall n m α prfn prfm, - Z (n + 1) m α ∝ + Z (n + 1) m α ∝= (Z n (m + 1) α ↕ —) ⟷ (cast (m + 1 + 1) m prfn @@ -549,7 +545,8 @@ Lemma Z_wrap_under_bot_right : forall n m α prfn prfm, (n_wire m ↕ ⊃)). Proof. transpose_of Z_wrap_under_bot_left. Qed. -Lemma Z_self_top_to_bottom_absorbtion_right_base : forall n m α, Z n m α ⟷ top_to_bottom m ∝ Z n m α. +Lemma Z_self_top_to_bottom_absorbtion_right_base : forall n m α, + Z n m α ⟷ top_to_bottom m ∝= Z n m α. Proof. intros. destruct m; [ simpl; cleanup_zx; easy | ]. @@ -567,7 +564,7 @@ Proof. - rewrite top_to_bottom_grow_r. erewrite <- (@cast_Z n _ ((S (S m)) + 1)). rewrite Z_add_r_base_rot. - rewrite (cast_compose_mid ((S (S m)) + 1)). + erewrite (cast_compose_mid ((S (S m)) + 1)). rewrite cast_contract. simpl_casts. rewrite compose_assoc. @@ -582,7 +579,7 @@ Proof. rewrite cast_Z. rewrite cast_compose_r. rewrite cast_Z. - rewrite (stack_empty_r_rev ⨉). + rewrite (stack_empty_r_back ⨉). replace ⦰ with (n_wire 0) by easy. rewrite cast_id. rewrite Z_self_swap_absorbtion_right. @@ -592,7 +589,8 @@ Unshelve. all: lia. Qed. -Lemma Z_self_bottom_to_top_absorbtion_right_base : forall n m α, Z n m α ⟷ bottom_to_top m ∝ Z n m α. +Lemma Z_self_bottom_to_top_absorbtion_right_base : forall n m α, + Z n m α ⟷ bottom_to_top m ∝= Z n m α. Proof. intros. destruct m; [ simpl; cleanup_zx; easy | ]. @@ -612,7 +610,7 @@ Proof. - rewrite bottom_to_top_grow_r. erewrite <- (@cast_Z n _ (1 + (S (S m)))). rewrite Z_add_r_base_rot. - rewrite (cast_compose_mid (1 + (S (S m)))). + erewrite (cast_compose_mid (1 + (S (S m)))). rewrite cast_contract. simpl_casts. rewrite compose_assoc. @@ -624,7 +622,7 @@ Proof. rewrite <- Z_add_r. rewrite <- (stack_empty_l ⨉). replace ⦰ with (n_wire 0) by easy. - rewrite <- (@cast_Z n _ (0 + (S (S (S m))))). + erewrite <- (@cast_Z n _ (0 + (S (S (S m))))). rewrite cast_compose_l. rewrite (stack_assoc (n_wire 0) ⨉ (n_wire _)). simpl_casts. @@ -634,7 +632,8 @@ Unshelve. all: lia. Qed. -Lemma Z_a_swap_absorbtion_right_base : forall n m α, Z n m α ⟷ a_swap m ∝ Z n m α. +Lemma Z_a_swap_absorbtion_right_base : forall n m α, + Z n m α ⟷ a_swap m ∝= Z n m α. Proof. intros. destruct m; [ simpl; cleanup_zx; easy | ]. @@ -656,7 +655,8 @@ Unshelve. all: lia. Qed. -Lemma Z_n_swap_absorbtion_right_base : forall n m α, Z n m α ⟷ n_swap m ∝ Z n m α. +Lemma Z_n_swap_absorbtion_right_base : forall n m α, + Z n m α ⟷ n_swap m ∝= Z n m α. Proof. intros n m. generalize dependent n. @@ -674,7 +674,7 @@ Proof. rewrite <- (stack_compose_distr (Z 1 1 0) —). rewrite <- compose_assoc. rewrite (Z_self_bottom_to_top_absorbtion_right_base). - rewrite <- (@cast_Z 1 _ (1 + m) (S m)). + erewrite <- (@cast_Z 1 _ (1 + m) (S m)). rewrite Z_add_r_base_rot. simpl_casts. rewrite compose_assoc. @@ -688,7 +688,8 @@ Unshelve. all: lia. Qed. -Lemma Z_n_wrap_under_r_base_unswapped : forall n m α, Z (n + m) 0 α ∝ (Z n m α ↕ n_wire m) ⟷ n_cup_unswapped m. +Lemma Z_n_wrap_under_r_base_unswapped : forall n m α, + Z (n + m) 0 α ∝= (Z n m α ↕ n_wire m) ⟷ n_cup_unswapped m. Proof. intros. generalize dependent n. @@ -696,14 +697,14 @@ Proof. induction m; intros; [simpl; cleanup_zx; simpl_casts; subst; easy | ]. remember (Z (n + (S m)) _ _) as LHS. rewrite n_cup_unswapped_grow_l. - rewrite <- (@cast_Z n _ (m + 1)). + erewrite <- (@cast_Z n _ (m + 1)). rewrite Z_add_r_base_rot. simpl_casts. rewrite <- compose_assoc. simpl. rewrite cast_compose_r. simpl_casts. - rewrite (cast_compose_l _ _ (Z n 2 α ⟷ (Z 1 m 0 ↕ Z 1 1 0) ↕ n_wire S m)). + rewrite (cast_compose_l _ _ (Z n 2 α ⟷ (Z 1 m 0 ↕ Z 1 1 0) ↕ n_wire (S m))). simpl_casts. rewrite stack_assoc. rewrite stack_nwire_distribute_r. @@ -724,13 +725,13 @@ Proof. cleanup_zx. rewrite cast_compose_r. simpl_casts. - simpl. + cbn. rewrite (stack_assoc_back _ —). rewrite (stack_assoc_back _ ⊃ (n_wire m)). - rewrite <- cast_compose_mid_contract. + erewrite <- cast_compose_mid_contract. rewrite <- stack_nwire_distribute_r. rewrite <- (nwire_stack_compose_botleft (Z 1 m 0) ⊃). - simpl. + cbn. cleanup_zx; simpl_casts. rewrite <- compose_assoc. rewrite stack_assoc_back. @@ -744,12 +745,12 @@ Proof. erewrite (cast_compose_partial_contract_r _ _ _ m _ _ _ _ _ _ _ (n_wire m ↕ ⊃)). rewrite <- (@Z_wrap_under_bot_right n m α). simpl_casts. - eapply (cast_diagrams (n + 1 + m) 0). + eapply (cast_diagrams_eq (n + 1 + m) 0). erewrite <- (@cast_Z (n + 1) _ (m) (m + 0)). rewrite cast_stack_l. - rewrite (cast_compose_mid (m + m)). + erewrite (cast_compose_mid (m + m)). rewrite 2 cast_contract. - rewrite <- cast_compose_mid_contract. + erewrite <- cast_compose_mid_contract. rewrite <- IHm. rewrite HeqLHS. simpl_casts. @@ -758,7 +759,8 @@ Unshelve. all: lia. Qed. -Lemma Z_n_wrap_under_r_base : forall n m α, Z (n + m) 0 α ∝ (Z n m α ↕ n_wire m) ⟷ n_cup m. +Lemma Z_n_wrap_under_r_base : forall n m α, + Z (n + m) 0 α ∝= (Z n m α ↕ n_wire m) ⟷ n_cup m. Proof. intros. unfold n_cup. @@ -769,7 +771,8 @@ Proof. easy. Qed. -Lemma Z_n_wrap_over_r_base_unswapped : forall n m α, Z (m + n) 0 α ∝ (n_wire m ↕ Z n m α) ⟷ n_cup_unswapped m. +Lemma Z_n_wrap_over_r_base_unswapped : forall n m α, + Z (m + n) 0 α ∝= (n_wire m ↕ Z n m α) ⟷ n_cup_unswapped m. Proof. intros. generalize dependent n. @@ -777,7 +780,7 @@ Proof. induction m; intros; [simpl; cleanup_zx; simpl_casts; subst; easy | ]. remember (Z (S m + n) 0 α) as LHS. rewrite n_cup_unswapped_grow_l. - rewrite <- (@cast_Z n _ (1 + m)). + erewrite <- (@cast_Z n _ (1 + m)). rewrite Z_add_r_base_rot. simpl_casts. rewrite stack_nwire_distribute_l. (* TODO: rename *) @@ -792,7 +795,7 @@ Proof. rewrite stack_assoc_back. simpl_casts. rewrite <- (stack_compose_distr (— ↕ (Z 1 1 0)) ⊃ (Z 1 m 0)). - rewrite (stack_empty_r_rev ⊃). + rewrite (stack_empty_r_back ⊃). simpl_casts. replace ⦰ with (n_wire 0) by easy. rewrite <- (Z_wrap_over_top_left 1 0). @@ -805,7 +808,7 @@ Proof. erewrite (cast_compose_mid (m + 3) _ _ (cast _ _ _ _ _) (cast _ _ _ _ (n_wire m ↕ (⊃ ↕ Z 1 m 0)))). rewrite cast_contract. rewrite cast_contract. - rewrite <- cast_compose_mid_contract. + erewrite <- cast_compose_mid_contract. rewrite <- stack_compose_distr. cleanup_zx. rewrite <- (nwire_stack_compose_botleft ⊃ (Z 1 m 0)). @@ -814,7 +817,7 @@ Proof. simpl. cleanup_zx. rewrite Z_spider_1_1_fusion. - eapply (cast_diagrams (m + (S n)) 0). + eapply (cast_diagrams_eq (m + (S n)) 0). rewrite cast_compose_l. simpl_casts. rewrite <- IHm. @@ -826,7 +829,8 @@ Unshelve. all: lia. Qed. -Lemma Z_n_wrap_over_r_base : forall n m α, Z (m + n) 0 α ∝ (n_wire m ↕ Z n m α) ⟷ n_cup m. +Lemma Z_n_wrap_over_r_base : forall n m α, + Z (m + n) 0 α ∝= (n_wire m ↕ Z n m α) ⟷ n_cup m. Proof. intros. rewrite n_cup_inv_n_swap_n_wire. @@ -837,25 +841,29 @@ Proof. easy. Qed. -Lemma Z_n_wrap_over_l_base_unswapped : forall n m α, Z 0 (n + m) α ∝ n_cap_unswapped n ⟷ (n_wire n ↕ Z n m α). +Lemma Z_n_wrap_over_l_base_unswapped : forall n m α, + Z 0 (n + m) α ∝= n_cap_unswapped n ⟷ (n_wire n ↕ Z n m α). Proof. transpose_of Z_n_wrap_over_r_base_unswapped. Qed. -Lemma Z_n_wrap_over_l_base : forall n m α, Z 0 (n + m) α ∝ n_cap n ⟷ (n_wire n ↕ Z n m α). +Lemma Z_n_wrap_over_l_base : forall n m α, + Z 0 (n + m) α ∝= n_cap n ⟷ (n_wire n ↕ Z n m α). Proof. transpose_of Z_n_wrap_over_r_base. Qed. -Lemma Z_n_wrap_under_l_base_unswapped : forall n m α, Z 0 (m + n) α ∝ n_cap_unswapped n ⟷ (Z n m α ↕ n_wire n). +Lemma Z_n_wrap_under_l_base_unswapped : forall n m α, + Z 0 (m + n) α ∝= n_cap_unswapped n ⟷ (Z n m α ↕ n_wire n). Proof. transpose_of Z_n_wrap_under_r_base_unswapped. Qed. -Lemma Z_n_wrap_under_l_base : forall n m α, Z 0 (m + n) α ∝ n_cap n ⟷ (Z n m α ↕ n_wire n). +Lemma Z_n_wrap_under_l_base : forall n m α, + Z 0 (m + n) α ∝= n_cap n ⟷ (Z n m α ↕ n_wire n). Proof. transpose_of Z_n_wrap_under_r_base. Qed. (* @nocheck name *) (* PI is captialized in Coq R *) -Lemma Z_2_PI : forall n m a, Z n m (INR a * 2 * PI) ∝ Z n m 0. +Lemma Z_2_PI : forall n m a, + Z n m (INR a * 2 * PI) ∝= Z n m 0. Proof. intros. - prop_exists_nonzero 1. - Msimpl. + prep_matrix_equivalence. simpl. unfold Z_semantics. rewrite Cexp_2_PI. diff --git a/src/CoreRules/ZXRules.v b/src/CoreRules/ZXRules.v index f1afa10..236cbcd 100644 --- a/src/CoreRules/ZXRules.v +++ b/src/CoreRules/ZXRules.v @@ -7,46 +7,57 @@ Require Export CoreRules.ZRules. Require Export CoreRules.XRules. - Theorem X_state_copy : forall (r n : nat) prfn prfm, - (X 0 1 ((INR r) * PI) ⟷ Z 1 n 0) ∝ + (X 0 1 ((INR r) * PI) ⟷ Z 1 n 0) + ∝[(√2 * (/√2 ^ n))%R] cast 0%nat n prfn prfm (n ⇑ (X 0 1 ((INR r) * PI))). Proof. intros. - assert (X_state_copy_ind : (X 0 1 (INR r * PI) ⟷ Z 1 2 0) ∝ + assert (X_state_copy_ind : (X 0 1 (INR r * PI) ⟷ Z 1 2 0) ∝[/(√2)%R] X 0 1 (INR r * PI) ↕ X 0 1 (INR r * PI)). { - prop_exists_nonzero (/ (√ 2)%R); Msimpl; simpl. - unfold X_semantics; unfold Z_semantics. - simpl. solve_matrix. - all: autorewrite with Cexp_db. - all: destruct (INR_pi_exp r); rewrite H. - all: try lca; C_field_simplify; try lca. - all: nonzero. + zxsymmetry. + split; [|C_field]. + symmetry. + (* rewrite Mscale_inv by nonzero. *) + prep_matrix_equivalence. + Msimpl; simpl. + unfold X_semantics, Z_semantics. + rewrite Cexp_0. + destruct (INR_pi_exp r); rewrite H; + cbv delta [kron_n kron hadamard Mmult scale I]; + by_cell; simpl; C_field; lca. } induction n; [| destruct n]. - - simpl. + - simpl. (* n = 0 --> √2 *) simpl_casts. - prop_exists_nonzero (√ 2)%R; Msimpl; simpl. - unfold X_semantics; unfold Z_semantics. + split; [|nonzero]. + prep_matrix_equivalence. + by_cell. + unfold X_semantics, Z_semantics, Mmult, + kron_n, kron, hadamard, I, scale; simpl. - solve_matrix. - destruct (INR_pi_exp r); rewrite H. - all: autorewrite with Cexp_db. - all: C_field_simplify; try lca; try nonzero. - - simpl. + Csimpl. + rewrite Rinv_1, Rmult_1_r. + C_field. + destruct (INR_pi_exp r); rewrite H; + autorewrite with Cexp_db; lca. + - simpl. (* n = 1 --> 1 *) rewrite Z_0_is_wire. simpl_casts. rewrite stack_empty_r. simpl_casts. cleanup_zx. - easy. - - eapply (cast_diagrams (S (S n) * 0) (S (S n) * 1)). + zxrefl. + rewrite Rmult_1_r. + rewrite Rinv_r by nonzero. + reflexivity. + - eapply (cast_diagrams_by (S (S n) * 0) (S (S n) * 1)). rewrite cast_contract. rewrite cast_compose_distribute. simpl_casts. simpl. - eapply (@cast_simplify 0 (S n * 0)%nat (S n) (S n * 1)%nat) in IHn. + eapply (@cast_simplify_by 0 (S n * 0)%nat (S n) (S n * 1)%nat) in IHn. rewrite cast_compose_distribute in IHn. rewrite cast_Z in IHn. rewrite cast_X in IHn. @@ -55,116 +66,106 @@ Proof. rewrite cast_id in IHn. rewrite grow_Z_top_right. rewrite <- compose_assoc. - rewrite IHn. + zxrewrite IHn. rewrite <- (stack_compose_distr (X 0 1 (INR r * PI)) (Z 1 2 0) (n ⇑ X 0 1 (INR r * PI)) (n_wire (n * 1))). - rewrite X_state_copy_ind. + zxrewrite X_state_copy_ind. cleanup_zx. rewrite (stack_assoc (X 0 1 (INR r * PI)) (X 0 1 (INR r * PI))). simpl_casts. - easy. + zxrefl. + autorewrite with RtoC_db. + C_field. Unshelve. all: lia. Qed. Theorem Z_state_copy : forall (r n : nat) prfn prfm, - (Z 0 1 ((INR r) * PI) ⟷ X 1 n 0) ∝ + (Z 0 1 ((INR r) * PI) ⟷ X 1 n 0) + ∝[(√2 * (/√2 ^ n))%R] cast 0%nat n prfn prfm (n ⇑ (Z 0 1 ((INR r) * PI))). Proof. - intros. - eapply (cast_diagrams (n * 0) (n * 1)). - rewrite cast_compose_distribute. - simpl_casts. - apply colorswap_diagrams. - autorewrite with colorswap_db. - simpl. - destruct n. - - simpl. - simpl_casts. - rewrite X_state_copy. - simpl. - simpl_casts. - easy. - - eapply (cast_diagrams (0) (S n)). - rewrite cast_compose_distribute. - simpl_casts. - apply X_state_copy. - Unshelve. - all: lia. + intros r n prfn prfm. + colorswap_of (X_state_copy r n prfn prfm). Qed. Theorem X_state_pi_copy : forall n prfn prfm, - ((X 0 1 PI) ⟷ Z 1 n 0) ∝ + ((X 0 1 PI) ⟷ Z 1 n 0) ∝[(√2 * (/√2 ^ n))%R] (cast 0 n prfn prfm (n ⇑ (X 0 1 PI))). Proof. intros. replace (PI)%R with (1 * PI)%R by lra. replace (1)%R with (INR 1)%R by reflexivity. - rewrite X_state_copy. - easy. + zxrewrite X_state_copy. + zxrefl. Qed. Theorem X_state_0_copy : forall n prfn prfm, - ((X 0 1 0) ⟷ Z 1 n 0) ∝ + ((X 0 1 0) ⟷ Z 1 n 0) ∝[(√2 * (/√2 ^ n))%R] (cast 0 n prfn prfm (n ⇑ (X 0 1 0))). Proof. intros. replace (0)%R with (0 * PI)%R at 1 by lra. replace (0)%R with (INR 0)%R by reflexivity. - rewrite X_state_copy. - replace (0 * PI)%R with (0)%R at 1 by lra. - easy. + zxrewrite X_state_copy. + rewrite Rmult_0_l. + zxrefl. Qed. Theorem Z_state_pi_copy : forall n prfn prfm, - ((Z 0 1 PI) ⟷ X 1 n 0) ∝ + ((Z 0 1 PI) ⟷ X 1 n 0) ∝[(√2 * (/√2 ^ n))%R] (cast 0 n prfn prfm (n ⇑ (Z 0 1 PI))). Proof. intros. replace (PI)%R with (1 * PI)%R by lra. replace (1)%R with (INR 1)%R by reflexivity. - rewrite Z_state_copy. - easy. + zxrewrite Z_state_copy. + zxrefl. Qed. Theorem Z_state_0_copy : forall n prfn prfm, - ((Z 0 1 0) ⟷ X 1 n 0) ∝ + ((Z 0 1 0) ⟷ X 1 n 0) ∝[(√2 * (/√2 ^ n))%R] (cast 0 n prfn prfm (n ⇑ (Z 0 1 0))). Proof. intros. replace (0)%R with (0 * PI)%R at 1 by lra. replace (0)%R with (INR 0)%R by reflexivity. - rewrite Z_state_copy. - replace (0 * PI)%R with (0)%R at 1 by lra. - easy. + zxrewrite Z_state_copy. + rewrite Rmult_0_l. + zxrefl. Qed. Lemma Z_copy : forall n r prfn prfm, - (Z 1 1 (INR r * PI) ⟷ X 1 n 0) ∝ + (Z 1 1 (INR r * PI) ⟷ X 1 n 0) ∝= X 1 n 0 ⟷ (cast n n prfn prfm (n ⇑ (Z 1 1 (INR r * PI)))). Proof. intros. - assert (Z_copy_ind : (Z 1 1 (INR r * PI) ⟷ X 1 2 0) ∝ + assert (Z_copy_ind : (Z 1 1 (INR r * PI) ⟷ X 1 2 0) ∝= X 1 2 0 ⟷ (Z 1 1 (INR r * PI) ↕ Z 1 1 (INR r * PI))). { - prop_exists_nonzero (1); Msimpl; simpl. - unfold X_semantics; unfold Z_semantics. - simpl. solve_matrix. - all: autorewrite with Cexp_db. - all: destruct (INR_pi_exp r); rewrite H. - all: try lca; C_field_simplify; try lca. - all: nonzero. + prep_matrix_equivalence. + Msimpl; simpl. + unfold X_semantics, Z_semantics. + rewrite Cexp_0. + destruct (INR_pi_exp r); rewrite H; + cbv delta [kron_n kron hadamard Mmult scale I]; + by_cell; simpl; C_field; lca. } - eapply (cast_diagrams 1 (n * 1)). + eapply (cast_diagrams_eq 1 (n * 1)). rewrite 2 cast_compose_distribute. simpl_casts. erewrite (@cast_compose_mid _ _ _ (n * 1)%nat _ _ (X 1 n 0)). simpl_casts. induction n; [ | destruct n]. - simpl. - solve_prop 1. + prep_matrix_equivalence. + simpl. + unfold X_semantics, Z_semantics; + rewrite Cexp_0; + cbv [kron_n kron hadamard Mmult scale I]; + by_cell; simpl; C_field; lca. - simpl. repeat rewrite X_0_is_wire. cleanup_zx. @@ -192,23 +193,18 @@ Proof. Qed. Lemma X_copy : forall n r prfn prfm, - (X 1 1 (INR r * PI) ⟷ Z 1 n 0) ∝ + (X 1 1 (INR r * PI) ⟷ Z 1 n 0) ∝= Z 1 n 0 ⟷ (cast n n prfn prfm (n ⇑ (X 1 1 (INR r * PI)))). Proof. - intros. - apply colorswap_diagrams. - simpl. - rewrite cast_colorswap. - rewrite n_stack_colorswap. - simpl. - apply Z_copy. + intros n r prfn prfm. + colorswap_of (Z_copy n r prfn prfm). Qed. Lemma Z_0_copy : forall n prfn prfm, - (Z 1 1 0 ⟷ X 1 n 0) ∝ + (Z 1 1 0 ⟷ X 1 n 0) ∝= X 1 n 0 ⟷ (cast n n prfn prfm (n ⇑ (Z 1 1 0))). @@ -222,7 +218,7 @@ Proof. Qed. Lemma Z_pi_copy : forall n prfn prfm, - (Z 1 1 PI ⟷ X 1 n 0) ∝ + (Z 1 1 PI ⟷ X 1 n 0) ∝= X 1 n 0 ⟷ (cast n n prfn prfm (n ⇑ (Z 1 1 PI))). @@ -236,7 +232,7 @@ Proof. Qed. Lemma X_0_copy : forall n prfn prfm, - (X 1 1 0 ⟷ Z 1 n 0) ∝ + (X 1 1 0 ⟷ Z 1 n 0) ∝= Z 1 n 0 ⟷ (cast n n prfn prfm (n ⇑ (X 1 1 0))). @@ -250,7 +246,7 @@ Proof. Qed. Lemma X_pi_copy : forall n prfn prfm, - (X 1 1 PI ⟷ Z 1 n 0) ∝ + (X 1 1 PI ⟷ Z 1 n 0) ∝= Z 1 n 0 ⟷ (cast n n prfn prfm (n ⇑ (X 1 1 PI))). diff --git a/src/DiagramRules/Bell.v b/src/DiagramRules/Bell.v index f65d316..14bfee6 100644 --- a/src/DiagramRules/Bell.v +++ b/src/DiagramRules/Bell.v @@ -5,11 +5,11 @@ Definition bell_state_prep := (((X 0 1 0) ↕ (X 0 1 0)) ⟷ (□ ↕ —) ⟷ ((Z 1 2 0 ↕ —) ⟷ (— ↕ X 2 1 0))). -Lemma bell_state_prep_correct : bell_state_prep ∝ ⊂. +Lemma bell_state_prep_correct : bell_state_prep ∝= ⊂. Proof. unfold bell_state_prep. rewrite <- stack_compose_distr. - assert (X 0 1 0 ⟷ □ ∝ Z 0 1 0) as H. + assert (X 0 1 0 ⟷ □ ∝= Z 0 1 0) as H. { replace (X 0 1 0) with (⊙ (Z 0 1 0)) at 1 by easy. rewrite colorswap_is_bihadamard; simpl; cleanup_zx; simpl_casts. @@ -21,7 +21,7 @@ Proof. rewrite Z_spider_1_1_fusion. rewrite <- nwire_stack_compose_botleft. rewrite compose_assoc. - rewrite <- (n_wire_stack 1 1); rewrite wire_to_n_wire at 4. + rewrite <- (n_wire_stack 1 1); rewrite wire_to_n_wire. rewrite (stack_assoc (n_wire 1) (n_wire 1)); simpl_casts. rewrite <- (stack_compose_distr (n_wire 1) (n_wire 1) (n_wire 1 ↕ X 0 1 0)). rewrite (dominated_X_spider_fusion_bot_right 0 0 1). @@ -31,16 +31,16 @@ Proof. rewrite <- cap_Z. easy. Unshelve. -all: lia. +all: reflexivity. Qed. Definition teleportation (a b : nat) := (⊂ ↕ Z 1 2 0) ⟷ ((X 1 1 (INR b * PI) ⟷ Z 1 1 (INR a * PI)) ↕ (((X 2 1 0) ↕ (Z 1 0 (INR a * PI)) ⟷ (□ ⟷ Z 1 0 (INR b * PI))))). -Lemma teleportation_correct : forall a b, teleportation a b ∝ —. +Lemma teleportation_correct : forall a b, teleportation a b ∝= —. Proof. intros; unfold teleportation. - assert (□ ⟷ Z 1 0 (INR b * PI) ∝ (X 1 0 (INR b * PI))). + assert (□ ⟷ Z 1 0 (INR b * PI) ∝= (X 1 0 (INR b * PI))). { replace (X 1 0 (INR b * PI)) with (⊙ (Z 1 0 (INR b * PI))) by easy. rewrite colorswap_is_bihadamard. @@ -48,7 +48,7 @@ Proof. easy. } rewrite H. - rewrite (stack_empty_r_rev (X 1 0 _)). + rewrite (stack_empty_r_back (X 1 0 _)). simpl_casts. rewrite <- (stack_compose_distr (X 2 1 0) (X 1 0 _) (Z 1 0 _) ⦰). rewrite X_spider_1_1_fusion. @@ -56,7 +56,7 @@ Proof. rewrite (stack_assoc_back (X 1 1 _ ⟷ Z 1 1 _) (X 2 0 _) (Z 1 0 _)). simpl_casts. rewrite <- (nwire_removal_l (X 2 0 _)). - simpl; rewrite stack_empty_r; simpl_casts. + cbn; rewrite stack_empty_r; simpl_casts. rewrite stack_compose_distr. rewrite (stack_assoc_back (X 1 1 _) — —). simpl_casts. diff --git a/src/DiagramRules/Bialgebra.v b/src/DiagramRules/Bialgebra.v index f282b22..b87e09e 100644 --- a/src/DiagramRules/Bialgebra.v +++ b/src/DiagramRules/Bialgebra.v @@ -5,10 +5,10 @@ Definition bi_alg_Z_X := ((Z_Spider 1 2 0) ↕ (Z_Spider 1 2 0) ⟷ (— ↕ ⨉ Definition bi_alg_X_Z := ((X_Spider 1 2 0) ↕ (X_Spider 1 2 0) ⟷ (— ↕ ⨉ ↕ —) ⟷ ((Z_Spider 2 1 0) ↕ (Z_Spider 2 1 0))). Theorem bi_algebra_rule_Z_X : - (X_Spider 2 1 0) ⟷ (Z_Spider 1 2 0) ∝ bi_alg_Z_X. + (X_Spider 2 1 0) ⟷ (Z_Spider 1 2 0) ∝[(√2)%R] bi_alg_Z_X. Proof. - prop_exists_nonzero 1. - simpl. + Admitted. + (* simpl. rewrite X_semantics_equiv, Z_semantics_equiv. unfold_dirac_spider. autorewrite with Cexp_db. @@ -56,22 +56,22 @@ Proof. restore_dims. repeat rewrite (kron_mixed_product (xbasis_plus × (_ ⊗ _)) (xbasis_plus × (_ ⊗ _)) ((ket _ ⊗ ket _) × bra _) ((ket _ ⊗ ket _) × bra _)). repeat rewrite (kron_mixed_product (xbasis_minus × (_ ⊗ _)) (xbasis_minus × (_ ⊗ _)) ((ket _ ⊗ ket _) × bra _) ((ket _ ⊗ ket _) × bra _)). - repeat rewrite Mmult_assoc. -Admitted. + repeat rewrite Mmult_assoc. *) + Theorem bi_algebra_rule_X_Z : - (Z_Spider 2 1 0) ⟷ (X_Spider 1 2 0) ∝ bi_alg_X_Z. + (Z_Spider 2 1 0) ⟷ (X_Spider 1 2 0) ∝[(√2)%R] bi_alg_X_Z. Proof. colorswap_of bi_algebra_rule_Z_X. Qed. Theorem hopf_rule_Z_X : - (Z_Spider 1 2 0) ⟷ (X_Spider 2 1 0) ∝ (Z_Spider 1 0 0) ⟷ (X_Spider 0 1 0). + (Z_Spider 1 2 0) ⟷ (X_Spider 2 1 0) ∝[/C2] (Z_Spider 1 0 0) ⟷ (X_Spider 0 1 0). Proof. intros. rewrite <- (@nwire_removal_r 2). - simpl. + cbv delta [n_wire]; simpl. rewrite stack_empty_r. simpl_casts. rewrite wire_loop at 1. @@ -94,7 +94,7 @@ Opaque n_stack1. simpl. repeat rewrite <- compose_assoc. rewrite <- (push_out_top (Z 0 1 0)). - assert (Hl : (Z 0 1 0 ↕ Z 1 2 0) ⟷ ((Z) 1 2 0 ↕ n_wire 2) ∝ Z 0 1 0 ↕ n_wire 1 ⟷ (Z 1 2 0 ↕ Z 1 2 0)). + assert (Hl : (Z 0 1 0 ↕ Z 1 2 0) ⟷ ((Z) 1 2 0 ↕ n_wire 2) ∝= Z 0 1 0 ↕ n_wire 1 ⟷ (Z 1 2 0 ↕ Z 1 2 0)). { rewrite <- stack_compose_distr. rewrite nwire_removal_r. @@ -105,7 +105,7 @@ Opaque n_stack1. rewrite Hl. repeat rewrite compose_assoc. rewrite <- (pull_out_top (X 1 0 0)). - assert (Hr : X 2 1 0 ↕ n_wire 2 ⟷ (X 1 0 0 ↕ X 2 1 0) ∝ X 2 1 0 ↕ (X) 2 1 0 ⟷ ((X) 1 0 0 ↕ n_wire 1)). + assert (Hr : X 2 1 0 ↕ n_wire 2 ⟷ (X 1 0 0 ↕ X 2 1 0) ∝= X 2 1 0 ↕ (X) 2 1 0 ⟷ ((X) 1 0 0 ↕ n_wire 1)). { rewrite <- stack_compose_distr. rewrite nwire_removal_l. @@ -115,7 +115,7 @@ Opaque n_stack1. } rewrite Hr. repeat rewrite <- compose_assoc. - assert (HBiAlgAssoc : (Z) 0 1 0 ↕ n_wire 1 ⟷ ((Z) 1 2 0 ↕ (Z) 1 2 0) ⟷ (n_wire 1 ↕ ⨉ ↕ n_wire 1) ⟷ ((X) 2 1 0 ↕ (X) 2 1 0) ⟷ ((X) 1 0 0 ↕ n_wire 1) ∝ + assert (HBiAlgAssoc : (Z) 0 1 0 ↕ n_wire 1 ⟷ ((Z) 1 2 0 ↕ (Z) 1 2 0) ⟷ (n_wire 1 ↕ ⨉ ↕ n_wire 1) ⟷ ((X) 2 1 0 ↕ (X) 2 1 0) ⟷ ((X) 1 0 0 ↕ n_wire 1) ∝= (Z) 0 1 0 ↕ n_wire 1 ⟷ (((Z) 1 2 0 ↕ (Z) 1 2 0) ⟷ (n_wire 1 ↕ ⨉ ↕ n_wire 1) ⟷ ((X) 2 1 0 ↕ (X) 2 1 0)) ⟷ ((X) 1 0 0 ↕ n_wire 1)). { repeat rewrite compose_assoc. @@ -126,8 +126,8 @@ Opaque n_stack1. rewrite <- wire_to_n_wire. Transparent n_stack1. fold bi_alg_Z_X. - rewrite <- bi_algebra_rule_Z_X. - assert (X_Wrap_Under_L_base : forall α, X 2 1 α ∝ (X 1 2 α ↕ —) ⟷ (— ↕ ⊃)). + zxrewrite <- bi_algebra_rule_Z_X. + assert (X_Wrap_Under_L_base : forall α, X 2 1 α ∝= (X 1 2 α ↕ —) ⟷ (— ↕ ⊃)). { intros. rewrite (X_wrap_under_bot_right 1). @@ -138,14 +138,14 @@ Transparent n_stack1. rewrite X_Wrap_Under_L_base. repeat rewrite <- compose_assoc. rewrite <- stack_wire_distribute_r. - rewrite Z_state_0_copy. + zxrewrite Z_state_0_copy. simpl_casts. simpl. cleanup_zx; simpl_casts. rewrite (stack_assoc (Z 0 1 0) ((Z) (0 + 0) (1 + 0) 0) —). simpl_casts. rewrite <- (stack_compose_distr ((Z) 0 1 0) — ((Z) (0 + 0) (1 + 0) 0 ↕ —) ⊃). - assert (Hl: (Z) (0 + 0) (1 + 0) 0 ↕ — ⟷ ⊃ ∝ Z 1 0 0). (* Todo : pull out lemma *) + assert (Hl: (Z) (0 + 0) (1 + 0) 0 ↕ — ⟷ ⊃ ∝= Z 1 0 0). (* Todo : pull out lemma *) { rewrite cup_Z. rewrite <- Z_0_is_wire. @@ -155,7 +155,7 @@ Transparent n_stack1. } rewrite Hl. cleanup_zx. - rewrite (stack_empty_r_rev (Z 1 2 0)). + rewrite (stack_empty_r_back (Z 1 2 0)). simpl_casts. rewrite <- (stack_compose_distr (Z 0 1 0) (Z 1 2 0) (Z 1 0 0) ⦰). cleanup_zx. @@ -164,7 +164,7 @@ Transparent n_stack1. rewrite <- cap_Z. rewrite (disconnected_stack_compose_r). simpl_casts. - assert (Hr : ⊂ ⟷ ((X) 1 0 0 ↕ —) ∝ X 0 1 0). + assert (Hr : ⊂ ⟷ ((X) 1 0 0 ↕ —) ∝= X 0 1 0). { rewrite cap_X. rewrite <- X_0_is_wire. @@ -174,13 +174,14 @@ Transparent n_stack1. } rewrite compose_assoc. rewrite Hr. - easy. + zxrefl. + autorewrite with RtoC_db; C_field. Unshelve. all: lia. Qed. Theorem hopf_rule_X_Z : - (X_Spider 1 2 0) ⟷ (Z_Spider 2 1 0) ∝ (X_Spider 1 0 0) ⟷ (Z_Spider 0 1 0). + (X_Spider 1 2 0) ⟷ (Z_Spider 2 1 0) ∝[/ 2] (X_Spider 1 0 0) ⟷ (Z_Spider 0 1 0). Proof. colorswap_of hopf_rule_Z_X. Qed. \ No newline at end of file diff --git a/src/DiagramRules/Completeness.v b/src/DiagramRules/Completeness.v index 34341ce..0cd2889 100644 --- a/src/DiagramRules/Completeness.v +++ b/src/DiagramRules/Completeness.v @@ -5,10 +5,11 @@ Require Import CompletenessComp. (* @nocheck name *) (* Conventional name *) -Lemma completeness_SUP : forall α, ((Z 0 1 α) ↕ (Z 0 1 (α + PI))) ⟷ (X 2 1 0) ∝ Z 0 2 (2 *α + PI) ⟷ X 2 1 0. +Lemma completeness_SUP : forall α, + ((Z 0 1 α) ↕ (Z 0 1 (α + PI))) ⟷ (X 2 1 0) ∝= Z 0 2 (2 *α + PI) ⟷ X 2 1 0. Proof. intros. - prop_exists_nonzero 1; + unfold proportional_by_1. simpl; unfold X_semantics. solve_matrix. @@ -37,7 +38,7 @@ Qed. (* Conventional name *) Lemma completeness_C : forall (α β γ : R), (Z 1 2 0) ⟷ (((Z 0 1 β ↕ —) ⟷ X 2 1 PI) ↕ ((Z 0 1 α ↕ —) ⟷ X 2 1 0)) ⟷ ((Z 1 2 β ↕ Z 1 2 α) ⟷ (— ↕ X 2 1 γ ↕ —)) ⟷ (((— ↕ Z 1 2 0) ⟷ (X 2 1 (-γ) ↕ —)) ↕ —) - ∝ + ∝= (Z 1 2 0) ⟷ (((Z 0 1 α ↕ —) ⟷ X 2 1 0) ↕ ((Z 0 1 β ↕ —) ⟷ X 2 1 PI)) ⟷ ((Z 1 2 α ↕ Z 1 2 β) ⟷ (— ↕ X 2 1 (-γ) ↕ —)) ⟷ (— ↕ ((Z 1 2 0 ↕ —) ⟷ (— ↕ X 2 1 γ))). Proof. (* solve matrix takes forever *) intros. @@ -47,14 +48,14 @@ Proof. (* solve matrix takes forever *) remember (((Z 1 2 α ↕ Z 1 2 β) ⟷ (— ↕ X 2 1 (-γ) ↕ —))) as cs2n. remember ((Z 1 2 0 ↕ —) ⟷ (— ↕ X 2 1 γ)) as cs3. remember (((— ↕ Z 1 2 0) ⟷ (X 2 1 (-γ) ↕ —))) as cs3f. - prop_exists_nonzero 1. + unfold proportional_by_1. simpl. rewrite Heqcs1. rewrite Heqcs1pi. clear Heqcs1; clear Heqcs1pi; clear cs1; clear cs1pi. rewrite c_step_1, c_step_1_pi. autorewrite with scalar_move_db. - rewrite Cmult_1_l. + rewrite 1?Cmult_1_l. apply Mscale_simplify; [| C_field]. replace ((Cexp β .* ∣0⟩⟨0∣ .+ ∣0⟩⟨1∣ .+ ∣1⟩⟨0∣ .+ Cexp β .* ∣1⟩⟨1∣)) with (Cexp β .* (I 2) .+ ∣0⟩⟨1∣ .+ ∣1⟩⟨0∣) by (rewrite <- Mplus01; lma). replace ((∣0⟩⟨0∣ .+ Cexp α .* ∣0⟩⟨1∣ .+ Cexp α .* ∣1⟩⟨0∣ .+ ∣1⟩⟨1∣)) with (I 2 .+ Cexp α .* (∣0⟩⟨1∣ .+ ∣1⟩⟨0∣)) by (rewrite <- Mplus01; lma). @@ -430,9 +431,9 @@ Qed. (* @nocheck name *) (* Conventional name *) Lemma completeness_BW : - ◁ ⟷ Z 1 1 PI ⟷ ▷ ∝ ▷ ⟷ X 1 1 PI. + ◁ ⟷ Z 1 1 PI ⟷ ▷ ∝= ▷ ⟷ X 1 1 PI. Proof. - prop_exists_nonzero 1. + unfold proportional_by_1. remember (Z 1 1 PI) as z. remember (X 1 1 PI) as x. simpl. @@ -467,7 +468,7 @@ Qed. (* Conventional name *) Lemma completeness_N : forall α β θ_1 θ_2 γ θ_3, 2 * Cexp (θ_3) * cos(γ) = Cexp (θ_1) * cos(α) + Cexp (θ_2) * cos(β) -> - (((Z 0 1 α ↕ Z 0 1 (-α) ⟷ X 2 1 0) ⟷ Z 1 1 θ_1) ↕ ((Z 0 1 β ↕ Z 0 1 (-β) ⟷ X 2 1 0) ⟷ Z 1 1 θ_2)) ⟷ ((— ↕ (X 0 1 (PI/2) ⟷ Z 1 2 0) ↕ —) ⟷ (X 2 1 0 ↕ X 2 1 0)) ⟷ (Z 1 1 (PI/4) ↕ Z 1 1 (PI/4)) ⟷ X 2 1 0 ∝ + (((Z 0 1 α ↕ Z 0 1 (-α) ⟷ X 2 1 0) ⟷ Z 1 1 θ_1) ↕ ((Z 0 1 β ↕ Z 0 1 (-β) ⟷ X 2 1 0) ⟷ Z 1 1 θ_2)) ⟷ ((— ↕ (X 0 1 (PI/2) ⟷ Z 1 2 0) ↕ —) ⟷ (X 2 1 0 ↕ X 2 1 0)) ⟷ (Z 1 1 (PI/4) ↕ Z 1 1 (PI/4)) ⟷ X 2 1 0 ∝= ((Z 0 1 γ ↕ Z 0 1 (-γ) ⟷ X 2 1 0) ↕ (Z 0 1 (PI/4) ↕ Z 0 1 (PI/4) ⟷ X 2 1 0)) ⟷ (Z 2 1 θ_3). Proof. intros. @@ -482,8 +483,7 @@ Proof. remember (Z 2 1 θ_3) as final_step_2. remember (Z 1 1 θ_1) as step_1_5. remember (Z 1 1 θ_2) as step_1_6. - prop_exists_nonzero 1. - Msimpl. + unfold proportional_by_1. simpl. rewrite Heqstep_1_1, Heqstep_1_2. rewrite Heqfinal_step. @@ -546,15 +546,11 @@ Proof. autorewrite with scalar_move_db. Msimpl. autorewrite with scalar_move_db. - rewrite Heqfinal_step at 1. - rewrite Heqfinal_step at 1. - rewrite Heqfinal_step at 1. - rewrite Heqfinal_step at 1. - rewrite ZX_semantic_equiv at 1. - rewrite ZX_semantic_equiv at 1. - rewrite ZX_semantic_equiv at 1. - rewrite ZX_semantic_equiv at 1. + match goal with |- _ = ?A => set (temp := A) end. + rewrite Heqfinal_step. + rewrite ZX_semantic_equiv. unfold_dirac_spider. + subst temp. rewrite Cexp_0. Msimpl. repeat rewrite Mmult_plus_distr_r. diff --git a/src/DiagramRules/Soundness.v b/src/DiagramRules/Soundness.v new file mode 100644 index 0000000..8725832 --- /dev/null +++ b/src/DiagramRules/Soundness.v @@ -0,0 +1,729 @@ +From QuantumLib Require Complex Matrix RealAux Polar. + +Module SoundnessC. + +Import Polar Modulus. + +Definition prop_lb (z : C) : nat := + (BinInt.Z.to_nat (Int_part (ln (Cmod z / 2) / ln (√2))%R%C) + 1)%nat. + +(* Decomposition assuming |z| <= 2 *) +Definition small_decomp (z : C) : R * R := + let a := acos ((Cmod z)^2 / 2 - 1) in + (a, get_arg (z / (1 + Cexp a))). + +Definition prop_decomp (z : C) : nat * (R * R) := + (prop_lb z, small_decomp (z / (√2 ^ prop_lb z))). + + +Lemma prop_step_1 (r : R) (Hr : 0 < r <= 2) : + √ (2 + 2 * cos (acos (r^2 / 2 - 1))) = r. +Proof. + assert (0 <= r ^ 2) by + (rewrite <- Rsqr_pow2, Rsqr_def; + apply Rmult_le_pos; + lra). + assert (r ^ 2 <= 2 ^ 2) by + (apply Rpow_le_compat_r; + lra). + rewrite cos_acos by lra. + apply sqrt_lem_1; [lra.. | ]. + rewrite <- Rsqr_pow2, Rsqr_def. + lra. +Qed. + +Lemma small_decomp_correct (z : C) : z <> 0 -> Cmod z <= 2 -> + (1 + Cexp (fst (small_decomp z))) * + (Cexp (snd (small_decomp z))) = + z. +Proof. + intros Hz0 Hz. + unfold small_decomp. + cbn -[pow]. + assert (Hmod : + Cmod (C1 + Cexp (acos (Cmod z ^ 2 / 2 - 1))) = Cmod z). 1:{ + rewrite Cmod_1_plus_Cexp. + assert (0 < Cmod z) by (apply Cmod_gt_0, Hz0). + rewrite prop_step_1; lra. + } + assert (C1 + Cexp (acos (Cmod z ^ 2 / 2 - 1)) <> 0) by + (rewrite <- Cmod_eq_0_iff, Hmod, Cmod_eq_0_iff; auto). + rewrite Cexp_get_arg_unit. + - C_field. + - rewrite Cmod_div by auto. + rewrite Hmod. + apply Rinv_r. + rewrite Cmod_eq_0_iff. + auto. +Qed. + +Lemma prop_lb_correct (z : C) : z <> 0 -> Cmod (z / (√2 ^ prop_lb z)) <= 2. +Proof. + intros Hz. + assert (Rlt 0 (√2 ^ prop_lb z)). 1:{ + pose proof (Rpow_pos (prop_lb z) (√2) + ltac:(pose Rlt_sqrt2_0; lra)) as H. + destruct H as [H | H]; [exact H|]. + symmetry in H. + rewrite Rpow_eq_0_iff in H. + pose proof sqrt2_neq_0. + lra. + } + assert (√ 2 ^ prop_lb z <> 0). 1:{ + rewrite RtoC_pow. + apply RtoC_neq. + lra. + } + rewrite Cmod_div by auto. + rewrite Rdiv_le_iff by (apply Cmod_gt_0; auto). + rewrite RtoC_pow. + rewrite Cmod_R. + rewrite Rabs_right by lra. + unfold prop_lb. + rewrite <- Rpower_pow by exact Rlt_sqrt2_0. + rewrite <- Rdiv_le_iff by apply exp_pos. + apply div_Rpower_le_of_le. + - apply Cmod_gt_0; auto. + - rewrite <- sqrt_1. + apply sqrt_lt_1; lra. + - rewrite plus_INR. + simpl. + enough (0 <= INR (Z.to_nat (Int_part (ln (Cmod z / 2) / ln (√ 2))))) by lra. + apply pos_INR. + - lra. + - rewrite plus_INR. + apply Rle_trans with (IZR (1 + (Int_part (ln (Cmod z / 2) / ln (√ 2))))); + [apply Rlt_le, lt_S_Int_part|]. + rewrite Z.add_comm. + rewrite plus_IZR. + simpl. + apply Rplus_le_compat_r. + generalize (Int_part (ln (Cmod z / 2) / ln (√2))). + intros w. + case w. + + simpl; lra. + + intros p. + rewrite pos_IZR. + simpl. + lra. + + intros p. + simpl. + rewrite IZR_NEG, pos_IZR. + pose proof (INR_pos p). + lra. +Qed. + +Lemma prop_equation (z : C) : z <> 0 -> + z = (√2 ^ fst (prop_decomp z)) * + (1 + Cexp (fst (snd (prop_decomp z)))) * + (Cexp (snd (snd (prop_decomp z)))). +Proof. + intros Hz. + assert (Rlt 0 (√2 ^ prop_lb z)). 1:{ + pose proof (Rpow_pos (prop_lb z) (√2) + ltac:(pose Rlt_sqrt2_0; lra)) as H. + destruct H as [H | H]; [exact H|]. + symmetry in H. + rewrite Rpow_eq_0_iff in H. + pose proof sqrt2_neq_0. + lra. + } + assert (√ 2 ^ prop_lb z <> 0). 1:{ + rewrite RtoC_pow. + apply RtoC_neq. + lra. + } + unfold prop_decomp. + cbn [fst snd]. + rewrite <- Cmult_assoc. + rewrite small_decomp_correct. + - C_field. + - apply Cdiv_nonzero; auto. + - apply prop_lb_correct, Hz. +Qed. + +Lemma fst_small_decomp_0 : fst (small_decomp 0) = PI. +Proof. + unfold small_decomp. + rewrite Cmod_0. + simpl. + rewrite Rmult_0_l, Rdiv_0_l, Rminus_0_l, acos_opp, acos_1. + lra. +Qed. + +Lemma prop_equation' (z : C) : + z = (√2 ^ fst (prop_decomp z)) * + (1 + Cexp (fst (snd (prop_decomp z)))) * + (Cexp (snd (snd (prop_decomp z)))). +Proof. + destruct (Ceq_dec z 0) as [H0 | Hnz]. + - unfold prop_decomp. + cbn [fst snd]. + rewrite H0. + unfold Cdiv. + rewrite Cmult_0_l, fst_small_decomp_0. + rewrite Cexp_PI. + lca. + - apply prop_equation, Hnz. +Qed. + + + + + + + + + + +End SoundnessC. + +Import SoundnessC. + + +From VyZX Require Import ZXCore Proportional. + + + +Lemma X_0_0_semantics (r : R) : + ⟦ X 0 0 r ⟧ = (1 + Cexp r) .* I 1. +Proof. + lma'. +Qed. + +Lemma Z_0_0_semantics (r : R) : + ⟦ Z 0 0 r ⟧ = (1 + Cexp r) .* I 1. +Proof. + lma'. +Qed. + +Lemma Z_semantics_0_0 (r : R) : + Z_semantics 0 0 r = (1 + Cexp r) .* I 1. +Proof. + exact (Z_0_0_semantics r). +Qed. + +Definition zx_sqrt2 : ZX 0 0 := + Z 0 1 0 ⟷ X 1 0 PI. + +Local Open Scope R_scope. + +Lemma zx_sqrt2_semantics : + ⟦ zx_sqrt2 ⟧ = (√2)%R .* I 1. +Proof. + match goal with |- ?A = _ => compute_matrix A end. + prep_matrix_equivalence. + rewrite make_WF_equiv. + by_cell. + autounfold with U_db. + cbn [list2D_to_matrix nth]. + cbn. + rewrite Cexp_0, Cexp_PI. + C_field. + lca. +Qed. + +Definition zx_invsqrt2 : ZX 0 0 := + X 0 3 0 ⟷ Z 3 0 0. + +Lemma zx_invsqrt2_semantics : + ⟦ zx_invsqrt2 ⟧ = / sqrt 2 .* I 1. +Proof. + cbn. + compute_matrix (Z_semantics 3 0 0). + rewrite Cexp_0. + prep_matrix_equivalence. + by_cell. + cbn -[X_semantics]. + Csimpl. + cbn. + rewrite Cexp_0. + Csimpl. + autounfold with U_db; cbn. + C_field. + lca. +Qed. + +Definition zx_cexp (r : R) : ZX 0 0 := + X 0 1 r ⟷ Z 1 0 PI ⟷ zx_invsqrt2. + +Lemma zx_cexp_semantics (r : R) : + ⟦ zx_cexp r ⟧ = Cexp r .* I 1. +Proof. + unfold zx_cexp. + set (T := X 0 1 r ⟷ Z 1 0 PI). + cbn -[zx_invsqrt2 T]. + rewrite zx_invsqrt2_semantics. + rewrite Mscale_mult_dist_l, Mmult_1_l by (restore_dims; auto_wf). + + match goal with |- ?A = _ => compute_matrix A end. + prep_matrix_equivalence. + autounfold with U_db; by_cell_no_intros; cbn. + rewrite Cexp_PI. + C_field. + lca. +Qed. + + +Fixpoint zx_nsqrt2 (n : nat) : ZX 0 0 := + match n with + | 0 => Empty + | S n' => zx_sqrt2 ⟷ zx_nsqrt2 n' + end. + +Lemma zx_nsqrt2_semantics n : + ⟦ zx_nsqrt2 n ⟧ = sqrt 2 ^ n .* I 1. +Proof. + induction n. + - lma'. + - cbn [zx_nsqrt2 ZX_semantics]. + rewrite zx_sqrt2_semantics. + rewrite IHn. + rewrite Mscale_mult_dist_l, Mscale_mult_dist_r, Mscale_assoc. + Msimpl. + rewrite Cmult_comm. + reflexivity. +Qed. + +Definition zx_of_const (z : C) : ZX 0 0 := + zx_nsqrt2 (fst (prop_decomp z)) ⟷ + Z 0 0 (fst (snd (prop_decomp z))) ⟷ + zx_cexp (snd (snd (prop_decomp z))). + + +Lemma zx_of_const_semantics c : + ⟦zx_of_const c⟧ = c .* I 1. +Proof. + unfold zx_of_const. + cbn [ZX_semantics]. + rewrite zx_cexp_semantics, Z_semantics_0_0, zx_nsqrt2_semantics. + repeat rewrite Mscale_mult_dist_l, Mmult_1_l by auto_wf. + rewrite 2!Mscale_assoc. + f_equal. + rewrite Cmult_comm, (Cmult_comm (Cexp _)), Cmult_assoc. + rewrite <- prop_equation'. + reflexivity. +Qed. + +Local Open Scope ZX_scope. + +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. + exists (zx_of_const c). + rewrite zx_of_const_semantics. + rewrite Mscale_kron_dist_l, kron_1_l by auto_wf. + reflexivity. +Qed. + + + + +Module ConcreteProp. + + +Import Matrix Setoid Complex. + +Fixpoint last_nonzero (f : nat -> C) (n : nat) : nat := + match n with + | 0 => 0 + | S n' => if Ceq_dec (f n') 0 then last_nonzero f n' else n' + end. + +Definition last_nonzero_val (f : nat -> C) (n : nat) : C := + f (last_nonzero f n). + + +Lemma last_nonzero_correct f n (Hn : exists (m : nat), (m < n)%nat /\ f m <> C0) : + f (last_nonzero f n) <> C0 /\ + forall m, (last_nonzero f n < m < n)%nat -> f m = 0. +Proof. + induction n; [destruct Hn as (?&?&?); easy|]. + simpl. + destruct (Ceq_dec (f n) C0) as [H0 | Hn0]. + - destruct Hn as (m & Hm & Hfm). + assert (m <> n) by (intros ->; easy). + specialize (IHn (ltac:(exists m; split;auto with zarith))) as [Hl Hr]. + split; [apply Hl|]. + intros m' [Hlast Hlt]. + bdestruct (m' =? n). + + subst; easy. + + apply Hr; lia. + - split; [auto|]. + lia. +Qed. + +Local Open Scope nat_scope. + +Lemma last_nonzero_small f n (Hn : n <> O) : + last_nonzero f n < n. +Proof. + enough (forall m, m <= n -> last_nonzero f m < n) by auto. + intros m Hm. + induction m; [simpl; lia|]. + simpl. + destruct (Ceq_dec (f m) C0); lia. +Qed. + +Lemma last_nonzero_small_or_eq f n : + {last_nonzero f n < n} + {last_nonzero f n = 0}. +Proof. + enough (forall m, m <= n -> + {last_nonzero f m < n} + {last_nonzero f m = 0}) by auto. + intros m Hm. + induction m; [simpl; right; reflexivity|]. + simpl. + destruct (Ceq_dec (f m) C0); [|left; lia]. + apply IHm; lia. +Qed. + + +Lemma last_nonzero_spec f n : + {last_nonzero f n < n /\ f (last_nonzero f n) <> C0} + + {last_nonzero f n = 0 /\ forall k, k < n -> f k = C0}. +Proof. + enough (forall m, m <= n -> + {last_nonzero f m < n /\ f (last_nonzero f m) <> C0} + + {last_nonzero f m = 0 /\ forall k, k < m -> f k = C0}) by auto. + intros m Hm. + induction m; [simpl; right; split; intros; lia|]. + simpl. + destruct (Ceq_dec (f m) C0). + - specialize (IHm ltac:(lia)). + destruct IHm as [Hl | [Hlv0 Hall]]; [left; auto|]. + right; split; [auto|]. + intros k Hk. + bdestruct (k =? m). + + subst; auto. + + apply Hall; lia. + - left; split; [lia | auto]. +Qed. + +Definition mat_last_nonzero {n m} (A : Matrix n m) : nat := + last_nonzero (fun i => A (i mod n) (i / n))%nat (n * m)%nat. + +Definition mat_last_nonzero_val {n m} (A : Matrix n m) : C := + last_nonzero_val (fun i => A (i mod n) (i / n))%nat (n * m)%nat. + +Lemma last_nonzero_eq_of_zero_iff (f g : nat -> C) n + (Hfg : forall k, (k < n)%nat -> f k = C0 <-> g k = C0) : + last_nonzero f n = last_nonzero g n. +Proof. + induction n; [reflexivity|]. + simpl. + specialize (IHn (fun k Hk => ltac:(auto))). + rewrite IHn. + destruct (Ceq_dec (f n) C0) as [Hf | Hf], (Ceq_dec (g n) C0); + rewrite Hfg in Hf by auto; easy. +Qed. + +Open Scope matrix_scope. + +Lemma mat_last_nonzero_eq_of_prop {n m} (A B : Matrix n m) + c (Hc : c <> C0) : + A ≡ c .* B -> + mat_last_nonzero A = mat_last_nonzero B. +Proof. + intros HAB. + unfold mat_last_nonzero. + apply last_nonzero_eq_of_zero_iff. + intros k Hk. + rewrite HAB by Modulus.show_moddy_lt. + unfold scale. + split. + - intros []%Cmult_integral; easy + auto. + - intros ->; lca. +Qed. + +Lemma mat_last_nonzero_val_eq_of_prop_gen {n m} (A B : Matrix n m) + c (Hc : c <> C0) (HAB0 : A 0 0 = (c * B 0 0)%C) : + A ≡ c .* B -> + mat_last_nonzero_val A = (c * mat_last_nonzero_val B)%C. +Proof. + intros HAB. + unfold mat_last_nonzero_val. + pose proof (mat_last_nonzero_eq_of_prop A B c Hc HAB) as Hrw. + unfold mat_last_nonzero in Hrw. + unfold last_nonzero_val. + rewrite Hrw. + destruct (last_nonzero_small_or_eq (fun i => B (i mod n) (i / n)) (n * m)) as + [Hsmall | Hz]. + - apply HAB; Modulus.show_moddy_lt. + - rewrite Hz. + destruct n; [apply HAB0|]. + simpl. + rewrite Nat.sub_diag. + apply HAB0. +Qed. + +Lemma mat_last_nonzero_val_eq_of_prop_nonempty {n m} (A B : Matrix n m) + c (Hc : c <> C0) (Hnm : n * m <> 0) : + A ≡ c .* B -> + mat_last_nonzero_val A = (c * mat_last_nonzero_val B)%C. +Proof. + intros HAB. + apply mat_last_nonzero_val_eq_of_prop_gen; [auto| |auto]. + apply HAB; lia. +Qed. + +Lemma prop_by_val_of_prop' {n m} (A B : Matrix n m) (c : C) (Hc : c <> C0) : + A ≡ c .* B -> + A ≡ (mat_last_nonzero_val A / mat_last_nonzero_val B) .* B. +Proof. + bdestruct (n * m =? 0). + - intros _ ?; nia. + - intros HAB. + rewrite HAB at 1. + apply mat_last_nonzero_val_eq_of_prop_nonempty in HAB; [|auto..]. + rewrite HAB. + unfold mat_last_nonzero_val, last_nonzero_val. + intros i j Hi Hj. + unfold scale. + destruct (last_nonzero_spec (fun i=>B (i mod n) (i / n)) (n * m)) + as [[Hsmall Hnz] | [Hlast Hzero]]. + + C_field. + + specialize (Hzero (j * n + i) ltac:(Modulus.show_moddy_lt)). + rewrite Modulus.mod_add_l, Nat.mod_small, Nat.div_add_l, + Nat.div_small, Nat.add_0_r in Hzero by lia. + rewrite Hzero. + lca. +Qed. + +Lemma mat_last_nonzero_eq_of_equiv {n m} {A B : Matrix n m} + (HAB : A ≡ B) (H : n * m <> 0) : + mat_last_nonzero_val A = mat_last_nonzero_val B. +Proof. + unfold mat_last_nonzero_val, last_nonzero_val. + pose proof (last_nonzero_small (fun i => A (i mod n) (i / n)) _ H) as Hsm. + revert Hsm. + erewrite last_nonzero_eq_of_zero_iff; + [intros ?; apply HAB; Modulus.show_moddy_lt|]. + intros k Hk. + rewrite HAB by Modulus.show_moddy_lt. + reflexivity. +Qed. + +Lemma prop_by_val_of_weakprop' {n m} (A B : Matrix n m) (c : C) : + A ≡ c .* B -> + A ≡ (mat_last_nonzero_val A / mat_last_nonzero_val B) .* B. +Proof. + destruct (Ceq_dec c C0). + - subst. + rewrite Mscale_0_l. + intros HA. + intros i j Hi Hj. + rewrite HA by auto. + unfold Zero. + assert (n * m <> 0) as Hnm by nia. + rewrite (mat_last_nonzero_eq_of_equiv HA Hnm). + unfold scale, mat_last_nonzero_val, last_nonzero_val, Zero. + lca. + - apply prop_by_val_of_prop'; auto. +Qed. + +Lemma prop_by_val_of_prop {n m} (A B : Matrix n m) : + (exists c, A ≡ c .* B /\ c <> C0) -> + A ≡ (mat_last_nonzero_val A / mat_last_nonzero_val B) .* B. +Proof. + intros (c & HAB & Hc). + apply prop_by_val_of_prop' with c; auto. +Qed. + +Lemma weakprop_iff_by_val {n m} (A B : Matrix n m) : + (exists c, A ≡ c .* B) <-> + A ≡ (mat_last_nonzero_val A / mat_last_nonzero_val B) .* B. +Proof. + split; [intros (c & HAB); apply prop_by_val_of_weakprop' with c; auto|]. + eauto. +Qed. + +Lemma mat_last_nonzero_val_eq_of_prop_strict {n m} (A B : Matrix n m) + c (Hc : c <> C0) : + A = c .* B -> + mat_last_nonzero_val A = (c * mat_last_nonzero_val B)%C. +Proof. + intros HAB. + unfold mat_last_nonzero_val. + pose proof (mat_last_nonzero_eq_of_prop A B c Hc ltac:(now rewrite HAB)) as Hrw. + unfold mat_last_nonzero in Hrw. + unfold last_nonzero_val. + rewrite Hrw, HAB. + reflexivity. +Qed. + +Lemma prop_by_val_of_strict_prop_WF {n m} (A B : Matrix n m) + (HA : WF_Matrix A) (HB : WF_Matrix B) : + (exists c, A = c .* B /\ c <> C0) -> + A = mat_last_nonzero_val A / mat_last_nonzero_val B .* B. +Proof. + intros (c & HAB & Hc). + apply mat_equiv_eq; [auto_wf..|]. + apply prop_by_val_of_prop. + rewrite HAB. + eauto using mat_equiv_refl. +Qed. + +Lemma mat_last_nonzero_val_zero_iff_WF {n m} (A : Matrix n m) + (HA : WF_Matrix A) : + mat_last_nonzero_val A = C0 <-> A = Zero. +Proof. + split. + - unfold mat_last_nonzero_val. + destruct (last_nonzero_spec (fun i : nat => A (i mod n) (i / n)) (n * m)) + as [[Hsm HF] | [Ha HZ]]. + + now intros H%HF. + + intros _. + apply mat_equiv_eq; [auto_wf..|]. + intros i j Hi Hj. + specialize (HZ (j * n + i) ltac:(Modulus.show_moddy_lt)). + rewrite Modulus.mod_add_l, Nat.mod_small, + Nat.div_add_l, Nat.div_small, Nat.add_0_r in HZ by lia. + exact HZ. + - intros ->. + reflexivity. +Qed. + +End ConcreteProp. + +Import ConcreteProp. + + + + +Local Open Scope C_scope. + + +Lemma eq_zero_of_prop {n m} (zx0 zx1 : ZX n m) + (H : zx0 ∝ zx1) : ⟦zx0⟧ = Zero -> ⟦zx1⟧ = Zero. +Proof. + destruct H as (c & HAB & Hc). + intros HZ; rewrite HZ in HAB. + apply mat_equiv_eq; [auto_wf..|]. + intros i j _ _. + pose proof (equal_f (equal_f HAB i) j) as H. + unfold scale, Zero in H. + symmetry in H. + rewrite Cmult_integral_iff in H. + destruct H; easy. +Qed. + +Lemma eq_zero_iff_of_prop {n m} {zx0 zx1 : ZX n m } + (H : zx0 ∝ zx1) : ⟦zx0⟧ = Zero <-> ⟦zx1⟧ = Zero. +Proof. + split; apply eq_zero_of_prop; easy. +Qed. + + + +Definition zxquot {n m} (zx0 zx1 : ZX n m) : C := + if Ceq_dec (mat_last_nonzero_val ⟦zx0⟧ / mat_last_nonzero_val ⟦zx1⟧) C0 then + C1 else mat_last_nonzero_val ⟦zx0⟧ / mat_last_nonzero_val ⟦zx1⟧. + +Lemma prop_by_quot_of_prop {n m} (zx0 zx1 : ZX n m) : + zx0 ∝ zx1 -> zx0 ∝[zxquot zx0 zx1] zx1. +Proof. + intros H. + pose proof H as Hstr%prop_by_val_of_strict_prop_WF; [|auto_wf..]. + unfold zxquot. + destruct (Ceq_dec (mat_last_nonzero_val ⟦zx0⟧ / mat_last_nonzero_val ⟦zx1⟧) C0) + as [[H0 | H1]%Cdiv_integral_dec | Hnz]. + - apply mat_last_nonzero_val_zero_iff_WF in H0; [|auto_wf]. + pose proof H0 as H1%(eq_zero_iff_of_prop H). + split; [|nonzero]. + rewrite H0, H1, Mscale_1_l. + reflexivity. + - apply mat_last_nonzero_val_zero_iff_WF in H1; [|auto_wf]. + pose proof H1 as H0%(eq_zero_iff_of_prop H). + split; [|nonzero]. + rewrite H0, H1, Mscale_1_l. + reflexivity. + - easy. +Qed. + +Lemma prop_by_iff_by_quot {n m} (zx0 zx1 : ZX n m) : + zx0 ∝ zx1 <-> zx0 ∝[zxquot zx0 zx1] zx1. +Proof. + split; [apply prop_by_quot_of_prop|]. + unfold proportional. + eauto. +Qed. + +Definition prop_by_sig {n m} (zx0 zx1 : ZX n m) : + zx0 ∝ zx1 -> {c | zx0 ∝[c] zx1} := + fun H => + exist _ (zxquot zx0 zx1) (prop_by_quot_of_prop zx0 zx1 H). + +(* Lemma mat_eq_dec_strong {n m} {A B : Matrix n m} + (HA : WF_Matrix A) (HB : WF_Matrix B) : + (A = B) + {'(i, j) : nat * nat | A i j <> B i j}. *) + +Module ProportionalDec. + +Lemma mat_eq_dec_WF {n m} {A B : Matrix n m} + (HA : WF_Matrix A) (HB : WF_Matrix B) : + {A = B} + {A <> B}. +Proof. + destruct (mat_equiv_dec A B) as [Heq | Hneq]. + - left. + apply mat_equiv_eq; assumption. + - right. + intros ->. + apply Hneq. + reflexivity. +(* Opaque because mat_equiv_dec is *) +Qed. + +Local Notation "'Decidable' P" := ({P} + {~ P}) + (at level 10, P at level 9) : type_scope. + +Lemma dec_and {P Q} (HP : Decidable P) (HQ : Decidable Q) : + Decidable (P /\ Q). +Proof. + destruct HP, HQ; [left|right..]; tauto. +Defined. + +Lemma dec_not {P} (HP : Decidable P) : + Decidable (~ P). +Proof. + destruct HP; [right|left]; tauto. +Defined. + +Lemma dec_iff {P Q} (HP : Decidable P) (H : P <-> Q) : + Decidable Q. +Proof. + destruct HP; [left | right]; tauto. +Defined. + +Lemma dec_iff' {P Q} (HP : Decidable P) (H : Q <-> P) : + Decidable Q. +Proof. + destruct HP; [left | right]; tauto. +Defined. + + + +Lemma proportional_by_1_dec {n m} (zx0 zx1 : ZX n m) : + Decidable (zx0 ∝= zx1). +Proof. + apply mat_eq_dec_WF; auto_wf. +Qed. + +Lemma proportional_by_dec {n m} (zx0 zx1 : ZX n m) (c : C) : + Decidable (zx0 ∝[c] zx1). +Proof. + apply dec_and. + - apply mat_eq_dec_WF; auto_wf. + - apply dec_not, Ceq_dec. +Qed. + +Lemma proportional_dec {n m} (zx0 zx1 : ZX n m) : + Decidable (zx0 ∝ zx1). +Proof. + refine (dec_iff' (proportional_by_dec _ _ _) (prop_by_iff_by_quot zx0 zx1)). +Qed. + +End ProportionalDec. diff --git a/src/Gates/GateRules.v b/src/Gates/GateRules.v index f15489c..dc6273d 100644 --- a/src/Gates/GateRules.v +++ b/src/Gates/GateRules.v @@ -24,15 +24,16 @@ Proof. all: split; nonzero. Qed. -Lemma _H_is_box : _H_ ∝ □. +Lemma _H_is_box : _H_ ∝[Cexp (PI/4)] □. Proof. - prop_exists_nonzero (Cexp (PI/4)). - simpl. + split; [|nonzero]. + prep_matrix_equivalence; cbn. unfold X_semantics, Z_semantics. + simpl. Msimpl. - solve_matrix; - field_simplify_eq [Cexp_PI2 Cexp_PI4 Ci2 Csqrt2_sqrt2_inv Csqrt2_inv]; - try apply c_proj_eq; try simpl; try R_field_simplify; try reflexivity; (try split; try apply RtoC_neq; try apply sqrt2_neq_0; try auto). + rewrite Cexp_PI2, Cexp_PI4. + unfold scale. + by_cell; cbn; C_field. Qed. Lemma _Rz_is_Rz : forall α, ⟦ _Rz_ α ⟧ = phase_shift α. @@ -53,7 +54,7 @@ Proof. all: lca. Qed. -Lemma cnot_involutive : _CNOT_R ⟷ _CNOT_ ∝ n_wire 2. +Lemma cnot_involutive : _CNOT_R ⟷ _CNOT_ ∝[/ C2] n_wire 2. Proof. rewrite <- compose_assoc. rewrite (compose_assoc (— ↕ (X 1 2 0))). @@ -71,7 +72,7 @@ Proof. simpl_casts. bundle_wires. rewrite (compose_assoc (— ↕ (⊂ ↕ —))). - rewrite wire_to_n_wire at 4. + rewrite wire_to_n_wire at 3. rewrite (nwire_stack_compose_topleft (X 2 1 0) (Z 2 2 (0 + 0))). rewrite <- (nwire_stack_compose_botleft (Z 2 2 (0 + 0)) (X 2 1 0)). repeat rewrite <- compose_assoc. @@ -79,7 +80,7 @@ Proof. rewrite <- (stack_compose_distr (n_wire 2) (n_wire (1 + 1)) (X 2 1 0) (X 1 2 0)). rewrite X_spider_1_1_fusion. rewrite Rplus_0_r. - simpl; cleanup_zx; simpl_casts. + cbn; cleanup_zx; simpl_casts. rewrite (compose_assoc _ (— ↕ — ↕ X 2 2 _)). rewrite stack_assoc. simpl_casts. @@ -110,7 +111,7 @@ Proof. rewrite <- (stack_compose_distr — — (Z 1 2 0 ↕ —)). rewrite <- stack_compose_distr. cleanup_zx. - rewrite hopf_rule_Z_X. + zxrewrite hopf_rule_Z_X. rewrite wire_to_n_wire. rewrite stack_nwire_distribute_r. rewrite stack_nwire_distribute_l. @@ -127,19 +128,19 @@ Proof. rewrite <- wire_to_n_wire. rewrite <- (stack_compose_distr — — — —). cleanup_zx. - easy. + zxrefl. Unshelve. all: lia. Qed. -Lemma cnot_is_cnot_r : _CNOT_ ∝ _CNOT_R. +Lemma cnot_is_cnot_r : _CNOT_ ∝= _CNOT_R. Proof. intros. remember (— ↕ X 1 2 0 ⟷ (Z 2 1 0 ↕ —)) as RHS. rewrite (Z_wrap_under_bot_left 1 1). rewrite (X_wrap_over_top_left 1 1). simpl_casts. - rewrite wire_to_n_wire at 2 3 4 5. + rewrite wire_to_n_wire. rewrite stack_nwire_distribute_l. rewrite stack_nwire_distribute_r. repeat rewrite <- compose_assoc. @@ -161,7 +162,7 @@ Proof. rewrite <- (nwire_stack_compose_topleft (⊃ ↕ n_wire 1)). rewrite <- compose_assoc. rewrite (compose_assoc _ (n_wire 1 ↕ ⊂ ↕ n_wire 2) _). - simpl; cleanup_zx; simpl_casts. + cbn; cleanup_zx; simpl_casts. rewrite 2 stack_assoc; simpl_casts. rewrite <- stack_wire_distribute_l. rewrite 2 stack_assoc_back; simpl_casts. @@ -175,16 +176,16 @@ Unshelve. all: lia. Qed. -Lemma cnot_inv_is_swapped_cnot : _CNOT_inv_ ∝ ⨉ ⟷ _CNOT_ ⟷ ⨉. +Lemma cnot_inv_is_swapped_cnot : _CNOT_inv_ ∝= ⨉ ⟷ _CNOT_ ⟷ ⨉. Admitted. -Lemma notc_is_swapp_cnot : _NOTC_ ∝ ⨉ ⟷ _CNOT_ ⟷ ⨉. +Lemma notc_is_swapp_cnot : _NOTC_ ∝= ⨉ ⟷ _CNOT_ ⟷ ⨉. Admitted. -Lemma notc_r_is_swapp_cnot_r : _NOTC_R ∝ ⨉ ⟷ _CNOT_R ⟷ ⨉. +Lemma notc_r_is_swapp_cnot_r : _NOTC_R ∝= ⨉ ⟷ _CNOT_R ⟷ ⨉. Admitted. -Lemma notc_is_notc_r : _NOTC_ ∝ _NOTC_R. +Lemma notc_is_notc_r : _NOTC_ ∝= _NOTC_R. Proof. rewrite notc_is_swapp_cnot. rewrite cnot_is_cnot_r. diff --git a/src/Ingest/Ingest.v b/src/Ingest/Ingest.v index 78bbda4..4842abb 100644 --- a/src/Ingest/Ingest.v +++ b/src/Ingest/Ingest.v @@ -351,6 +351,7 @@ Proof. repeat rewrite kron_1_r; try auto with wf_db. * replace (S n - n - 1)%nat with 0%nat by lia. apply Mscale_simplify; [ | easy ]. + fold (n_wire (S n)). rewrite n_wire_semantics. repeat rewrite id_kron. replace (2 ^ S n + (2 ^ S n + 0))%nat with (2 * 2 ^ S n)%nat by lia. @@ -431,6 +432,7 @@ Proof. repeat rewrite unfold_pad. simpl. Msimpl. + fold (n_wire n). rewrite n_wire_semantics. rewrite id_kron. replace (2 ^ n + (2 ^ n + 0))%nat with (2 * 2 ^ n)%nat by lia.