Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Open
brando90 opened this issue Dec 11, 2022 · 2 comments

Comments

@brando90
Copy link

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
Copy link
Contributor

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
Copy link
Member

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants