# Zulip Chat Archive

## Stream: new members

### Topic: Some thoughts on tactics and proof readability / portability

#### ElCondor (Nov 17 2023 at 05:48):

Hi!

As a newcomer to Lean I would like to share a thought I had (and which I suppose has already been discussed?).

With Lean, using some tactic like `simp`

(or `norm_num`

, ...) I can prove a lemma directly:

```
lemma a_more_or_less_complex_lemma: ... := by simp
```

From the proof-writer point of view, this is very nice (if the tactic succeeds) because I can move move on to my other goals.

From the proof-reader point of view, this is less nice because I might be interested to know the details of the proof of `a_more_or_less_complex_lemma`

, especially if it's complex, and the way it is written doesn't make anything explicit.

Also, if I want to take this proof and port it to another proof system, there is no guarantee that there will be a similar strategy able to solve that lemma.

There even is no guarantee that this lemma will be portable from one version of Lean to another (well, there is no guarantee either if the steps are detailed but at least we have an idea what is going on).

How should that concern be addressed?

Also, when a tactic like `simp`

in my example successfully proves `a_more_or_less_complex_lemma`

, is there some easy way to turn this into an explicit proof? (the only way I found is to `#print a_more_or_less_complex_lemma`

and see what it does but the presentation isn't really reader-friendly)

#### Kyle Miller (Nov 17 2023 at 06:09):

One thing you can do for a more-explicit proof is use `simp?`

, which tells you exactly which lemmas `simp`

used.

The `simp`

tactic doesn't generate a particularly readable proof. It'd be neat if it could output a proof script using `conv`

tactics and `rw`

.

#### Joachim Breitner (Nov 17 2023 at 06:48):

Or even an explicit `calc`

for when you really want a readable human like proof! (I dabbled in that direction once, but got stuck somewhere. Will maybe pick up the calcifier once I am more versed in metaprogramming and have some slack time)

Last updated: Dec 20 2023 at 11:08 UTC