The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 05/07/2015 10:32 AM, Cedric Auger wrote:
> 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.

Speaking from the IDE implementation side, I think there's a legitimate use 
case for such a feature: lemma extraction. `company-coq` already implements 
this on top of Proof-General: you press a key, specify the hypotheses that 
you want to keep, and it inserts a new (selected hypotheses + dependencies -> 
goal) lemma for you.

I often come across cases where I have a bunch of useless hypotheses and a 
few relevant ones, as part of a larger proof. In these cases I like to pull 
out the relevant hypotheses and the goal into a separate lemma, that I can 
just use in conjunction with [eauto using] in the larger proof. For example:

  p : nat
  q : nat
  r : nat
  H : p < q < r
  H0 : p + q < q + r
  H1 : exists s : nat, p + q + r < s
  n : nat
  m : nat
  IHm : n + m = m + n
  ============================
   n + S m = S m + n

In this case I want to get the following lemma generated automatically:

  Lemma subgoal:
    forall n m : nat, n + m = m + n -> n + S m = S m + n.

company-coq already has a feature to do this automatically (C-c C-a C-x) 
based on a sequence of [generalize dependent] and [clear]), but it breaks 
when printing-only notations are in used in the display of the goal. Some 
sort of [Set Printing Reparsable] option would be a very welcome addition in 
this case; the other printing options are tricky to fine-tune automatically.

Clément.