From 427bd2d0476a0b814774bcabce54b11ce27a3495 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 3 Feb 2023 14:56:57 +0100 Subject: [PATCH] Warn on Qed Let declaration cf https://github.com/coq/coq/issues/10459 --- doc/sphinx/language/core/sections.rst | 7 ++++ test-suite/output/SuggestProofUsing.v | 1 + test-suite/output/UnivBinders.out | 3 ++ theories/Arith/PeanoNat.v | 2 +- theories/FSets/FSetEqProperties.v | 16 ++++---- theories/Logic/Eqdep_dec.v | 2 +- theories/MSets/MSetEqProperties.v | 8 ++-- theories/NArith/NArith.v | 2 +- theories/Numbers/Cyclic/Int31/Ring31.v | 2 +- theories/Numbers/Cyclic/Int63/Ring63.v | 2 +- theories/Numbers/Integer/Binary/ZBinary.v | 2 +- theories/QArith/Qfield.v | 46 ++++++++++++++++------- theories/Sorting/Permutation.v | 8 ++-- theories/ZArith/Wf_Z.v | 4 +- vernac/declare.ml | 10 ++++- 15 files changed, 78 insertions(+), 37 deletions(-) diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 8f17ec4e9ac4..c0ed0167ddad 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -66,6 +66,13 @@ usable outside the section as shown in this :ref:`example ff diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index ba605b7be5aa..440e478a5d07 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -1265,5 +1265,5 @@ Register Nat.nlt_0_r as num.nat.nlt_0_r. Section TestOrder. Let test : forall x y, x<=y -> y<=x -> x=y. - Proof. Nat.order. Qed. + Proof. Nat.order. Defined. End TestOrder. diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index 10f3955870b2..4a040bf0ffdf 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -596,10 +596,13 @@ Section Bool. Variable f:elt->bool. Variable Comp: Proper (E.eq==>Logic.eq) f. -Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)). +Local Definition Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)). Proof. repeat red; intros; f_equal; auto. -Qed. +Defined. + +Local Hint Resolve Comp' : core. +Local Hint Unfold compat_bool : core. Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x. Proof. @@ -694,7 +697,7 @@ Qed. Lemma union_filter: forall f g, (compat_bool E.eq f) -> (compat_bool E.eq g) -> forall s, union (filter f s) (filter g s) [=] filter (fun x=>orb (f x) (g x)) s. Proof. -clear Comp' Comp f. +clear Comp f. intros. assert (compat_bool E.eq (fun x => orb (f x) (g x))). - unfold compat_bool, Proper, respectful; intros. @@ -785,10 +788,7 @@ Section Bool'. Variable f:elt->bool. Variable Comp: compat_bool E.eq f. -Let Comp' : compat_bool E.eq (fun x =>negb (f x)). -Proof. -unfold compat_bool, Proper, respectful in *; intros; f_equal; auto. -Qed. +Hint Resolve Comp' : core. Lemma exists_mem_1: forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false. @@ -826,7 +826,7 @@ Proof. intros. rewrite for_all_exists in H; auto. rewrite negb_true_iff in H. -destruct (for_all_mem_4 (fun x =>negb (f x)) Comp' s) as (x,p); auto. +destruct (for_all_mem_4 (fun x =>negb (f x)) (Comp' f Comp) s) as (x,p); auto. elim p;intros. exists x;split;auto. rewrite <-negb_false_iff; auto. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index 4af90ae12d7a..6893df07e07b 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -61,7 +61,7 @@ Section EqdepDec. | or_intror neqxy => False_ind _ (neqxy u) end. - Let nu_constant (y:A) (u v:x = y) : nu u = nu v. + Local Definition nu_constant (y:A) (u v:x = y) : nu u = nu v. unfold nu. destruct (eq_dec y) as [Heq|Hneq]. - reflexivity. diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index 1e42ebc8bd63..2c75880205a9 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -601,7 +601,7 @@ Variable Comp: Proper (E.eq==>Logic.eq) f. Let Comp' : Proper (E.eq==>Logic.eq) (fun x =>negb (f x)). Proof. repeat red; intros; f_equal; auto. -Qed. +Defined. Lemma filter_mem: forall s x, mem x (filter f s)=mem x s && f x. Proof. @@ -784,10 +784,12 @@ Section Bool'. Variable f:elt->bool. Variable Comp: Proper (E.eq==>Logic.eq) f. -Let Comp' : Proper (E.eq==>Logic.eq) (fun x => negb (f x)). +Local Definition Comp' : Proper (E.eq==>Logic.eq) (fun x => negb (f x)). Proof. repeat red; intros; f_equal; auto. -Qed. +Defined. + +Local Hint Resolve Comp' : core. Lemma exists_mem_1: forall s, (forall x, mem x s=true->f x=false) -> exists_ f s=false. diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index d17edaed2b46..82adc5bf5438 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -31,5 +31,5 @@ Section TestOrder. Let test : forall x y, x<=y -> y<=x -> x=y. Proof. N.order. - Qed. + Defined. End TestOrder. diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v index cfff25aab4b9..028b1cf46ac4 100644 --- a/theories/Numbers/Cyclic/Int31/Ring31.v +++ b/theories/Numbers/Cyclic/Int31/Ring31.v @@ -103,5 +103,5 @@ Add Ring Int31Ring : Int31Ring Section TestRing. Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x. intros. ring. -Qed. +Defined. End TestRing. diff --git a/theories/Numbers/Cyclic/Int63/Ring63.v b/theories/Numbers/Cyclic/Int63/Ring63.v index 9ccf4cceb19c..7e0d4857658a 100644 --- a/theories/Numbers/Cyclic/Int63/Ring63.v +++ b/theories/Numbers/Cyclic/Int63/Ring63.v @@ -63,5 +63,5 @@ Add Ring Uint63Ring : Uint63Ring Section TestRing. Let test : forall x y, 1 + x*y + x*x + 1 = 1*1 + 1 + y*x + 1*x*x. intros. ring. -Qed. +Defined. End TestRing. diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 8944cc8638c6..1c3725810624 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -33,7 +33,7 @@ Section TestOrder. Let test : forall x y, x<=y -> y<=x -> x=y. Proof. z_order. - Qed. + Defined. End TestOrder. (** Z forms a ring *) diff --git a/theories/QArith/Qfield.v b/theories/QArith/Qfield.v index 92da59377c3b..5d66c9794600 100644 --- a/theories/QArith/Qfield.v +++ b/theories/QArith/Qfield.v @@ -83,53 +83,73 @@ Add Field Qfield : Qsft Section Examples. +Section Ex1. Let ex1 : forall x y z : Q, (x+y)*z == (x*z)+(y*z). intros. ring. -Qed. +Defined. +End Ex1. +Section Ex2. Let ex2 : forall x y : Q, x+y == y+x. intros. ring. -Qed. +Defined. +End Ex2. +Section Ex3. Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z). intros. ring. -Qed. +Defined. +End Ex3. +Section Ex4. Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2). ring. -Qed. +Defined. +End Ex4. +Section Ex5. Let ex5 : 1+1 == 2#1. ring. -Qed. +Defined. +End Ex5. +Section Ex6. Let ex6 : (1#1)+(1#1) == 2#1. ring. -Qed. +Defined. +End Ex6. +Section Ex7. Let ex7 : forall x : Q, x-x== 0. intro. ring. -Qed. +Defined. +End Ex7. +Section Ex8. Let ex8 : forall x : Q, x^1 == x. intro. ring. -Qed. +Defined. +End Ex8. +Section Ex9. Let ex9 : forall x : Q, x^0 == 1. intro. ring. -Qed. +Defined. +End Ex9. +Section Ex10. Let ex10 : forall x y : Q, ~(y==0) -> (x/y)*y == x. -intros. -field. -auto. -Qed. + intros. + field. + auto. +Defined. +End Ex10. End Examples. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 0cf90e7e441f..871e533e7ca4 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -719,7 +719,7 @@ Implicit Type l : list A. Let adapt f n := let m := f (S n) in if le_lt_dec m (f 0) then m else pred m. -Let adapt_injective f : Injective f -> Injective (adapt f). +Local Definition adapt_injective f : Injective f -> Injective (adapt f). Proof. unfold adapt. intros Hf x y EQ. destruct le_lt_dec as [LE|LT]; destruct le_lt_dec as [LE'|LT']. @@ -736,9 +736,9 @@ Proof. elim (proj1 (Nat.lt_nge _ _) LT LT'). - apply eq_add_S, Hf. now rewrite <- (Nat.lt_succ_pred _ _ LT), <- (Nat.lt_succ_pred _ _ LT'), EQ. -Qed. +Defined. -Let adapt_ok a l1 l2 f : Injective f -> length l1 = f 0 -> +Local Definition adapt_ok a l1 l2 f : Injective f -> length l1 = f 0 -> forall n, nth_error (l1++a::l2) (f (S n)) = nth_error (l1++l2) (adapt f n). Proof. unfold adapt. intros Hf E n. @@ -754,7 +754,7 @@ Proof. apply Nat.lt_succ_r; assumption. + apply Nat.lt_succ_r; assumption. + apply Nat.lt_le_incl; assumption. -Qed. +Defined. Lemma Permutation_nth_error l l' : Permutation l l' <-> diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v index ec2f9a4dcf41..a0d6931e7d7a 100644 --- a/theories/ZArith/Wf_Z.v +++ b/theories/ZArith/Wf_Z.v @@ -91,11 +91,11 @@ Section Efficient_Rec. Let R (a b:Z) := 0 <= a /\ a < b. - Let R_wf : well_founded R. + Local Definition R_wf : well_founded R. Proof. apply well_founded_lt_compat with Z.to_nat. intros x y (Hx,H). apply Z2Nat.inj_lt; Z.order. - Qed. + Defined. Lemma natlike_rec2 : forall P:Z -> Type, diff --git a/vernac/declare.ml b/vernac/declare.ml index d257cf74091f..80771341e551 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -483,6 +483,12 @@ let objVariable : Id.t Libobject.Dyn.tag = let inVariable v = Libobject.Dyn.Easy.inj v objVariable +let warn_opaque_let = CWarnings.create ~name:"opaque-let" ~category:"fragile" + Pp.(fun name -> + Id.print name ++ + strbrk " is declared opaque but this is not fully respected" ++ + strbrk " inside the section and not at all outside the section.") + let declare_variable_core ~name ~kind d = (* Variables are distinguished by only short names *) if Decls.variable_exists name then @@ -516,7 +522,9 @@ let declare_variable_core ~name ~kind d = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (name, se) in - Glob_term.Explicit, de.proof_entry_opaque, de.proof_entry_universes + let opaque = de.proof_entry_opaque in + let () = if opaque then warn_opaque_let name in + Glob_term.Explicit, opaque, de.proof_entry_universes in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); Decls.(add_variable_data name {opaque;kind});