Feature definitional cast

src/CoreData/Proportional.v

@@ -847,6 +847,7 @@ Lemma cast_compat :
     cast n' m' prfn0 prfm0 zx0 ∝ cast n' m' prfn0 prfm0 zx1.
 Proof.
   intros n m n' m' Hn Hm zx0 zx1 [x [Hzx0 Hx]].
+  rewrite fn_cast_eq_cast_core.
   subst.
   prop_exists_nonzero x; auto.
 Qed.

src/CoreData/ZXCore.v

@@ -2,6 +2,7 @@
 Require Import QuantumLib.Proportional.
 Require Import QuantumLib.VectorStates.
 Require Import QuantumLib.Kronecker.
+Require StrictProp.
 
 Require Export SemanticCore.
 
@@ -32,14 +33,55 @@
           ZX (n_0 + n_1) (m_0 + m_1)
   | Compose {n m o} (zx0 : ZX n m) (zx1 : ZX m o) : ZX n o.
 
-Definition cast (n m : nat) {n' m'} 
+
+
+Definition cast_core (n m : nat) {n' m'} 
               (prfn : n = n') (prfm : m = m') (zx : ZX n' m') : ZX n m.
 Proof.
   destruct prfn.
   destruct prfm.
   exact zx.
 Defined.
 
+
+(* @nocheck name *)
+Definition False_rect' {A : Type} (f : False) : A :=
+	StrictProp.sEmpty_rect (fun _ => A) (False_sind _ f).
+
+(* @nocheck name *)
+Lemma False_rect'_irrel {A} (f f' : False) : 
+	@False_rect' A f = False_rect' f'.
+Proof.
+	reflexivity.
+Qed.
+
+Definition canon_nateq {n m} (H : n = m) : n = m :=
+  match Nat.eq_dec n m with 
+  | left Hnm => Hnm
+  | right HF => False_rect' (HF H)
+  end.
+
+Definition cast (n m : nat) {n' m'} (Hn : n = n') (Hm : m = m') 
+	(zx : ZX n' m') : ZX n m :=
+	cast_core n m (canon_nateq Hn) (canon_nateq Hm) zx.
+
+Notation cast' n m prfn prfm zx := (cast n m (eq_sym prfn) (eq_sym prfm) zx)
+  (only parsing).
+
+Lemma cast_eq_cast_core {n m n' m'} (Hn : n = n') (Hm : m = m') (zx : ZX n' m') :
+	cast n m Hn Hm zx = cast_core n m Hn Hm zx.
+Proof.
+  unfold cast.
+  f_equal; apply UIP_nat.
+Qed.
+
+Lemma fn_cast_eq_cast_core : @cast = @cast_core.
+Proof.
+	repeat (apply functional_extensionality_dep; intros).
+	apply cast_eq_cast_core.
+Qed.
+
+
 (* Notations for the ZX diagrams *)
 Notation "⦰" := Empty : ZX_scope. (* \revemptyset *)
 Notation "⊂" := Cup : ZX_scope. (* \subset *)
@@ -91,6 +133,7 @@
 Lemma cast_semantics : forall {n m n' m'} {eqn eqm} (zx : ZX n m),
   ⟦ cast n' m' eqn eqm zx ⟧ = ⟦ zx ⟧.
 Proof.
+  rewrite fn_cast_eq_cast_core.
   intros.
   subst.
   easy.
@@ -190,9 +233,9 @@
 Definition n_wire := fun n => n ↑ Wire.
 Definition n_box := fun n => n ↑ Box.
 
 #[global]
 Arguments n_wire !_%nat_scope /. 
 #[global]
 Arguments n_box !_%nat_scope /. 
 
 Lemma n_wire_semantics {n} : ⟦ n_wire n ⟧ = I (2^n).
@@ -221,7 +264,7 @@
 
 (* Transpose of a diagram *)
 
 Reserved Notation "zx ⊤" (at level 0). (* \top *)
 Fixpoint transpose {nIn nOut} (zx : ZX nIn nOut) : ZX nOut nIn :=
   match zx with
   | ⦰ => ⦰
@@ -237,7 +280,7 @@
 
 (* Negating the angles of a diagram, complex conjugate *)
 
 Reserved Notation "zx ⊼" (at level 0). (* \barwedge *)
 Fixpoint conjugate {n m} (zx : ZX n m) : ZX n m :=
   match zx with
   | Z n m α => Z n m (-α)

src/CoreRules/CapCupRules.v

@@ -58,7 +58,8 @@ Lemma n_cup_1_cup : n_cup 1 ∝= ⊃.
 Proof.
   unfold n_cup.
   cbn.
-  rewrite stack_empty_r_fwd, 2 cast_id.
+  rewrite stack_empty_r.
+  cbn.
   rewrite wire_removal_l.
   bundle_wires.
   now rewrite 2!nwire_removal_l.
@@ -591,13 +592,14 @@ Proof.
     repeat rewrite cast_contract.
     apply compose_simplify_eq; [ | apply cast_simplify_eq; easy].
     simpl_casts.
-    rewrite 2 stack_assoc.
+    rewrite 2 stack_assoc_fwd.
     simpl_casts.
     rewrite wire_to_n_wire, n_wire_stack.
-    rewrite 2 stack_assoc_back.
+    rewrite 2 stack_assoc_back_fwd.
     simpl_casts.
-    erewrite <- (@cast_n_wire (n + 1) (S n)) at 2.
+    erewrite <- (@cast_n_wire (n + 1) (1 + n)).
     rewrite cast_stack_r.
+    rewrite cast_n_wire.
     rewrite n_wire_stack.
     cast_irrelevance.
 Unshelve.
@@ -983,8 +985,7 @@ Proof.
   induction n.
   - unfold n_cup, n_stacked_caps.
     cbn.
-    rewrite zx_of_perm_0.
-    now rewrite stack_empty_l, cast_id.
+    now rewrite stack_empty_l.
   - rewrite n_cup_grow_l.
     rewrite n_stacked_caps_succ.
     rewrite IHn.