Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpoints

Ack-by: Zimmi48
Reviewed-by: ppedrot

15 files changed, 100 insertions, 24 deletions

diff --git a/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
new file mode 100644
index 0000000000..d69a94205f
--- /dev/null
+++ b/doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
@@ -0,0 +1,5 @@
+- **Added:**
+  New warning on using :cmd:`Fixpoint` or :cmd:`CoFixpoint` for
+  definitions which are not recursive
+  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
+  by Hugo Herbelin)
diff --git a/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst b/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst
new file mode 100644
index 0000000000..f22fff0736
--- /dev/null
+++ b/doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  :cmd:`Fixpoint`\s of the standard library without a recursive call turned
+  into ordinary :cmd:`Definition`\s
+  (`#12121 <https://github.com/coq/coq/pull/12121>`_,
+  by Hugo Herbelin; fixes `#11903 <https://github.com/coq/coq/pull/11903>`_).
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 28c5359a04..4be18ccda9 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -286,7 +286,7 @@ example, the null and all list function(al)s can be defined as follows:
    .. coqtop:: all
 
       Variable d: Set.
-      Fixpoint null (s : list d) :=
+      Definition null (s : list d) :=
         if s is nil then true else false.
       Variable a : d -> bool.
       Fixpoint all (s : list d) : bool :=
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 07f578d2a8..c53dcc7edd 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -159,7 +159,7 @@ let recompute_binder_list fixpoint_exprl =
       fixpoint_exprl
   in
   let (_, _, _, typel), _, ctx, _ =
-    ComFixpoint.interp_fixpoint ~cofix:false fixl
+    ComFixpoint.interp_fixpoint ~check_recursivity:false ~cofix:false fixl
   in
   let constr_expr_typel =
     with_full_print
diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 60bc9cbf55..ff7918b4e6 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -12,3 +12,27 @@ let fix f (m : nat) : nat := match m with
 Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1)
      = cofix inf : Inf := {| projS := inf |}
      : Inf
+File "stdin", line 57, characters 0-51:
+Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
+File "stdin", line 60, characters 0-103:
+Warning: Not a fully mutually defined fixpoint
+(k1 depends on k2 but not conversely).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 62, characters 0-106:
+Warning: Not a fully mutually defined fixpoint
+(l2 and l1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 64, characters 0-103:
+Warning: Not a fully mutually defined fixpoint
+(m2 and m1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
+File "stdin", line 72, characters 0-25:
+Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
+File "stdin", line 75, characters 0-48:
+Warning: Not a fully mutually defined fixpoint
+(a2 and a1 are not mutually dependent).
+Well-foundedness check may fail unexpectedly.
+ [non-full-mutual,fixpoints]
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 398528de72..26c276b68b 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,39 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   lia.
 Qed.
 
-CoInductive Inf := S { projS : Inf }.
-Definition expand_Inf (x : Inf) := S (projS x).
-CoFixpoint inf := S inf.
+CoInductive Inf := IS { projS : Inf }.
+Definition expand_Inf (x : Inf) := IS (projS x).
+CoFixpoint inf := IS inf.
 Eval compute in inf.
+
+Module Recursivity.
+
+Open Scope nat_scope.
+
+Fixpoint f n := match n with 0 => 0 | S n => f n end.
+Fixpoint g n := match n with 0 => 0 | S n => n end.
+Fixpoint h1 n := match n with 0 => 0 | S n => h2 n end
+with h2 n := match n with 0 => 0 | S n => h1 n end.
+Fixpoint k1 n := match n with 0 => 0 | S n => k2 n end
+with k2 n := match n with 0 => 0 | S n => n end.
+Fixpoint l1 n := match n with 0 => 0 | S n => l1 n end
+with l2 n := match n with 0 => 0 | S n => l2 n end.
+Fixpoint m1 n := match n with 0 => 0 | S n => m1 n end
+with m2 n := match n with 0 => 0 | S n => n end.
+(* Why not to allow this definition ?
+Fixpoint h1' n := match n with 0 => 0 | S n => h2' n end
+with h2' n := h1' n.
+*)
+CoInductive S := cons : nat -> S -> S.
+CoFixpoint c := cons 0 c.
+CoFixpoint d := cons 0 c.
+CoFixpoint e1 := cons 0 e2
+with e2 := cons 1 e1.
+CoFixpoint a1 := cons 0 a1
+with a2 := cons 1 a2.
+(* Why not to allow this definition ?
+CoFixpoint b1 := cons 0 b2
+with b2 := b1.
+*)
+
+End Recursivity.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index f78c0ecc1e..ad0124db6d 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -123,7 +123,7 @@ Definition create l x e r :=
 
 Definition assert_false := create.
 
-Fixpoint bal l x d r :=
+Definition bal l x d r :=
   let hl := height l in
   let hr := height r in
   if gt_le_dec hl (hr+2) then
@@ -191,7 +191,7 @@ Fixpoint remove_min l x d r : t*(key*elt) :=
   [|height t1 - height t2| <= 2].
 *)
 
-Fixpoint merge s1 s2 :=  match s1,s2 with
+Definition merge s1 s2 :=  match s1,s2 with
   | Leaf, _ => s2
   | _, Leaf => s1
   | _, Node l2 x2 d2 r2 h2 =>
diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v
index 855db8bc3f..2a84456500 100644
--- a/theories/Init/Decimal.v
+++ b/theories/Init/Decimal.v
@@ -179,7 +179,7 @@ Definition del_head_int n d :=
 (** [del_tail n d] removes [n] digits at end of [d]
     or returns [zero] if [d] has less than [n] digits. *)
 
-Fixpoint del_tail n d := rev (del_head n (rev d)).
+Definition del_tail n d := rev (del_head n (rev d)).
 
 Definition del_tail_int n d :=
   match d with
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index ea53618acb..04685cc3eb 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -126,7 +126,7 @@ Infix "?=" := compare (at level 70, no associativity) : N_scope.
 
 (** Boolean equality and comparison *)
 
-Fixpoint eqb n m :=
+Definition eqb n m :=
   match n, m with
     | 0, 0 => true
     | pos p, pos q => Pos.eqb p q
@@ -313,7 +313,7 @@ Definition land n m :=
 
 (** Logical [diff] *)
 
-Fixpoint ldiff n m :=
+Definition ldiff n m :=
  match n, m with
   | 0, _ => 0
   | _, 0 => n
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 55b9ec4a44..c05ed9ebf4 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -208,7 +208,7 @@ Definition gtb x y :=
     | _ => false
   end.
 
-Fixpoint eqb x y :=
+Definition eqb x y :=
   match x, y with
     | 0, 0 => true
     | pos p, pos q => Pos.eqb p q
diff --git a/theories/extraction/ExtrOcamlBigIntConv.v b/theories/extraction/ExtrOcamlBigIntConv.v
index 7740bb41d9..29bd732c78 100644
--- a/theories/extraction/ExtrOcamlBigIntConv.v
+++ b/theories/extraction/ExtrOcamlBigIntConv.v
@@ -45,14 +45,14 @@ Fixpoint bigint_of_pos p :=
   | xI p => bigint_succ (bigint_twice (bigint_of_pos p))
  end.
 
-Fixpoint bigint_of_z z :=
+Definition bigint_of_z z :=
  match z with
   | Z0 => bigint_zero
   | Zpos p => bigint_of_pos p
   | Zneg p => bigint_opp (bigint_of_pos p)
  end.
 
-Fixpoint bigint_of_n n :=
+Definition bigint_of_n n :=
  match n with
   | N0 => bigint_zero
   | Npos p => bigint_of_pos p
diff --git a/theories/extraction/ExtrOcamlIntConv.v b/theories/extraction/ExtrOcamlIntConv.v
index a5be08ece4..d9c88defa5 100644
--- a/theories/extraction/ExtrOcamlIntConv.v
+++ b/theories/extraction/ExtrOcamlIntConv.v
@@ -42,14 +42,14 @@ Fixpoint int_of_pos p :=
   | xI p => int_succ (int_twice (int_of_pos p))
  end.
 
-Fixpoint int_of_z z :=
+Definition int_of_z z :=
  match z with
   | Z0 => int_zero
   | Zpos p => int_of_pos p
   | Zneg p => int_opp (int_of_pos p)
  end.
 
-Fixpoint int_of_n n :=
+Definition int_of_n n :=
  match n with
   | N0 => int_zero
   | Npos p => int_of_pos p
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index e4fa212a23..d3c1d2e767 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -53,7 +53,7 @@ let rec partial_order cmp = function
                     (z, Inr (List.add_set cmp x (List.remove cmp y zge)))
                   else
                     (z, Inr zge)) res in
-            browse ((y,Inl x)::res) xge' (List.union cmp xge (List.remove cmp x yge))
+            browse ((y,Inl x)::res) xge' (List.union cmp xge yge)
           else
             browse res (List.add_set cmp y (List.union cmp xge' yge)) xge
         with Not_found -> browse res (List.add_set cmp y xge') xge
@@ -82,16 +82,25 @@ let warn_non_full_mutual =
          (fun (x,xge,y,yge,isfix,rest) ->
           non_full_mutual_message x xge y yge isfix rest)
 
-let check_mutuality env evd isfix fixl =
+let warn_non_recursive =
+  CWarnings.create ~name:"non-recursive" ~category:"fixpoints"
+         (fun (x,isfix) ->
+          let k = if isfix then "fixpoint" else "cofixpoint" in
+          strbrk "Not a truly recursive " ++ str k ++ str ".")
+
+let check_true_recursivity env evd isfix fixl =
   let names = List.map fst fixl in
   let preorder =
     List.map (fun (id,def) ->
-      (id, List.filter (fun id' -> not (Id.equal id id') && Termops.occur_var env evd id' def) names))
+      (id, List.filter (fun id' -> Termops.occur_var env evd id' def) names))
       fixl in
   let po = partial_order Id.equal preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
     | (x,Inr xge)::(y,Inr yge)::rest ->
        warn_non_full_mutual (x,xge,y,yge,isfix,rest)
+    | _ ->
+  match po with
+    | [x,Inr []] -> warn_non_recursive (x,isfix)
     | _ -> ()
 
 let interp_fix_context ~program_mode ~cofix env sigma fix =
@@ -222,7 +231,7 @@ let interp_recursive ~program_mode ~cofix (fixl : 'a Vernacexpr.fix_expr_gen lis
 let check_recursive isfix env evd (fixnames,_,fixdefs,_) =
   if List.for_all Option.has_some fixdefs then begin
     let fixdefs = List.map Option.get fixdefs in
-    check_mutuality env evd isfix (List.combine fixnames fixdefs)
+    check_true_recursivity env evd isfix (List.combine fixnames fixdefs)
   end
 
 let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
@@ -232,12 +241,12 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
   Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
 
 (* XXX: Unify with interp_recursive  *)
-let interp_fixpoint ~cofix l :
+let interp_fixpoint ?(check_recursivity=true) ~cofix l :
   ( (Constr.t, Constr.types) recursive_preentry *
     UState.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
   let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
-  check_recursive true env evd fix;
+  if check_recursivity then check_recursive true env evd fix;
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a19b96f0f3..dcb61d38d9 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -58,7 +58,8 @@ val interp_recursive :
 (** Exported for Funind *)
 
 val interp_fixpoint
-  :  cofix:bool
+  :  ?check_recursivity:bool ->
+     cofix:bool
   -> lident option fix_expr_gen list
   -> (Constr.t, Constr.types) recursive_preentry *
      UState.universe_decl * UState.t *
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 95e573a671..f4636c5724 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -580,12 +580,12 @@ let fixpoint_message indexes l =
   | [] -> CErrors.anomaly (Pp.str "no recursive definition.")
   | [id] -> Id.print id ++ str " is recursively defined" ++
       (match indexes with
-         | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+         | Some [|i|] -> str " (guarded on "++pr_rank i++str " argument)"
          | _ -> mt ())
   | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
                   spc () ++ str "are recursively defined" ++
                   match indexes with
-                    | Some a -> spc () ++ str "(decreasing respectively on " ++
+                    | Some a -> spc () ++ str "(guarded respectively on " ++
                         prvect_with_sep pr_comma pr_rank a ++
                         str " arguments)"
                     | None -> mt ()))