I would like to be able use something like de Bruijn indices in Isabelle or in Coq, in order to refer to variables that have been introduced by quantifiers. For example, instead of writing:
forall x. forall y. (p x y)
I would like to write something like:
forall x. forall y. (p '2' '1')
where the indices '2' and '1' indicate that these variables are bound by, respectively, the second and the first quantifier (counting from inside to outside).
The reason why I need to do this is that the quantifiers will actually be hidden by abbreviations, and therefore I will not know the names of the variables. My formula will look like this:
box box (p '2' '1')
where box should be an abbreviation for something that introduces an unnamed/hidden bound variable, and I want '2' and '1' to refer to the unnamed/hidden variables introduced by the leftmost and rightmost "box", respectively.
Is it possible to achieve something like this in Isabelle or in Coq??
I can only speak constructively for Isabelle here: the formal syntax uses standard de-Bruijn representation of lambda terms internally, and there are various ways to reuse that for your own syntax and special notation. In fact, Isabelle/HOL is just another application of Isabelle, so its quantifiers and other binders are defined in user-space by regular mechanisms of the system.
The concepts to look for are "binders", "syntax transformations", "syntax translations" etc. notably in the Isabelle/Isar Reference Manual. This can be stretched quite far, e.g. see how implicit bindings for Hoare logic is done; it is just one small example of many others that have accumulated over the years.
In the Hoare Logic example, the implicit abstraction is introduced via the special syntax constant _quote, which is associated with Syntax_Trans.quote_tr from Isabelle/Pure -- it is a practically useful concept. That idea can be pushed even further to allow nesting of quotation/antiquotation (see $ISABELLE_HOME/src/HOL/ex/Multiquote.thy), although that did not have practical relevance in applications to the best of my knowledge.
BTW, I would be very surprised if Coq didn't have similar mechanisms for user notation with binders.