From 8a02738a47d7dcbf93967b5f8a46f1a0f50f3840 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 13:55:23 +0200
Subject: Slight modification of the partial-order algorithm so that it does
 not remove itself in the set of elements bigger than it if it is indeed the
 case.

This does not impact the warning issued when the recursivity is not
mutual but this produces a result consistent with the unary case when
the order is reflexive (i.e. results of the form (x,Inr[x,y]) happens
also in the mutual case to indicate a cycle x<=y<=x while before we
had results of the form (x,Inr[x]) only in the unary case). I.e.:

Before:
(x,[y]),(y,[x]) -> (x,Inr[]),(y,Inl x)
(x,[x]) -> (x,Inr[x])

Now:
(x,[y]),(y,[x]) -> (x,Inr[x]),(y,Inl x)
(x,[x]) -> (x,Inr[x])
---
 vernac/comFixpoint.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index e4fa212a23..4c7a706fdb 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
-- 
cgit v1.2.3


From a6b2029042ae2e5f51fcae6d922fc8437ae1ff13 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 12:58:05 +0200
Subject: Warn when a (co)fixpoint is not truly recursive.

---
 plugins/funind/gen_principle.ml |  2 +-
 vernac/comFixpoint.ml           | 19 ++++++++++++++-----
 vernac/comFixpoint.mli          |  3 ++-
 3 files changed, 17 insertions(+), 7 deletions(-)

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 55e659d487..600e11afc4 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/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 4c7a706fdb..d3c1d2e767 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -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 *
-- 
cgit v1.2.3


From df8df4637dfb4106854554cc2ac94b4fdd565e80 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 13:00:09 +0200
Subject: Fixing #11903: Fixpoints not truly recursive in standard library.

There was also a non truly recursive in the doc.
---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 +-
 theories/FSets/FMapAVL.v                             | 4 ++--
 theories/Init/Decimal.v                              | 2 +-
 theories/NArith/BinNatDef.v                          | 4 ++--
 theories/ZArith/BinIntDef.v                          | 2 +-
 theories/extraction/ExtrOcamlBigIntConv.v            | 4 ++--
 theories/extraction/ExtrOcamlIntConv.v               | 4 ++--
 7 files changed, 11 insertions(+), 11 deletions(-)

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/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
-- 
cgit v1.2.3


From 653a06b843e380927b93e325dcbe1c339810406f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 13:24:53 +0200
Subject: Changing fixpoint message "decreasing" -> "guarded".

This is to be compatible with the possibility of having non truly
recursive fixpoints.
---
 vernac/declare.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 357f58feea..f9b8019b45 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 ()))
-- 
cgit v1.2.3


From 2d8cbfd83c72f81284ea0fc85b39515d4e8fe05e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 19 Apr 2020 13:28:36 +0200
Subject: Testing different combinations of non truly recursive (co)fixpoints.

---
 test-suite/output/Fixpoint.out | 24 ++++++++++++++++++++++++
 test-suite/output/Fixpoint.v   | 38 +++++++++++++++++++++++++++++++++++---
 2 files changed, 59 insertions(+), 3 deletions(-)

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.
-- 
cgit v1.2.3


From d14a43f7acb982b054185545b5c02820244fc240 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Apr 2020 18:17:49 +0200
Subject: Adding change logs for PR #12121.

Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>

Also including feedback from Enrico Tassi.
---
 .../12121-master+fix11903-warn-non-truly-fixpoint.rst                | 5 +++++
 .../12121-master+fix11903-warn-non-truly-fixpoint.rst                | 5 +++++
 2 files changed, 10 insertions(+)
 create mode 100644 doc/changelog/02-specification-language/12121-master+fix11903-warn-non-truly-fixpoint.rst
 create mode 100644 doc/changelog/10-standard-library/12121-master+fix11903-warn-non-truly-fixpoint.rst

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>`_).
-- 
cgit v1.2.3