Making Theorem with more flexible + code cleanup

dev/ci/user-overlays/18743-herbelin-master+more-flexible-theorem-with.sh

@@ -0,0 +1 @@
+overlay equations https://github.com/herbelin/Coq-Equations main+adapt+coq-pr18743-more-flexible-theorem-with 18743 master+more-flexible-theorem-with

doc/changelog/02-specification-language/18743-master+more-flexible-theorem-with.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  Mutually-proved theorems with statements in different coinductive
+  types now supported
+  (`#18743 <https://github.com/coq/coq/pull/18743>`_,
+  by Hugo Herbelin).

engine/eConstr.mli

@@ -426,7 +426,7 @@ end
 
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
-val push_rec_types : (t, t, ERelevance.t) Constr.prec_declaration -> env -> env
+val push_rec_types : rec_declaration -> env -> env
 
 val push_named : named_declaration -> env -> env
 val push_named_context : named_context -> env -> env

pretyping/pretyping.ml

@@ -70,34 +70,51 @@ open Inductiveops
 
 (************************************************************************)
 
-(* An auxiliary function for searching for fixpoint guard indexes *)
+(* An auxiliary function for searching for fixpoint guard indices *)
 
-exception Found of int array
+(* Tells the possible indices liable to guard a fixpoint *)
+type possible_fix_indices = int list list
+
+(* Tells if possibly a cofixpoint or a fixpoint over the given list of possible indices *)
+type possible_guard = {
+  possibly_cofix : bool;
+  possible_fix_indices : possible_fix_indices;
+} (* Note: if no fix indices are given, it has to be a cofix *)
+
+exception Found of int array option
 
 let nf_fix sigma (nas, cs, ts) =
   let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
   (Array.map EConstr.Unsafe.to_binder_annot nas, Array.map inj cs, Array.map inj ts)
 
-let search_guard ?loc ?evars env possible_indexes fixdefs =
-  (* Standard situation with only one possibility for each fix. *)
-  (* We treat it separately in order to get proper error msg. *)
+let search_guard ?loc ?evars env {possibly_cofix; possible_fix_indices} fixdefs =
   let is_singleton = function [_] -> true | _ -> false in
-  if List.for_all is_singleton possible_indexes then
-    let indexes = Array.of_list (List.map List.hd possible_indexes) in
-    let fix = ((indexes, 0),fixdefs) in
-    (try check_fix ?evars env fix
-     with reraise ->
-       let (e, info) = Exninfo.capture reraise in
-       let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
-       Exninfo.iraise (e, info));
-    indexes
+  let one_fix_possibility = List.for_all is_singleton possible_fix_indices in
+  if one_fix_possibility && not possibly_cofix then
+    let indexes = Array.of_list (List.map List.hd possible_fix_indices) in
+    let fix = ((indexes, 0), fixdefs) in
+    try let () = check_fix ?evars env fix in Some indexes
+    with reraise ->
+      let (e, info) = Exninfo.capture reraise in
+      let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
+      Exninfo.iraise (e, info)
   else
+    let zero_fix_possibility = List.for_all List.is_empty possible_fix_indices in
+    if zero_fix_possibility && possibly_cofix then
+      (* Maybe can we skip this check since it will be done in the kernel again *)
+      let cofix = (0, fixdefs) in
+      try let () = check_cofix ?evars env cofix in None
+      with reraise ->
+        let (e, info) = Exninfo.capture reraise in
+        let info = Option.cata (fun loc -> Loc.add_loc info loc) info loc in
+        Exninfo.iraise (e, info)
+    else
     (* we now search recursively among all combinations *)
-    let combinations = List.combinations possible_indexes in
-    if List.is_empty combinations then
-      user_err ?loc (Pp.str "A fixpoint needs at least one parameter.");
-    (try
-       List.iter
+    let combinations = List.combinations possible_fix_indices in
+    let flags = { (typing_flags env) with Declarations.check_guarded = true } in
+    let env = Environ.set_typing_flags flags env in
+    try
+       let () = List.iter
          (fun l ->
             let indexes = Array.of_list l in
             let fix = ((indexes, 0),fixdefs) in
@@ -108,14 +125,20 @@ let search_guard ?loc ?evars env possible_indexes fixdefs =
                error when totality is assumed but the strutural argument is
                not specified. *)
             try
-              let flags = { (typing_flags env) with Declarations.check_guarded = true } in
-              let env = Environ.set_typing_flags flags env in
-              check_fix ?evars env fix; raise (Found indexes)
+              let () = check_fix ?evars env fix in raise (Found (Some indexes))
             with TypeError _ -> ())
-          combinations;
+          combinations in
+       let () =
+         if possibly_cofix then
+           (* Maybe can we skip this check since it will be done in the kernel again *)
+           try let () = check_cofix env (0, fixdefs) in raise (Found None)
+           with TypeError _ -> () in
        let errmsg = "Cannot guess decreasing argument of fix." in
-         user_err ?loc (Pp.str errmsg)
-     with Found indexes -> indexes)
+       user_err ?loc (Pp.str errmsg)
+     with Found indexes -> indexes
+
+let search_fix_guard ?loc ?evars env possible_fix_indices fixdefs =
+  Option.get (search_guard ?loc ?evars env {possibly_cofix=false; possible_fix_indices} fixdefs)
 
 let esearch_guard ?loc env sigma indexes fix =
   (* not sure if we still need to nf_fix when calling search_guard with ~evars
@@ -128,6 +151,9 @@ let esearch_guard ?loc env sigma indexes fix =
   with TypeError (env,err) ->
     raise (PretypeError (env,sigma,TypingError (of_type_error err)))
 
+let esearch_fix_guard ?loc env sigma possible_fix_indices fix =
+  Option.get (esearch_guard ?loc env sigma {possibly_cofix=false; possible_fix_indices} fix)
+
 (* To force universe name declaration before use *)
 
 let { Goptions.get = is_strict_universe_declarations } =
@@ -844,15 +870,15 @@ struct
                  but doing it properly involves delta-reduction, and it finally
                  doesn't seem worth the effort (except for huge mutual
                  fixpoints ?) *)
-          let possible_indexes =
+          let possible_fix_indices =
             Array.to_list (Array.mapi
                              (fun i annot -> match annot with
                              | Some n -> [n]
                              | None -> List.interval 0 (Context.Rel.nhyps ctxtv.(i) - 1))
            vn)
           in
           let fixdecls = (names,ftys,fdefs) in
-          let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in
+          let indexes = esearch_fix_guard ?loc !!env sigma possible_fix_indices fixdecls in
           make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
         | GCoFix i ->
           let fixdecls = (names,ftys,fdefs) in

pretyping/pretyping.mli

@@ -30,13 +30,31 @@ val get_bidirectionality_hint : GlobRef.t -> int option
 
 val clear_bidirectionality_hint : GlobRef.t -> unit
 
-(** An auxiliary function for searching for fixpoint guard indexes *)
+(** An auxiliary function for searching for fixpoint guard indices *)
+
+(* Tells the possible indices liable to guard a fixpoint *)
+type possible_fix_indices = int list list
+
+(* Tells if possibly a cofixpoint or a fixpoint over the given list of possible indices *)
+type possible_guard = {
+  possibly_cofix : bool;
+  possible_fix_indices : possible_fix_indices;
+} (* Note: if no fix indices are given, it has to be a cofix *)
 
 val search_guard :
-  ?loc:Loc.t -> ?evars:CClosure.evar_handler -> env -> int list list -> Constr.rec_declaration -> int array
+  ?loc:Loc.t -> ?evars:CClosure.evar_handler -> env ->
+  possible_guard -> Constr.rec_declaration -> int array option
+
+val search_fix_guard : (* For Fixpoints only *)
+  ?loc:Loc.t -> ?evars:CClosure.evar_handler -> env ->
+  possible_fix_indices -> Constr.rec_declaration -> int array
 
 val esearch_guard :
-  ?loc:Loc.t -> env -> evar_map -> int list list ->
+  ?loc:Loc.t -> env -> evar_map -> possible_guard ->
+  EConstr.rec_declaration -> int array option
+
+val esearch_fix_guard : (* For Fixpoints only *)
+  ?loc:Loc.t -> env -> evar_map -> possible_fix_indices ->
   EConstr.rec_declaration -> int array
 
 type typing_constraint =

tactics/tactics.ml

@@ -97,7 +97,6 @@ exception OneIntroPatternExpected
 exception KeepAndClearModifierOnlyForHypotheses
 exception FixpointOnNonInductiveType
 exception NotEnoughProducts
-exception FixpointSameMutualInductiveType
 exception AllMethodsInCoinductiveType
 exception ReplacementIllTyped of exn
 exception NotEnoughPremises
@@ -238,8 +237,6 @@ let tactic_interp_error_handler = function
       str "Cannot do a fixpoint on a non inductive type."
   | NotEnoughProducts ->
       str "Not enough products."
-  | FixpointSameMutualInductiveType ->
-      str "Fixpoints should be on the same mutual inductive declaration."
   | AllMethodsInCoinductiveType ->
       str "All methods must construct elements in coinductive types."
   | ReplacementIllTyped e ->
@@ -625,9 +622,7 @@ let rec mk_holes env sigma = function
 let rec check_mutind env sigma k cl = match EConstr.kind sigma (strip_outer_cast sigma cl) with
 | Prod (na, c1, b) ->
   if Int.equal k 1 then
-    try
-      let ((sp, _), u), _ = find_inductive env sigma c1 in
-      (sp, u)
+    try ignore (find_inductive env sigma c1)
     with Not_found -> error FixpointOnNonInductiveType
   else
     let open Context.Rel.Declaration in
@@ -642,7 +637,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.project gl in
   let concl = Proofview.Goal.concl gl in
-  let (sp, u) = check_mutind env sigma n concl in
+  let () = check_mutind env sigma n concl in
   let firsts, lasts = List.chop j rest in
   let all = firsts @ (f, n, concl) :: lasts in
   let all = List.map (fun (f, n, ar) ->
@@ -654,9 +649,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   | [] -> sign
   | (f, r, n, ar) :: oth ->
     let open Context.Named.Declaration in
-    let (sp', u')  = check_mutind env sigma n ar in
-    if not (QMutInd.equal env sp sp') then
-      error FixpointSameMutualInductiveType;
+    let ()  = check_mutind env sigma n ar in
     if mem_named_context_val f sign then
       error (IntroAlreadyDeclared f);
     mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth

test-suite/success/Fixpoint.v

@@ -564,3 +564,28 @@ match t with
 end.
 
 End Wish16040.
+
+Module TheoremWith.
+
+CoInductive Stream : Set := Cons : nat -> Stream -> Stream.
+
+(* Support for mutually recursive theorems in non-mutual types *)
+Theorem a : Stream with b : Stream.
+Proof.
+apply (Cons 0), b.
+apply (Cons 0), a.
+Defined.
+
+Theorem c (n:nat) : Stream with d (n:nat) : Stream. (* corecursive *)
+Proof.
+apply (Cons n), (d n).
+apply (Cons n), (c n).
+Defined.
+
+Theorem c' (n:nat) : Stream with d' (n:nat) : Stream. (* recursive *)
+Proof.
+destruct n as [|n']. apply a. apply (d' n').
+destruct n as [|n']. apply a. apply (c' n').
+Defined.
+
+End TheoremWith.

vernac/comFixpoint.ml

@@ -260,38 +260,36 @@ let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
   (fix,pl,uctx,info)
 
 let build_recthms ~indexes fixnames fixtypes fiximps =
-  let fix_kind, cofix = match indexes with
-    | Some indexes -> Decls.Fixpoint, false
-    | None -> Decls.CoFixpoint, true
+  let fix_kind, possible_guard = match indexes with
+    | Some possible_fix_indices -> Decls.Fixpoint, Pretyping.{possibly_cofix = false; possible_fix_indices}
+    | None -> Decls.CoFixpoint, Pretyping.{possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) fixtypes}
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
         let args = List.map Context.Rel.Declaration.get_name ctx in
         Declare.CInfo.make ~name ~typ ~args ~impargs ()
       ) fixnames fixtypes fiximps
   in
-  fix_kind, cofix, thms
+  fix_kind, possible_guard, thms
 
 let declare_fixpoint_interactive_generic ?indexes ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
-  let fix_kind, cofix, thms = build_recthms ~indexes fixnames fixtypes fiximps in
-  let indexes = Option.default [] indexes in
-  let init_terms = Some fixdefs in
+  let fix_kind, possible_guard, thms = build_recthms ~indexes fixnames fixtypes fiximps in
   let evd = Evd.from_ctx ctx in
   let info = Declare.Info.make ~poly ~scope ?clearbody ~kind:(Decls.IsDefinition fix_kind) ~udecl ?typing_flags ?user_warns ~ntns () in
-  Declare.Proof.start_mutual_with_initialization ~info
-    evd ~mutual_info:(cofix,indexes,init_terms) ~cinfo:thms ?using None
+    Declare.Proof.start_mutual_with_initialization ~info ~cinfo:thms
+      ~init_terms:fixdefs ~possible_guard ?using evd
 
 let declare_fixpoint_generic ?indexes ?scope ?clearbody ~poly ?typing_flags ?user_warns ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns =
   (* We shortcut the proof process *)
-  let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
+  let fix_kind, possible_guard, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in
   let fixdefs = List.map Option.get fixdefs in
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
   let info = Declare.Info.make ?scope ?clearbody ~kind:fix_kind ~poly ~udecl ?typing_flags ?user_warns ~ntns () in
   let cinfo = fixitems in
   let _ : GlobRef.t list =
     Declare.declare_mutually_recursive ~cinfo ~info ~opaque:false ~uctx
-      ~possible_indexes:indexes ~rec_declaration ?using ()
+      ~possible_guard ~rec_declaration ?using ()
   in
   ()
 

vernac/comProgramFixpoint.ml

@@ -216,8 +216,8 @@ let out_def = function
 let collect_evars_of_term evd c ty =
   Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty)
 
-let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fixkind fixl =
-  let cofix = fixkind = Declare.Obls.IsCoFixpoint in
+let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using kind fixl =
+  let cofix = kind = Decls.CoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     let env = Global.env () in
     let env = Environ.update_typing_flags ?typing_flags env in
@@ -243,36 +243,23 @@ let do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?
   let fiximps = List.map pi2 info in
   let fixdefs = List.map out_def fixdefs in
   let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
-  let () = if not cofix then begin
-      let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in
-      (* XXX: are we allowed to have evars here? *)
-      let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in
-      let fixdefs = List.map (EConstr.Vars.subst_vars evd (List.rev fixnames)) fixdefs in
-      let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in
-      let fixdecls =
-        Array.of_list (List.map2 (fun x r -> make_annot (Name x) (EConstr.ERelevance.kind evd r)) fixnames fixrs),
-        Array.of_list fixtypes,
-        Array.of_list fixdefs
-      in
-      let evars = Evd.evar_handler evd in
-      let indexes =
-        let env = Global.env () in
-        let env = Environ.update_typing_flags ?typing_flags env in
-        Pretyping.search_guard ~evars env possible_indexes fixdecls in
-      let env = Environ.update_typing_flags ?typing_flags env in
-      List.iteri (fun i _ ->
-          Inductive.check_fix ~evars env
-            ((indexes,i),fixdecls))
-        fixl
-  end in
-  let uctx = Evd.evar_universe_context evd in
-  let kind = match fixkind with
-  | Declare.Obls.IsFixpoint _ -> Decls.(IsDefinition Fixpoint)
-  | Declare.Obls.IsCoFixpoint -> Decls.(IsDefinition CoFixpoint)
+  let possible_guard =
+    if cofix then Pretyping.{possibly_cofix = true; possible_fix_indices = List.map (fun _ -> []) info}
+    else Pretyping.{possibly_cofix = false; possible_fix_indices = List.map ComFixpoint.compute_possible_guardness_evidences info} in
+  let () =
+    (* An early check of guardedness before working on the obligations *)
+    let fixdecls =
+      Array.of_list (List.map2 (fun x r -> make_annot (Name x) r) fixnames fixrs),
+      Array.of_list fixtypes,
+      Array.of_list fixdefs
+    in
+    ignore (Pretyping.esearch_guard env evd possible_guard fixdecls)
   in
+  let uctx = Evd.evar_universe_context evd in
+  let kind = Decls.(IsDefinition kind) in
   let ntns = List.map_append (fun { Vernacexpr.notations } -> List.map Metasyntax.prepare_where_notation notations ) fixl in
   let info = Declare.Info.make ~poly ~scope ?clearbody ~kind ~udecl ?typing_flags ?user_warns ~ntns () in
-  Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ?using fixkind
+  Declare.Obls.add_mutual_definitions ~pm ~info ~uctx ?using ~possible_guard defs
 
 let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
   let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
@@ -299,13 +286,13 @@ let do_fixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using l =
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
       let annots = List.map (fun fix ->
           Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in
-      let fixkind = Declare.Obls.IsFixpoint annots in
+      let kind = Decls.Fixpoint in
       let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in
-      do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fixkind l
+      do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using kind l
     | _, _ ->
       CErrors.user_err
         (str "Well-founded fixpoints not allowed in mutually recursive blocks.")
 
 let do_cofixpoint ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using fixl =
   let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
-  do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using Declare.Obls.IsCoFixpoint fixl
+  do_program_recursive ~pm ~scope ?clearbody ~poly ?typing_flags ?user_warns ?using Decls.CoFixpoint fixl