Stream: Coq users

Topic: Abstract and tactic-in-terms


view this post on Zulip Guillaume Melquiond (Mar 11 2021 at 12:26):

Is abstract supposed to work in tactic-in-terms? The documentation says that it does not work "properly". But does that mean that it does not work at all? Obviously, it cannot work if there are evars lying around, but I cannot even make it work in the fully determined case. Here is a very simplified example:

Definition foo : { x | x = _ } :=
  ltac:(exists 0; refine (_: _=0); abstract reflexivity).

Unfortunately, the proof of reflexivity is not abstracted away. Notice that I cannot use the proof mode here, because the type of the definition is not yet fully determined.

view this post on Zulip Enrico Tassi (Mar 11 2021 at 13:08):

Internally, there is no reason for not letting one start a definition in interactive mode when the type is not fully ground. I'd recommend lifting this limitation (and make many other used happy I believe) rather than hacking with abstract and tacinterms

view this post on Zulip Enrico Tassi (Mar 11 2021 at 13:11):

Maybe you could try Program Definition...

view this post on Zulip Guillaume Melquiond (Mar 11 2021 at 15:30):

No, Program Definition does not help, because it requires that the term (even with holes) has a ground type, just like Definition. Or, perhaps I am misunderstanding what you mean.

view this post on Zulip Enrico Tassi (Mar 11 2021 at 15:58):

You are right. One more reason to lift the limitation.

view this post on Zulip Matthieu Sozeau (Mar 19 2021 at 11:27):

Indeed, this limitation is pretty bad.


Last updated: Jan 31 2023 at 12:01 UTC