Zulip Chat Archive

Stream: new members

Topic: tactic style proofs to term style proofs


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Feb 19 2019 at 05:03):

#print

view this post on Zulip Mario Carneiro (Feb 19 2019 at 05:03):

The reverse is much harder

view this post on Zulip Kenny Lau (Feb 19 2019 at 08:22):

@Mario Carneiro exact

view this post on Zulip Mario Carneiro (Feb 19 2019 at 08:22):

you know what I mean

view this post on Zulip 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:

view this post on Zulip Kevin Buzzard (Feb 19 2019 at 19:22):

They are definitionally equal!

view this post on Zulip Johan Commelin (Feb 19 2019 at 19:26):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Mar 06 2019 at 05:27):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Thomas (Mar 06 2019 at 05:47):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Mar 06 2019 at 05:55):

As a classic example, ring is written in mathlib.

view this post on Zulip 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/

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 06 2019 at 06:02):

The tactic state often makes these proofs easier to read in lean

view this post on Zulip Scott Morrison (Mar 06 2019 at 06:05):

Particularly rewriting can be a huge pain without the help of a tactic.

view this post on Zulip Patrick Thomas (Mar 06 2019 at 06:08):

What is the tactic state?

view this post on Zulip Mario Carneiro (Mar 06 2019 at 06:09):

Are you using emacs or vscode to read lean files?

view this post on Zulip Mario Carneiro (Mar 06 2019 at 06:09):

it is strongly recommended to use the lean mode in one of these editors

view this post on Zulip Patrick Thomas (Mar 06 2019 at 06:10):

vscode

view this post on Zulip Mario Carneiro (Mar 06 2019 at 06:10):

If you use ctrl-space to bring up the 'lean messages' view, then with your cursor inside a tactic block you will see the "tactic state" printed

view this post on Zulip Mario Carneiro (Mar 06 2019 at 06:11):

it describes the current goal to be proven, and you can step through a tactic proof by moving your cursor after each tactic

view this post on Zulip Patrick Thomas (Mar 06 2019 at 06:16):

Ah. I see.

view this post on Zulip Andrew Ashworth (Mar 06 2019 at 06:53):

Isar is very popular, I wouldn't the declarative style is less prevalent


Last updated: May 10 2021 at 00:31 UTC