# Zulip Chat Archive

## Stream: general

### Topic: explode command

#### Mario Carneiro (Aug 30 2018 at 23:54):

While on the flight home, I decided to actually write the wishlist tactic I've mentioned to a few people, which displays lean proofs in a line by line style heavily annotated with type ascriptions so it looks more like a Fitch style proof. I'm still tweaking the display options, but here's what it looks like right now:

import tactic.explode section end #explode iff_true

iff_true : ∀ (a : Prop), a ↔ true ↔ a 0│ │ a ├ Prop 1│ │ h │ ┌ a ↔ true 2│ │ trivial │ │ true 3│1,2│ iff.mpr │ │ a 4│3 │ ∀I │ (a ↔ true) → a 5│ │ iff_true_intro │ a → (a ↔ true) 6│4,5│ iff.intro │ a ↔ true ↔ a

#### Johan Commelin (Aug 31 2018 at 04:38):

Ok, I can parse this, and it looks really helpful... but why is line `0`

at the top, instead of the bottom?

#### Mario Carneiro (Aug 31 2018 at 04:38):

it's numbered like lines of proof

#### Johan Commelin (Aug 31 2018 at 04:39):

It seems to me that `0`

follows from `6`

, but maybe I misunderstand `0`

#### Johan Commelin (Aug 31 2018 at 04:39):

Also, I'd rather read them upside down.

#### Mario Carneiro (Aug 31 2018 at 04:39):

lambdas are introduced with the intro variable on top of the bracket

#### Johan Commelin (Aug 31 2018 at 04:39):

First split the goal, then you get two subtrees... etc..

#### Mario Carneiro (Aug 31 2018 at 04:40):

Yes, I usually read metamath proofs bottom up as well

#### Johan Commelin (Aug 31 2018 at 04:40):

Aaah, that is what `0`

is doing, of course!

#### Johan Commelin (Aug 31 2018 at 04:40):

Well... there is a solution to that: have `#explode`

reverse the order...

#### Johan Commelin (Aug 31 2018 at 04:40):

But now I see that `0`

should remain at the top.

#### Johan Commelin (Aug 31 2018 at 04:40):

So it's not that easy...

#### Mario Carneiro (Aug 31 2018 at 04:41):

I suppose, but that will get confusing to explain to people

#### Mario Carneiro (Aug 31 2018 at 04:41):

I would prefer a forward proof ordering on the page

#### Mario Carneiro (Aug 31 2018 at 04:41):

even if your interest is drawn from the bottom up

#### Johan Commelin (Aug 31 2018 at 04:41):

How far is this representation from writing a `begin end`

proof?

#### Johan Commelin (Aug 31 2018 at 04:42):

Could you generate that as well?

#### Mario Carneiro (Aug 31 2018 at 04:42):

what do you mean?

#### Mario Carneiro (Aug 31 2018 at 04:42):

like you want the lines to correspond to `apply`

and `intro`

?

#### Johan Commelin (Aug 31 2018 at 04:42):

Right.

#### Johan Commelin (Aug 31 2018 at 04:42):

`#deobfuscate`

#### Mario Carneiro (Aug 31 2018 at 04:43):

it's pretty close, there are some edge cases where you see explicit `∀E`

and `∀I`

steps

#### Johan Commelin (Aug 31 2018 at 04:44):

Even if it isn't perfect, I'dd really like it.

#### Mario Carneiro (Aug 31 2018 at 04:45):

can you mockup?

#### Johan Commelin (Aug 31 2018 at 04:46):

What do you mean? This example? Or more general?

#### Mario Carneiro (Aug 31 2018 at 04:48):

either, something that shows off what you would like to see

#### Johan Commelin (Aug 31 2018 at 04:48):

Rob has this interface with mathematica... with certain terms corresponding to certain mathematica terms

#### Johan Commelin (Aug 31 2018 at 04:49):

So we could also have a dictionary `\lam <-> intros`

etc...

#### Johan Commelin (Aug 31 2018 at 04:49):

But I don't have a clear picture how to actually implement this

#### Mario Carneiro (Aug 31 2018 at 04:50):

oh, there is a potential problem with making a real runnable proof script, as opposed to just a display like this... it has to parse as valid lean, and sometimes `pp`

doesn't give good results

#### Mario Carneiro (Aug 31 2018 at 04:50):

I am currently hiding non proof terms in `#explode`

, but probably this won't work in a proof script

#### Johan Commelin (Aug 31 2018 at 04:52):

iff_true : ∀ (a : Prop), a ↔ true ↔ a 0│ │ a ├ Prop | intro (intros?) 1│ │ h │ ┌ a ↔ true | intro (intros?) 2│ │ trivial │ │ true | exact trivial 3│1,2│ iff.mpr │ │ a | apply iff.mpr 4│3 │ ∀I │ (a ↔ true) → a | ??? 5│ │ iff_true_intro │ a → (a ↔ true) | exact iff_true_intro 6│4,5│ iff.intro │ a ↔ true ↔ a | apply iff.intro (split?)

#### Johan Commelin (Aug 31 2018 at 04:54):

I just added an extra column, and it totally wouldn't run.

#### Mario Carneiro (Aug 31 2018 at 04:54):

I guess part of the problem with line for line translating this display into a proof script is that forward proving is less natural

#### Mario Carneiro (Aug 31 2018 at 04:55):

you have to use lots of `have`

#### Johan Commelin (Aug 31 2018 at 04:55):

Right

#### Mario Carneiro (Aug 31 2018 at 04:55):

and the positioning of the `intro`

is weird

#### Mario Carneiro (Aug 31 2018 at 04:58):

The hard stuff is when dealing with `eq.rec`

though

iff_not_comm : ∀ {a b : Prop} [_inst_1 : decidable a] [_inst_2 : decidable b], a ↔ ¬b ↔ (b ↔ ¬a) 0 │ │ a ├ Prop 1 │ │ b ├ Prop 2 │ │ _inst_1 ├ decidable a 3 │ │ _inst_2 ├ decidable b 4 │ │ eq.refl │ (a ↔ ¬b ↔ (b ↔ ¬a)) = (a ↔ ¬b ↔ (b ↔ ¬a)) 5 │ │ iff_def │ a ↔ ¬b ↔ (a → ¬b) ∧ (¬b → a) 6 │5 │ propext │ (a ↔ ¬b) = ((a → ¬b) ∧ (¬b → a)) 7 │4,6 │ eq.rec │ (a ↔ ¬b ↔ (b ↔ ¬a)) = ((a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a)) 8 │7 │ id │ (a ↔ ¬b ↔ (b ↔ ¬a)) = ((a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a)) 9 │ │ eq.refl │ ((a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a)) = ((a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a)) 10│ │ iff_def │ b ↔ ¬a ↔ (b → ¬a) ∧ (¬a → b) 11│10 │ propext │ (b ↔ ¬a) = ((b → ¬a) ∧ (¬a → b)) 12│9,11 │ eq.rec │ ((a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a)) = ((a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b)) 13│12 │ id │ ((a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a)) = ((a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b)) 14│ │ imp_not_comm │ a → ¬b ↔ b → ¬a 15│ │ not_imp_comm │ ¬b → a ↔ ¬a → b 16│14,15│ and_congr │ (a → ¬b) ∧ (¬b → a) ↔ (b → ¬a) ∧ (¬a → b) 17│13,16│ eq.mpr │ (a → ¬b) ∧ (¬b → a) ↔ (b ↔ ¬a) 18│8,17 │ eq.mpr │ a ↔ ¬b ↔ (b ↔ ¬a)

#### Reid Barton (Aug 31 2018 at 06:16):

You should make a version which outputs those judgment tree things and outputs LaTeX

#### Patrick Massot (Aug 31 2018 at 07:28):

Noooo! We triggered Mario's immune defenses. He spent three days with people who want Lean to prove everything by itself, he merged tidy and then, flying back, he wrote the Lean2metamath tactic!

#### Kevin Buzzard (Aug 31 2018 at 12:36):

"On the flight home, I wrote an explode command" = "I just risked getting the plane diverted because the guy next to me panicked"

#### Mario Carneiro (Aug 31 2018 at 12:37):

I originally called it `mmshow`

but I decided against metamath branding it

Last updated: Aug 03 2023 at 10:10 UTC