explode command

Stream: general

[Mario Carneiro]

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]

Ok, I can parse this, and it looks really helpful... but why is line 0 at the top, instead of the bottom?

[Mario Carneiro]

it's numbered like lines of proof

[Johan Commelin]

It seems to me that 0 follows from 6, but maybe I misunderstand 0

[Johan Commelin]

Also, I'd rather read them upside down.

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

Yes, I usually read metamath proofs bottom up as well

[Johan Commelin]

Aaah, that is what 0 is doing, of course!

[Johan Commelin]

Well... there is a solution to that: have #explode reverse the order...

[Johan Commelin]

But now I see that 0 should remain at the top.

[Johan Commelin]

So it's not that easy...

[Mario Carneiro]

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

[Mario Carneiro]

I would prefer a forward proof ordering on the page

[Mario Carneiro]

even if your interest is drawn from the bottom up

[Johan Commelin]

How far is this representation from writing a begin end proof?

[Johan Commelin]

Could you generate that as well?

[Mario Carneiro]

what do you mean?

[Mario Carneiro]

like you want the lines to correspond to apply and intro?

[Johan Commelin]

Right.

[Johan Commelin]

#deobfuscate

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

can you mockup?

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

I am currently hiding non proof terms in #explode, but probably this won't work in a proof script

[Johan Commelin]

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]

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

[Mario Carneiro]

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]

you have to use lots of have

[Johan Commelin]

Right

[Mario Carneiro]

and the positioning of the intro is weird

[Mario Carneiro]

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]

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

[Patrick Massot]

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]

"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]

I originally called it mmshow but I decided against metamath branding it