Remove all possible 8.18 deprecation warnings while keeping 8.16 working

inQWIRE · Jan 25, 2024 · 63736c5 · 63736c5
1 parent a8d111f
commit 63736c5
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 12 deletions.
diff --git a/Complex.v b/Complex.v
@@ -624,6 +624,7 @@ Proof.  intros.
         rewrite <- H' in H2. easy.
 Qed.
 
+
 Lemma Cinv_mult_distr : forall c1 c2 : C, c1 <> 0 -> c2 <> 0 -> / (c1 * c2) = / c1 * / c2.
 Proof.
   intros.
@@ -634,7 +635,7 @@ Proof.
     rewrite Rmult_div.
     rewrite Rmult_opp_opp.
     unfold Rminus.
-    rewrite <- RIneq.Ropp_div.
+    rewrite <- Ropp_div.
     rewrite <- Rdiv_plus_distr.
     rewrite Rmult_plus_distr_r.
     rewrite Rmult_plus_distr_l.

diff --git a/FiniteGroups.v b/FiniteGroups.v
@@ -16,7 +16,7 @@ Global Program Instance list_is_monoid {X} : Monoid (list X) :=
   { Gzero := []
   ; Gplus := @app X
   }.
-Next Obligation. rewrite app_nil_end; easy. Qed.
+Next Obligation. rewrite <- app_nil_r; easy. Qed.
 Next Obligation. rewrite app_assoc; easy. Qed.
 
 

diff --git a/Polynomial.v b/Polynomial.v
@@ -1031,7 +1031,7 @@ Lemma Peq_skipn_Peq_nil : forall (p1 p2 : Polynomial),
   skipn (length p1) p2 ≅ [].
 Proof. intros. 
        apply Peq_firstn_eq in H0; auto.
-       rewrite (app_nil_end p1) in H.
+       rewrite <- (app_nil_r p1) in H.
        rewrite H0, <- (firstn_skipn (length p1)) in H. 
        apply Peq_app_Peq in H.
        easy. 
@@ -1378,14 +1378,16 @@ Proof. apply ind_from_end; try easy.
          destruct H0 as [n [a [p' [H1 H2] ] ] ].
          exists (S n), a, p'.
          split; auto. 
-         rewrite H2, app_assoc_reverse.
+         rewrite H2, <- app_assoc.
          apply f_equal_gen; try easy.
          simpl. 
          rewrite repeat_cons.
          easy. 
        - exists 0, x, l.
-         split; auto.         
-         apply app_nil_end.
+         split; auto. 
+         simpl.        
+         rewrite app_nil_r.
+         easy.
 Qed.
 
 Lemma compactify_breakdown : forall (p : Polynomial),

diff --git a/Prelim.v b/Prelim.v
@@ -290,13 +290,13 @@ Tactic Notation "gen" ident(X1) ident(X2) ident(X3) ident(X4) ident(X5) :=
 
 Lemma double_mult : forall (n : nat), (n + n = 2 * n)%nat. Proof. intros. lia. Qed.
 Lemma pow_two_succ_l : forall x, (2^x * 2 = 2 ^ (x + 1))%nat.
-Proof. intros. rewrite Nat.mul_comm. rewrite <- Nat.pow_succ_r'. intuition. Qed.
+Proof. intros. rewrite Nat.mul_comm. rewrite <- Nat.pow_succ_r'. auto with *. Qed.
 Lemma pow_two_succ_r : forall x, (2 * 2^x = 2 ^ (x + 1))%nat.
-Proof. intros. rewrite <- Nat.pow_succ_r'. intuition. Qed.
+Proof. intros. rewrite <- Nat.pow_succ_r'. auto with *. Qed.
 Lemma double_pow : forall (n : nat), (2^n + 2^n = 2^(n+1))%nat. 
 Proof. intros. rewrite double_mult. rewrite pow_two_succ_r. reflexivity. Qed.
 Lemma pow_components : forall (a b m n : nat), a = b -> m = n -> (a^m = b^n)%nat.
-Proof. intuition. Qed.
+Proof. auto with *. Qed.
 Lemma pow_positive : forall a b, a <> 0 -> 0 < a ^ b.
 Proof. intros. induction b; simpl; lia. Qed.  
 
@@ -378,7 +378,7 @@ Qed.
 Corollary subset_self : forall (X : Type) (l1 : list X),
   l1 ⊆ l1. 
 Proof. intros X l1. assert (H: l1 ⊆ (l1 ++ [])). { apply subset_concat_l. }
-       rewrite <- app_nil_end in H. apply H. 
+       rewrite app_nil_r in H. apply H. 
 Qed.
 
 Lemma subsets_add : forall (X : Type) (l1 l2 l3 : list X),

diff --git a/Quantum.v b/Quantum.v
@@ -898,7 +898,8 @@ Proof.
         ++ apply functional_extensionality. intros x.
            bdestructΩ (n + x <? n).
            bdestructΩ (n <=? n + x).
-           rewrite minus_plus.
+           rewrite (Nat.add_comm n x).
+           rewrite Nat.add_sub.
            easy.
         ++ intros x L.
            bdestructΩ (y =? x).
@@ -955,7 +956,8 @@ Proof.
         ++ apply functional_extensionality. intros z.
            bdestructΩ (n + z <? n).
            bdestructΩ (n <=? n + z).
-           rewrite minus_plus.
+           rewrite (Nat.add_comm n z).
+           rewrite Nat.add_sub.
            easy.
         ++ rewrite big_sum_0. easy.
            intros z.