From 76eacdb2d301764fe016260c2035285221b35a20 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 20 Sep 2024 12:43:02 +0200 Subject: [PATCH] Adapt to https://github.com/coq/coq/pull/19530 --- src/Algebra/IntegralDomain.v | 2 +- src/Algebra/Nsatz.v | 35 ++++++---------------- src/Arithmetic/ModularArithmeticTheorems.v | 8 ++--- src/Arithmetic/PrimeFieldTheorems.v | 2 +- src/Compilers/MapBaseType.v | 2 +- src/Compilers/MapBaseTypeWf.v | 2 +- src/Compilers/Named/AListContext.v | 4 +-- src/Compilers/Named/FMapContext.v | 2 +- src/Compilers/Named/MapCast.v | 2 +- src/Compilers/Named/MapCastInterp.v | 2 +- src/Compilers/Named/MapCastWf.v | 2 +- src/Compilers/Named/MapType.v | 2 +- src/Primitives/MxDHRepChange.v | 2 +- src/Util/AdditionChainExponentiation.v | 2 +- src/Util/Factorize.v | 2 +- src/Util/ListUtil.v | 2 +- src/Util/ListUtil/SetoidList.v | 2 +- src/Util/MSetPositive/Facts.v | 2 +- src/Util/Tuple.v | 2 +- 19 files changed, 31 insertions(+), 48 deletions(-) diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v index bfdc36bd68..63e7d76ed7 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -173,7 +173,7 @@ End IntegralDomain. (** Tactics for polynomial equations over integral domains *) -Require Coq.nsatz.Nsatz. +From Coq Require NsatzTactic. Ltac dropAlgebraSyntax := cbv beta delta [ diff --git a/src/Algebra/Nsatz.v b/src/Algebra/Nsatz.v index bd754dd2ce..426579eae5 100644 --- a/src/Algebra/Nsatz.v +++ b/src/Algebra/Nsatz.v @@ -2,28 +2,17 @@ periodically check whether we still need it -- once enough bugs get fixed in mailine, we hope to drop this implementation *) -Require Coq.nsatz.Nsatz. -Require Import Coq.Lists.List. +From Coq Require NsatzTactic. +From Coq Require Import List. Require Export Crypto.Util.FixCoqMistakes. -(** For compat with https://github.com/coq/coq/pull/12073 *) -Module Nsatz. - Import nsatz.Nsatz. - Notation check_correct := check_correct. - Ltac Nsatz_nsatz := nsatz. - Ltac nsatz := Nsatz_nsatz. - Notation PEevalR := PEevalR. - Notation psos_r1 := psos_r1. - Notation psos_r1b := psos_r1b. -End Nsatz. - Generalizable All Variables. Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)} : forall x y, eq (sub x y) zero <-> eq x y. Proof. split;intros Hx. - { eapply Nsatz.psos_r1b. eapply Hx. } - { eapply Nsatz.psos_r1. eapply Hx. } + { eapply NsatzTactic.psos_r1b. eapply Hx. } + { eapply NsatzTactic.psos_r1. eapply Hx. } Qed. Ltac get_goal := lazymatch goal with |- ?g => g end. @@ -54,15 +43,9 @@ Ltac nsatz_get_reified_goal reified_package := lazymatch reified_package with (_, _, ?goal) => goal end. Require Import Coq.setoid_ring.Ring_polynom. -(* Kludge for 8.4/8.5 compatibility *) -Module Import mynsatz_compute. - Import nsatz.Nsatz. - Global Ltac mynsatz_compute x := nsatz_compute x. -End mynsatz_compute. -Ltac nsatz_compute x := mynsatz_compute x. Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens := - nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). + NsatzTactic.nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens). Ltac nsatz_compute_get_leading_coefficient := lazymatch goal with @@ -111,15 +94,15 @@ Ltac nsatz_domain_sugar_power domain sugar power := nsatz_rewrite_and_revert domain; let reified_package := nsatz_reify_equations eq zero in let fv := nsatz_get_free_variables reified_package in - let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in + let interp := constr:(@NsatzTactic.PEevalR _ _ _ _ _ _ _ _ Fops fv) in let reified_givens := nsatz_get_reified_givens reified_package in let reified_goal := nsatz_get_reified_goal reified_package in nsatz_compute_to_goal sugar nparams reified_goal power reified_givens; let a := nsatz_compute_get_leading_coefficient in let crt := nsatz_compute_get_certificate in intros _ (* discard [nsatz_compute] output *); intros; - apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); - [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] + apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@NsatzTactic.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond)); + [ nsatz_nonzero; cbv iota beta delta [NsatzTactic.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS] | solve [vm_cast_no_check (eq_refl true)] (* if this fails, the prover returned a bad certificate *) | solve [repeat (split; [assumption|]); exact I] ] end. @@ -182,7 +165,7 @@ Module Export Hints. Ncring_initial.gen_phiZ_morph Ncring_initial.multiplication_phi_ring . - Import nsatz.Nsatz. + Import NsatzTactic. Global Existing Instances Qops Qri diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 835aba5af9..45f51ac983 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -1,10 +1,10 @@ -Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. +From Coq Require Import Lia Morphisms Morphisms_Prop. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.Arithmetic.ModularArithmeticPre. -Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) -Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop Coq.Setoids.Setoid. -Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. +From Coq Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *) +From Coq Require Import Morphisms Morphisms_Prop Setoid. +From Coq Require Export InitialRing Ring_theory Ring_tac NArithRing. Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult. Require Crypto.Algebra.Ring Crypto.Algebra.Field. diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index ee731a24cf..4d833f5ac5 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -2,7 +2,7 @@ Require Export Crypto.Spec.ModularArithmetic. Require Export Crypto.Arithmetic.ModularArithmeticTheorems. Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac. -Require Import Coq.nsatz.Nsatz. +From Coq Require Import NsatzTactic. Require Import Coq.micromega.Lia Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Import Crypto.Arithmetic.ModularArithmeticPre. Require Import Crypto.Util.NumTheoryUtil. diff --git a/src/Compilers/MapBaseType.v b/src/Compilers/MapBaseType.v index 554bba4a2d..ca54461f67 100644 --- a/src/Compilers/MapBaseType.v +++ b/src/Compilers/MapBaseType.v @@ -1,4 +1,4 @@ -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.ExprInversion. diff --git a/src/Compilers/MapBaseTypeWf.v b/src/Compilers/MapBaseTypeWf.v index d612ad5bf3..eca4cdba14 100644 --- a/src/Compilers/MapBaseTypeWf.v +++ b/src/Compilers/MapBaseTypeWf.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Wf. diff --git a/src/Compilers/Named/AListContext.v b/src/Compilers/Named/AListContext.v index ffc8355eed..7a1d68990f 100644 --- a/src/Compilers/Named/AListContext.v +++ b/src/Compilers/Named/AListContext.v @@ -1,6 +1,6 @@ (** * Context made from an associative list, without modules *) -Require Import Coq.Bool.Sumbool. -Require Import Coq.Lists.List. +From Coq Require Import Sumbool. +From Coq Require Import List. Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Util.Tactics.BreakMatch. diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v index 6cac1b597e..b90c3bd8ce 100644 --- a/src/Compilers/Named/FMapContext.v +++ b/src/Compilers/Named/FMapContext.v @@ -1,4 +1,4 @@ -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Coq.FSets.FMapInterface. Require Import Coq.FSets.FMapFacts. Require Import Crypto.Compilers.Named.Context. diff --git a/src/Compilers/Named/MapCast.v b/src/Compilers/Named/MapCast.v index fddee84faf..31f67f6e11 100644 --- a/src/Compilers/Named/MapCast.v +++ b/src/Compilers/Named/MapCast.v @@ -1,4 +1,4 @@ -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Named.Context. diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v index 2c757d5ed0..c915794800 100644 --- a/src/Compilers/Named/MapCastInterp.v +++ b/src/Compilers/Named/MapCastInterp.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Relations. diff --git a/src/Compilers/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v index b3698d94dc..8a74371e47 100644 --- a/src/Compilers/Named/MapCastWf.v +++ b/src/Compilers/Named/MapCastWf.v @@ -1,5 +1,5 @@ Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Coq.Logic.Eqdep_dec. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Relations. diff --git a/src/Compilers/Named/MapType.v b/src/Compilers/Named/MapType.v index 15b40f7b7b..b750b6ca74 100644 --- a/src/Compilers/Named/MapType.v +++ b/src/Compilers/Named/MapType.v @@ -1,4 +1,4 @@ -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Named.Syntax. diff --git a/src/Primitives/MxDHRepChange.v b/src/Primitives/MxDHRepChange.v index d015a561fb..23c9112ab8 100644 --- a/src/Primitives/MxDHRepChange.v +++ b/src/Primitives/MxDHRepChange.v @@ -1,4 +1,4 @@ -Require Import Coq.Lists.SetoidList. +From Coq Require Import SetoidList. Require Import Crypto.Spec.MxDH. Require Import Crypto.Algebra.Monoid Crypto.Algebra.Group Crypto.Algebra.Ring Crypto.Algebra.Field. Require Import Crypto.Util.Tuple Crypto.Util.Prod. diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v index 803cc85c63..9da5c67d98 100644 --- a/src/Util/AdditionChainExponentiation.v +++ b/src/Util/AdditionChainExponentiation.v @@ -1,5 +1,5 @@ Require Import Coq.funind.FunInd. -Require Import Coq.Lists.List Coq.Lists.SetoidList. Import ListNotations. +From Coq Require Import List SetoidList. Import ListNotations. Require Import Coq.Numbers.BinNums Coq.NArith.BinNat. Require Import Crypto.Util.ListUtil. Require Import Crypto.Algebra.Monoid Crypto.Algebra.ScalarMult. diff --git a/src/Util/Factorize.v b/src/Util/Factorize.v index 40ae914175..3b66bcccb7 100644 --- a/src/Util/Factorize.v +++ b/src/Util/Factorize.v @@ -1,4 +1,4 @@ -Require Import Coq.Bool.Sumbool. +From Coq Require Import Sumbool. Require Import Coq.micromega.Psatz Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Import Coq.NArith.NArith. Require Import Coq.PArith.PArith. diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index cc475db2ef..820cc92774 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -1819,7 +1819,7 @@ Hint Rewrite <- @firstn_update_nth : pull_firstn. #[global] Hint Rewrite <- @firstn_update_nth : push_update_nth. -Require Import Coq.Lists.SetoidList. +From Coq Require Import SetoidList. Global Instance Proper_nth_default : forall A eq, Proper (eq==>eqlistA eq==>Logic.eq==>eq) (nth_default (A:=A)). Proof. diff --git a/src/Util/ListUtil/SetoidList.v b/src/Util/ListUtil/SetoidList.v index 59bae9ac41..461c3a07c2 100644 --- a/src/Util/ListUtil/SetoidList.v +++ b/src/Util/ListUtil/SetoidList.v @@ -1,6 +1,6 @@ Require Import Coq.Lists.List. Require Import Coq.Setoids.Setoid. -Require Import Coq.Lists.SetoidList. +From Coq Require Import SetoidList. Require Import Crypto.Util.Option. Import ListNotations. diff --git a/src/Util/MSetPositive/Facts.v b/src/Util/MSetPositive/Facts.v index 540eac074a..20077e980e 100644 --- a/src/Util/MSetPositive/Facts.v +++ b/src/Util/MSetPositive/Facts.v @@ -1,7 +1,7 @@ Require Import Coq.Setoids.Setoid. Require Import Coq.Classes.Morphisms Coq.Classes.Morphisms_Prop. Require Import Coq.Lists.List. -Require Import Coq.Lists.SetoidList. +From Coq Require Import SetoidList. Require Import Coq.MSets.MSetPositive. Require Import Coq.MSets.MSetFacts. Require Import Crypto.Util.Tactics.BreakMatch. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 2431be73b6..daa883394b 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -1156,7 +1156,7 @@ Proof. repeat intro; subst; auto; reflexivity. Qed. -Require Import Coq.Lists.SetoidList. +From Coq Require Import SetoidList. Global Instance fieldwise'_Proper : forall {n A B}, Proper (pointwise_relation _ (pointwise_relation _ impl) ==> eq ==> eq ==> impl) (@fieldwise' A B n) | 10.