Fix issue Failure to prove functional induction #577

src/principles.ml

@@ -686,7 +686,7 @@ let subst_rec env evd cutprob s lhs =
     (compose_subst env ~sigma:evd subst lhs) cutprob
   in subst, csubst
 
-let subst_protos s gr =
+let subst_protos info s gr =
   let open Context.Rel.Declaration in
   let modified = ref false in
   let env = Global.env () in
@@ -721,17 +721,16 @@ let subst_protos s gr =
   if !modified then
     (* let ty = Reductionops.nf_beta env sigma ty in *)
     (equations_debug Pp.(fun () -> str"Fixed hint " ++ Printer.pr_econstr_env env sigma term);
-     let sigma, _ = Typing.type_of env sigma term in
-     let sigma = Evd.minimize_universes sigma in
-     Hints.hint_constr (Evarutil.nf_evar sigma term, Some (Evd.sort_context_set sigma)))
+     let id = Nameops.add_suffix (Nametab.basename_of_global gr) "_hint" in
+     let cst, (_sigma, _ec) = Equations_common.declare_constant id term None ~poly:(is_polymorphic info) ~kind:(Decls.IsDefinition info.decl_kind) sigma in
+     Hints.hint_globref (GlobRef.ConstRef cst))
   else Hints.hint_globref gr
   [@@ocaml.warning "-3"]
 
 let declare_wf_obligations s info =
   let make_resolve gr =
     equations_debug Pp.(fun () -> str"Declaring wf obligation " ++ Printer.pr_global gr);
-    (Hints.empty_hint_info, true,
-     subst_protos s gr)
+    (Hints.empty_hint_info, true, subst_protos info s gr)
   in
   let dbname = Principles_proofs.wf_obligations_base info in
   let locality = if Global.sections_are_opened () then Hints.Local else Hints.SuperGlobal in

src/principles.mli

@@ -19,7 +19,7 @@ val is_applied_to_structarg : Names.Id.t -> Syntax.rec_type -> int -> bool optio
 
 val smash_ctx_map : Environ.env -> Evd.evar_map -> Context_map.context_map -> Context_map.context_map * EConstr.t list
 
-val subst_protos: Names.Constant.t list -> Names.GlobRef.t -> Hints.hint_term
+val subst_protos: Splitting.term_info -> Names.Constant.t list -> Names.GlobRef.t -> Hints.hint_term
 
 val find_rec_call : Syntax.rec_type ->
            Evd.evar_map ->

src/splitting.ml

@@ -1174,8 +1174,7 @@ let solve_equations_obligations_program ~pm flags recids loc i sigma hook =
       if EConstr.isRef !evd hd then
         (if !Equations_common.debug then
            Feedback.msg_debug
-             (str"mapping obligation to " ++ Printer.pr_econstr_env env !evd t ++
-              Prettyp.print_about env !evd (CAst.make (Constrexpr.AN (Libnames.qualid_of_ident id))) None);
+             (str"mapping obligation to " ++ Printer.pr_econstr_env env !evd t ++ Id.print id);
          let cst, i = EConstr.destConst !evd hd in
          let ctx = Environ.constant_context (Global.env ()) cst in
          let ctx = gather_fresh_context !evd (EConstr.EInstance.kind sigma i) ctx in

test-suite/_CoqProject

@@ -76,6 +76,7 @@ issues/issue321.v
 issues/issue399.v
 issues/issue499.v
 issues/issue500.v
+issues/issue577.v
 issues/coq_pr_16995.v
 eqdec_error.v
 noconf_simplify.v

test-suite/issues/issue577.v

@@ -0,0 +1,108 @@
+From Coq Require Import List String.
+From Equations Require Import Equations.
+
+Module A.
+Section test.
+  Set Equations Transparent.
+  Set Universe Polymorphism.
+  Import Sigma_Notations.
+
+  Open Scope nat.
+
+  Inductive term := T  | L (t: list term).
+
+  Definition env_ty :Type := string -> option (list string *  term).
+
+  Inductive ty : forall (A B  : Type), (A -> B -> Type) -> Type :=
+    | f_a : ty env_ty term (fun  _ _ => nat)
+    | f_b : ty env_ty  string (fun  _ _ =>  nat)
+    .
+
+    Derive Signature NoConfusion for ty.
+
+    Fixpoint T_size (t:term) :nat := match t with
+    | T => 0
+    | L ts => List.fold_left (fun acc t => acc + (T_size t)) ts 1
+    end.
+
+    Equations measure : (Σ A B P (_ : A) (_ : B) , ty A B P) -> nat :=
+        | (_,_,_, _,t,f_a) => T_size t
+        | (_,_,_,_,_,f_b)  =>  0
+
+.
+Definition rel := Program.Wf.MR lt measure.
+
+#[global] Instance: WellFounded rel.
+Proof.
+  red. apply Wf.measure_wf. apply Wf_nat.lt_wf.
+Defined.
+
+Definition pack {A B } {P} (x1 : A) (x2 : B) (t : ty A B P) :=
+     (A,B,P, x1, x2, t) : (Σ A B  P (_ : A) (_ : B) , ty A B  P).
+
+End test.
+Equations mutrecf {A B} {P} (t : ty A B P) (a : A) (b : B)  : P a b   by wf (pack a b t) rel :=
+| f_a , _, _  => 0
+| f_b,env,fname with env fname =>
+    {
+        | Some (_,t) =>
+            let heretofail := 0 in
+            let reccall := mutrecf f_a env t in
+            0
+        | None =>  0
+    }
+.
+
+Solve Obligations with intros; red ;red ; cbn ; auto with arith.
+Parameter h :forall b, (T_size b < 0)%nat.
+Next Obligation. red. red. cbn. apply h. Qed.
+End A.
+
+Module B.
+Section todo.
+  Set Equations Transparent.
+  Set Universe Polymorphism.
+
+  Definition M (T : Type) : Type := nat -> T * nat.
+
+  Definition bind {A B : Type} (m : M A) (f : A -> M B) : M B :=
+      fun c =>  let (a, c') := m c in f a c'.
+
+  Inductive termA := T (p:termB) with termB := P.
+
+  Inductive ty : forall (A  : Type), (A  -> Type) -> Type :=
+  | f_a : ty  termB (fun _  => @M nat)
+  | f_b : ty  termA (fun _ => @M nat)
+  .
+  Derive Signature NoConfusion for ty.
+  Import Sigma_Notations.
+
+  Equations measure : (Σ A P (_ : A) , ty A P) -> nat :=
+      | (_,_,p,f_a) => 0
+      | (_,_,t,f_b) => 1
+  .
+
+  Definition rel := Program.Wf.MR lt measure.
+  #[global] Instance: WellFounded rel.
+  Proof.
+      red. apply Wf.measure_wf. apply Wf_nat.lt_wf.
+  Defined.
+
+  Definition pack {A } {P} (x1 : A)  (t : ty A P) :=
+       (A,P, x1, t) : (Σ A  P (_ : A) , ty A  P).
+End todo.
+
+Equations mutrec {A} {P} (t : ty A  P) (x: A) : P x  by wf (pack x t) rel :=
+
+| f_a , _ => fun _ => (0,0)%nat
+| f_b ,T p =>
+    bind (fun _ => (0,0%nat)) (fun c =>
+        let heretofail := 0 in
+        bind (mutrec f_a p) (fun _ =>
+            fun _ => (0,0)%nat
+        )
+    )
+.
+Solve Obligations with red ;red ; cbn ; auto with arith.
+About mutrec_elim.
+End B.