Fixes for 8.16

inQWIRE · Jan 21, 2025 · d23b369 · d23b369
1 parent e3bc141
commit d23b369
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/src/CoreRules/SwapRules.v b/src/CoreRules/SwapRules.v
@@ -358,7 +358,7 @@ Lemma a_swap_transpose : forall n,
   (a_swap n) ⊤ ∝= a_swap n.
 Proof.
   intros.
-  induction n using (Nat.measure_induction nat idn).
+  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 | ].

diff --git a/src/CoreRules/ZXRules.v b/src/CoreRules/ZXRules.v
@@ -108,7 +108,7 @@ Proof.
 	replace (0)%R with (0 * PI)%R at 1 by lra.
 	replace (0)%R with (INR 0)%R by reflexivity.
 	zxrewrite X_state_copy.
-	rewrite INR_0, Rmult_0_l.
+	rewrite Rmult_0_l.
 	zxrefl.
 Qed.
 
@@ -131,7 +131,7 @@ Proof.
 	replace (0)%R with (0 * PI)%R at 1 by lra.
 	replace (0)%R with (INR 0)%R by reflexivity.
 	zxrewrite Z_state_copy.
-	rewrite INR_0, Rmult_0_l.
+	rewrite Rmult_0_l.
 	zxrefl.
 Qed.
 

diff --git a/src/DiagramRules/Soundness.v b/src/DiagramRules/Soundness.v
@@ -52,7 +52,7 @@ Proof.
   - C_field.
   - rewrite Cmod_div by auto.
     rewrite Hmod.
-    rewrite Rdiv_diag; [reflexivity|].
+    apply Rinv_r.
     rewrite Cmod_eq_0_iff.
     auto.
 Qed.