Modify name of induction scheme hypotheses

dev/ci/user-overlays/20813-dhalilov-better-names-for-induction-principle-cases.sh

@@ -0,0 +1,3 @@
+overlay hott https://github.com/dhalilov/HoTT better-names-for-induction-principle-cases 20813
+
+overlay stdlib https://github.com/dhalilov/stdlib better-names-for-induction-principle-cases 20813

doc/changelog/14-misc/20813-better-names-for-induction-principle-cases-Changed.rst

@@ -0,0 +1,4 @@
+- **Changed:**
+  Hypotheses of generated induction schemes use the constructor name instead of `f`, `f0`, etc
+  (`#20813 <https://github.com/rocq-prover/rocq/pull/20813>`_,
+  by Dario Halilovic).

pretyping/indrec.ml

@@ -203,8 +203,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib, mip) s =
     else
       let cs = lift_constructor (k+1) constrs.(k) in
       let t = build_branch_type !!env sigma dep (mkRel (k+1)) cs in
-      let namef = make_name env "f" relevance in
-      let decl = LocalAssum (namef, t) in
+      let branch_name = make_annot (Name cs.cs_name) relevance in
+      let decl = LocalAssum (branch_name, t) in
       get_branches (RelEnv.push_rel decl env) (k + 1) (decl :: accu)
   in
 
@@ -589,9 +589,9 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u =
                   true dep !!env !evdref (vargs,depPvec,i+j) indi cs recarg
               in
               let r_0 = Retyping.relevance_of_sort sfam in
-              let namef = make_name env "f" r_0 in
-                mkLambda (namef, p_0,
-                  (onerec (RelEnv.push_rel (LocalAssum (namef,p_0)) env)) (j+1))
+              let case_name = make_annot (Name cs.cs_name) r_0 in
+                mkLambda (case_name, p_0,
+                  (onerec (RelEnv.push_rel (LocalAssum (case_name,p_0)) env)) (j+1))
           in onerec env 0
       | [] ->
           makefix i listdepkind

pretyping/inductiveops.ml

@@ -376,6 +376,7 @@ let make_case_info env ind style =
 (*s Useful functions *)
 
 type constructor_summary = {
+  cs_name : Id.t;
   cs_cstr : constructor puniverses;
   cs_params : constr list;
   cs_nargs : int;
@@ -384,6 +385,7 @@ type constructor_summary = {
 }
 
 let lift_constructor n cs = {
+  cs_name = cs.cs_name;
   cs_cstr = cs.cs_cstr;
   cs_params = List.map (lift n) cs.cs_params;
   cs_nargs = cs.cs_nargs;
@@ -412,7 +414,9 @@ let get_constructor ((ind,u),mib,mip,params) j =
   let (args,ccl) = Term.decompose_prod_decls typi in
   let (_,allargs) = Constr.decompose_app_list ccl in
   let vargs = List.skipn (List.length params) allargs in
-  { cs_cstr = (ith_constructor_of_inductive ind j,u);
+  let name = mip.mind_consnames.(j-1) in
+  { cs_name = name;
+    cs_cstr = (ith_constructor_of_inductive ind j,u);
     cs_params = params;
     cs_nargs = Context.Rel.length args;
     cs_args = EConstr.of_rel_context args;

pretyping/inductiveops.mli

@@ -158,6 +158,7 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 (** Extract information from an inductive family *)
 
 type constructor_summary = {
+  cs_name : Id.t; (* name of the constructor *)
   cs_cstr : constructor puniverses;    (* internal name of the constructor plus universes *)
   cs_params : constr list;   (* parameters of the constructor in current ctx *)
   cs_nargs : int;            (* length of arguments signature (letin included) *)

test-suite/output/Cases.out

@@ -1,13 +1,13 @@
 t_rect =
-fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
+fun (P : t -> Type) (k : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
 fix F (t : t) : P t :=
   match t as t0 return (P t0) with
-  | k _ x0 => f x0 (F x0)
+  | k _ x0 => k x0 (F x0)
   end
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
-Arguments t_rect (P f)%_function_scope t
+Arguments t_rect (P k)%_function_scope t
      = fun d : TT => match d with
                      | {| f3 := b |} => b
                      end

test-suite/output/PrintInfos.out

@@ -127,7 +127,7 @@ Alias.eq_ind :
 forall [A : Type] (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y
 
 Alias.eq_ind is not universe polymorphic
-Arguments Alias.eq_ind [A]%_type_scope x P%_function_scope f y e
+Arguments Alias.eq_ind [A]%_type_scope x P%_function_scope eq_refl y e
   (where some original arguments have been renamed)
 Alias.eq_ind is transparent
 Expands to: Constant PrintInfos.Alias.eq_ind (syntactically equal to

test-suite/output/PrintMatch.out

@@ -1,27 +1,27 @@
 eqT_rect@{u u0} =
 fun (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0})
-  (f : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) =>
+  (reflT : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) =>
 match e :> eqT@{u} a _ as e0 in (eqT _ a1) return (P a1 e0) with
-| reflT _ => f
+| reflT _ => reflT
 end
      : forall (A : Type@{u}) (a : A)
          (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}),
        P a (reflT@{u} a) -> forall (a0 : A) (e : eqT@{u} a a0), P a0 e
 (* u u0 |=  *)
 
-Arguments eqT_rect A%_type_scope a P%_function_scope f a0 e
+Arguments eqT_rect A%_type_scope a P%_function_scope reflT a0 e
 seq_rect =
 fun (A : Type@{seq_rect.u1}) (a : A)
   (P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}) 
-  (f : P a (srefl a)) (a0 : A) (s : seq a a0) =>
+  (srefl : P a (srefl a)) (a0 : A) (s : seq a a0) =>
 match s :> seq a a0 as s0 in (seq _ a1) return (P a1 s0) with
-| srefl _ => f
+| srefl _ => srefl
 end
      : forall (A : Type@{seq_rect.u1}) (a : A)
          (P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}),
        P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s
 
-Arguments seq_rect A%_type_scope a P%_function_scope f a0 s
+Arguments seq_rect A%_type_scope a P%_function_scope srefl a0 s
 eq_sym =
 fun (A : Type) (x y : A) (H : @eq A x y) =>
 match H in (@eq _ _ a) return (@eq A a x) with