Zulip Chat Archive

Stream: new members

Topic: tactic style proofs to term style proofs

Patrick Thomas (Feb 19 2019 at 03:57):

Is it possible to automatically translate a tactic style proof to a term style proof? Is it theoretically possible?

Mario Carneiro (Feb 19 2019 at 05:03):

#print

Mario Carneiro (Feb 19 2019 at 05:03):

The reverse is much harder

Kenny Lau (Feb 19 2019 at 08:22):

@Mario Carneiro exact

Mario Carneiro (Feb 19 2019 at 08:22):

you know what I mean

Johan Commelin (Feb 19 2019 at 19:16):

Note that #print will give you a term-mode proof indeed. But it is not in the style that mathlib likes. After all, not all term-mode proofs are equal :grinning:

Kevin Buzzard (Feb 19 2019 at 19:22):

They are definitionally equal!

Johan Commelin (Feb 19 2019 at 19:26):

Sure, but the mathlib maintainers have even stricter notions of equality :joking:

Patrick Thomas (Mar 06 2019 at 05:11):

I tried #print on the default example from the web editor, but I could not really understand the result. If I wanted to write a program to translate a tactic style proof to a declarative style proof using statements like 'let' and 'have', would that be feasible?

Patrick Thomas (Mar 06 2019 at 05:12):

I would have to learn tactics first, but if I did so, I'm wondering how difficult it would be.

Mario Carneiro (Mar 06 2019 at 05:14):

Only if the proof uses "boring tactics" like intros, have, change, refine, exact, apply and cases to some extent

Mario Carneiro (Mar 06 2019 at 05:14):

If it uses rw or simp or even more complicated tactics, the corresponding proof term is much more complicated

Patrick Thomas (Mar 06 2019 at 05:18):

I guess I was thinking of translating from the list of tactics themselves, or even the code for the tactics, not the resulting proof term. Would that make a difference?

Scott Morrison (Mar 06 2019 at 05:27):

Not really; rw and simp often produce irreducibly complicated proofs terms.

Patrick Thomas (Mar 06 2019 at 05:43):

Is there documentation on how the tactics are implemented in code? Maybe that would help me understand the issue better.

Scott Morrison (Mar 06 2019 at 05:45):

You mean the core tactics like rw and simp? No, the only available documentation is the C++ source code.

Patrick Thomas (Mar 06 2019 at 05:47):

Are there user created tactics outside of the 'core' tactics?

Scott Morrison (Mar 06 2019 at 05:54):

Absolutely. Read https://github.com/leanprover-community/mathlib/blob/master/docs/tactics.md for an overview, or directly read the source code for these at https://github.com/leanprover-community/mathlib/tree/master/src/tactic

Scott Morrison (Mar 06 2019 at 05:55):

As a classic example, ring is written in mathlib.

Scott Morrison (Mar 06 2019 at 05:55):

There's a nice blog post explaining a baby version of ring at https://xenaproject.wordpress.com/2018/06/13/ab3/

Patrick Thomas (Mar 06 2019 at 06:00):

Thank you, I'll take a look.
I'm curious as to why the tactic style seems to be more prevalent than the declarative style in the proof assistants that I have seen. Is it because they are better suited to automated deduction?