Why induction principle such as list_rect cannot be added in Hint database?

Using Rocq
1

Hi all. May I ask why is induction principle, say list_rect, cannot be added to any Hint database?

I tried adding it but the error: “list_rect cannot be used as a hint.” appeared.

2

As the documentation states: “The head symbol of the type of list_rect is a bound variable such that this tactic cannot be associated to a constant.”

More precisely, hints use the head symbol of the consequent (e.g., eq, lt) to guess when they can be used. Since list_rect has type forall P, ... -> P ..., its head symbol P is not known until the lemma has been applied.

1 Like
3

Thank you for your prompt reply. :slight_smile: