Warn on Qed Let declaration

doc/sphinx/language/core/sections.rst

@@ -66,6 +66,13 @@ usable outside the section as shown in this :ref:`example <section_local_declara
    In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant
    for which the computational behavior is relevant.  See :ref:`proof-editing-mode`.
 
+.. warn:: @ident is declared opaque but this is not fully respected inside the section and not at all outside the section.
+
+   Terminating the proof for a :cmd:`Let` with :cmd:`Qed` with `Let` is not recommended.
+   The variable will appear to have no body inside proofs but the kernel will still use
+   the body when checking, and it will be treated the same as a
+   :cmd:`Defined` `Let` when the section is closed.
+
 .. cmd:: Context {+ @binder }
 
    Declare variables in the context of the current section, like :cmd:`Variable`,

test-suite/output/SuggestProofUsing.v

@@ -1,6 +1,7 @@
 Require Program.Tactics.
 
 Set Suggest Proof Using.
+Set Warnings "-opaque-let".
 
 Lemma nosec : nat. Proof. exact 0. Qed.
 

test-suite/output/UnivBinders.out

@@ -69,6 +69,9 @@ mono
 File "./output/UnivBinders.v", line 70, characters 0-52:
 The command has indeed failed with message:
 Universe uu already exists.
+File "./output/UnivBinders.v", line 78, characters 47-51:
+Warning: ff is declared opaque but this is not fully respected inside the
+section and not at all outside the section. [opaque-let,fragile]
 bobmorane =
 let tt := Type@{UnivBinders.32} in
 let ff := Type@{UnivBinders.34} in tt -> ff

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.

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.

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.

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.

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.

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.

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.

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 *)

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.
 

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' <->

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,

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});