Reference Manual should document that `vm_compute` and `native_compute` ignore parameters of inductive constructors

[JasonGross]

I could not find this documented at https://coq.github.io/doc/master/refman/proofs/writing-proofs/equality.html?highlight=vm_compute#coq:tacn.vm_compute . Here is an example:

Eval cbv in @existT nat (fun n => n + n = 2) 1 eq_refl.
(*      = existT (fun n : nat => (fix add (n0 m : nat) {struct n0} : nat := match n0 with
                                                                         | 0 => m
                                                                         | S p => S (add p m)
                                                                         end) n n = 2) 1 eq_refl
     : {n : nat & n + n = 2}
 *)
Eval vm_compute in @existT nat (fun n => n + n = 2) 1 eq_refl.
(*      = existT (fun n : nat => n + n = 2) 1 eq_refl
     : {n : nat & n + n = 2}
 *)
Eval native_compute in @existT nat (fun n => n + n = 2) 1 eq_refl.
(*      = existT (fun n : nat => n + n = 2) 1 eq_refl
     : {n : nat & n + n = 2}
 *)

cc @jfehrle

[JasonGross]

Here is a bit of text that might be used to justify this in the refman: Omitting the parameters of inductive constructors is a principled choice: if two well-typed expressions have the same type, then it's safe to erase all inductive parameters to constructors when comparing them. Futhermore, these parameters will often be functions even in closed terms, so normalizing underneath their binders can be expensive.

(Parameters can perhaps link to https://coq.github.io/doc/master/refman/language/core/inductive.html#parametrized-inductive-types. Parameters as contrasted with indices are described at https://coq.github.io/doc/master/refman/language/core/inductive.html#the-match-with-end-construction, though I've always found the Agda description of indices vs parameters at https://agda.readthedocs.io/en/v2.6.1.3/language/data-types.html#indexed-datatypes with the example of Vector to be more concisely understandable when I've forgotten which arguments are parameters and which are indices ("In contrast to parameters which are required to be the same for all constructors, indices can vary from constructor to constructor. They are declared after the colon [...]"))

[silene]

Could it be that it is not documented because this is actually a bug? vm_compute and native_compute are expected to compute normal forms, and clearly, on your examples, that is not the case.

[JasonGross]

I believe this is not a bug and that it might cause a severe performance regression to "fix" it. The purpose of these tactics is to leave behind a cast in the proof term that instructs the kernel on how to normalize two types for comparison. Normalizing function-typed parameters of inductive constructors will almost always result in enormous terms that are not useful. I wouldn't be surprised if I could cook up an example where implementing this "fix" changes the asymptotic running time of a reduction in a bad way.

[silene]

Notwithstanding opacity concerns, cbv, lazy, vm_compute, and native_compute, are expected to normalize terms to the same normal form. If you feel that normalization should not apply to parameters of inductive constructors, then cbv and lazy should be fixed. Indeed, why would the sentence "Normalizing function-typed parameters of inductive constructors will almost always result in enormous terms that are not useful" not apply to cbv and lazy?

[JasonGross]

Indeed, why would the sentence "Normalizing function-typed parameters of inductive constructors will almost always result in enormous terms that are not useful" not apply to cbv and lazy?

I can defend the design choice for vm_compute and native_compute because these reduction mechanisms are specifically optimized. I think the rest of the tactics live on a spectrum. For simpl and cbn, for example, I expect that we do want to normalize parameters, because these tactics are more about making the end result look pretty to the user, and are not used for complete reduction. For cbv and lazy, I can see arguments in both directions. Like vm_compute and native_compute, they do complete reduction, which is not very useful for function-typed parameters. Like simpl and cbn, they are sometimes used to make the goal more understandable. Furthermore, there are some cases where you want to normalize function-typed parameters, for example if you're going to use constr_eq to compare the types of hypotheses and you need to be sure that they are normalized similarly. It's going to be very confusing if cbv [foo] in * does not unfold foo even when unfold foo in * does and moreover a tactic fails because foo is unfolded in one hypothesis but not another. (This is not a concern for vm_compute and native_compute which, even if they took whitelists of identifiers to unfold, would not be very useful for unfolding in hypotheses because they leave behind no casts.)