Modify name of induction scheme hypotheses

Author: dhalilov

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) *)

proofs/clenv.ml

@@ -818,7 +818,7 @@ and mk_arggoals ~metas env sigma goalacc funty allargs =
 
 let treat_case env sigma ci lbrty accu =
   let open EConstr in
-  let fold (sigma, accu) (ctx, ty) =
+  let fold (sigma, accu) (name, ctx, ty) =
     let open Context.Rel.Declaration in
     let brctx = Array.of_list (List.rev_map get_annot ctx) in
     let args = Context.Rel.instance mkRel 0 ctx in
@@ -842,7 +842,7 @@ let std_refine ~metas env sigma cl r =
 
 type refiner_kind =
 | Std of Meta.t * EConstr.t
-| Case of case_node * (EConstr.rel_context * EConstr.t) array
+| Case of case_node * (Id.t * EConstr.rel_context * EConstr.t) array
 
 let refiner_gen is_case =
   let open Proofview.Notations in
@@ -1002,11 +1002,12 @@ let case_pf ?(with_evars=false) ~dep (indarg, typ) =
     let get_branch cs =
       let base = mkApp (pred, cs.cs_concl_realargs) in
       let argctx = cs.cs_args in
+      let name = cs.cs_name in
       if dep then
         let argctx = Namegen.name_context env sigma argctx in
-        (argctx, applist (base, [build_dependent_constructor cs]))
+        (name, argctx, applist (base, [build_dependent_constructor cs]))
       else
-        (argctx, base)
+        (name, argctx, base)
     in
     Array.map get_branch constrs
   in
@@ -1032,7 +1033,7 @@ let case_pf ?(with_evars=false) ~dep (indarg, typ) =
     Internal.Case ((ci, u, pms, (p,r), iv, c), branches)
   | PrimitiveEta args ->
     let mv = new_meta () in
-    let (ctx, t) = branches.(0) in
+    let (_, ctx, t) = branches.(0) in
     let metas = Meta.meta_declare mv (it_mkProd_or_LetIn t ctx) metas in
     Internal.Std (metas, mkApp (mkMeta mv, Array.map nf_betaiota args))
   in

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