How to evaluate proof terms through opaque definitions?

Question

Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.

I understand why Coq doesn’t do this by default, and guess it would probably interact in unfavourable ways with proof irrelevance. My aim is not to use this computation as part of a proof, but rather purely for debugging/meta-analysis - much like how the Print command can display the proof terms associated with lemmas, even if they are actually opaque.

Is it possible, using the Coq api if necassary, to perform computation ignoring opaqueness of terms?

Think something like a PrintReduced command that reduces its argument as much as possible (until it reaches constructors, existential variables or axioms - things for which the definition doesn’t exist at all).

Answer 1

There are two types of opaque terms in Coq really opaque terms produced by Qed and terms with delayed evaluation produced by the Opaque command. I don't recall the details of opaque modules. You may just want the Transparent command.

IIRC the Bytecode evaluator ignores opacity https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:cmd.Eval . I think you can use it in definitions along the lines of https://coq.inria.fr/refman/language/core/definitions.html

Definition foo := Eval vm_compute in bar.

There is a trick I can't remember the source of at the moment for deopaquing decidable proof terms.

Suppose you have a procedure like

Definition decide (x y: nat): option (x = y).

Which is complete I suppose

Lemma complete x: if decide x x is Some _ then True else False p.

You can take an opaque proof to a nonopaque proof with something like

Definition fresh {x y: nat} (p: x = y): x = y :=
  if decide x y is Some q
  then q
  else p.

I hope this can help a little with your problem. Your question is a little unclear but I am also not familiar enough with opacity in Coq.