Zulip Chat Archive

Stream: new members

Topic: eq.rec in goal sub-proof

view this post on Zulip Chase Norman (Dec 26 2020 at 00:27):

I'm experiencing the issue discussed by Bjørn below:

Bjørn Kjos-Hanssen said:

When I #print the proof term, it is very long, and moreover when I try to use it directly in my code, I get invalid 'eq.rec' application,

I'm attempting to reference a subproof (in the form of an underscore) that is contained within my goal. This subproof does not work when copied because of an invalid 'eq.rec' application. Is there a more proper way to reference these proofs? library_search manages to solve the goal, but using its output does not. I presume this is unintended behavior.

view this post on Zulip Bryan Gin-ge Chen (Dec 26 2020 at 00:32):

Can you give a #mwe ?

view this post on Zulip Chase Norman (Dec 26 2020 at 02:43):

Getting a mwe might be difficult for this sort of scenario. I found a solution, albeit a 100 line copy-paste solution. For those who are experiencing the same issue, try temporarily setting set_option pp.all true .

view this post on Zulip Bjørn Kjos-Hanssen (Dec 26 2020 at 02:53):

There was maybe a relevant recent discussion here:
Bryan Gin-ge Chen said:

You can wrap your tactic in show_term { ... } to see the term that the tactic constructs (see tactic#show_term). In many cases the term is much too large and complex to be of any use though.

view this post on Zulip Eric Wieser (Dec 26 2020 at 08:59):

It would be great if there were a tactic to extract _ proofs within the goal state into local hypotheses

view this post on Zulip Reid Barton (Dec 27 2020 at 00:00):

It sounds like you took a wrong turn earlier.

Last updated: May 15 2021 at 23:13 UTC