## 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?

#### Mario Carneiro (Mar 06 2019 at 06:02):

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

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

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

#### Patrick Thomas (Mar 06 2019 at 06:08):

What is the tactic state?

#### Mario Carneiro (Mar 06 2019 at 06:09):

Are you using emacs or vscode to read lean files?

#### Mario Carneiro (Mar 06 2019 at 06:09):

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

vscode

#### 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

#### 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

Ah. I see.

#### 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