Equations, funelim and new variables

Using Coq
1

I’m very happy with the funelim tactic except for the new variable names it introduces. I would like to control the names chosen (as with the induction tactic). Currently I use for instance

  funelim (dnf C D);
    rename C0 into C;
    try rename l into D;
    try clear Heq;
    try rename H into IH;
    try rename H0 into IH'.

to cover all of the (many) cases resulting from the defining equations of the function dnf. This is unsatisfactory since the script will break if Equations changes its naming policy. As quick fix the inductive hypotheses could be named IHn, and the names given in the patterns of the defining equations could be preserved. Also the Heq’s could be eliminated by default. This would get rid of all clears and renames in the example above.

2

Indeed, funelim is not the most robust with respect to naming. I tried to improve the situation, but it’s maybe not ideal yet. It is not true that the Heq hypotheses can always be substituted I think, in presence of dependent types at least the rewrites are not always possible.

3

Hi,
Even in non dependent cases Heq on non-variable terms must be kept. Others can be removed with subst.

4

I improved it a little bit in the latest version, but it’s not robust yet. There is an alternative apply_funelim tactic now that does less introductions. The substitution of equalities is indeed not possible in general but surely one can come up with heuristics and write the appropriate tactic to simplify goals.