How does one print proof terms as de bruijn indices instead of random named variables in Coq?

[brando90]

cross: https://coq.discourse.group/t/how-does-one-print-proof-terms-as-de-bruijn-indices-instead-of-random-named-variables-in-coq/1847/2

[NeuralCoder3]

Here is a helper method I wrote a few years ago in MetaCoq that achieves this: https://github.com/uds-psl/metacoq-nested-induction/blob/master/source/de_bruijn_print.v

The code is a bit older and I am sure there is better code in the current MetaCoq version to do this. But this should get the idea along.

The printing is relatively primitive and ignores identifiers for the most part. My application was to manually check the de Bruijn indices that I created myself in the plugins I wrote. For more general applications, I am not sure if it will be helpful to see the de Bruijn indices as they are hard to read as a human.

I believe there were also more sophisticated printing functions that use identifiers if possible and could be modified to a more readable hybrid printer.

[yforster]

If you want a hybrid printer printing both de Bruijn indices and names, you could change line 149 of template-coq/theories/Pretty.v to

    | Some id => id ^ "(" ^ string_of_nat n ^ ")"

and then in a file do

From MetaCoq.Template Require Import Loader All Pretty.
Import MCMonadNotation.

Definition print_with_de_Bruijn {A} (a : A) :=
  t <- tmEval cbv a ;;
  q <- tmQuoteRec t ;;
  r <- tmEval cbv (print_term (fst q, Monomorphic_ctx) [] true (snd q)) ;;
  tmPrint r.

MetaCoq Run (print_with_de_Bruijn plus).

which will pretty-print the cbv normal form of plus with both identifiers and indices