The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-05-07 15:56 GMT+02:00 Gert Smolka <smolka AT ps.uni-saarland.de>:

Coq sometimes prints terms in such a way that they cannot be parsed again.  This is irritating when you learn Coq and also ruins some examples I would like to use when teaching proof terms.  The problem is with type inference.  Here is an example.

Definition L : true <> false :=
   fun A => eq_ind_r (x := false) (fun b => if b then False else True) I A.

Print L.

(* fun A : true = false =>
      eq_ind_r (fun b : bool => if b then False else True) I A *)

Check fun A : true = false =>
         eq_ind_r (fun b : bool => if b then False else True) I A.

(* Error blah blah *)

This is run with Coq 8.4.  The problem persists in Coq 8.5

I would hope that printing terms such that they can be parsed is a design goal.

Gert

​You can set/unset printing of many things. Implicit arguments, notations, universes belong to the set of things that you can force to print. This would mainly result in reparsable results output (though, it may not be 100% working).

You can also write your own library without using any thing implicit, and deactivate automatic insertion of implicit anotations.

"Printing terms such that they can be parsed again" is not a design goal and is very unlikely to become one (well, unless for the case where you unset all printing options). This is mainly due to the fact that some times, you may want to have "print-only" notations.

For instance, think of the "{x:A|P x}" type.

You can write a function "certify : ∀ A (P : A → Prop) (x : A), P x → {x:A|P x}", and want to have a notation turning "certify A P x H" into "⊲x‖P⊳" for improved readability:
 "certify nat (fun x => x<>0) 1 (fun H => match H in _=y return match y with O => False | _ => True end with eq_refl => I end)"

versus

 "⊲1‖fun x => x<>0⊳"

Such a notation is clearly not revertible, and can still be considered useful.

Thus the only hint I can provide is "first request your IDE to stop hiding stuff, then print, then copy/paste, then restore the printing state of the IDE".

Maybe that within a IDE, a thing which could be considered is to have a "copy as reparsable" in the IDE menu, which would automatically do this.
That does not seem trivial at all to have a useful feature from this.