## Stream: new members

### Topic: Determining the lemma applied by ext1

#### Eric Wieser (Jun 13 2020 at 11:16):

I've a tactic-mode proof that uses ext1, and I'd like to know exactly which lemma was applied. Is there an easy way to find out?

#### Eric Wieser (Jun 13 2020 at 11:17):

The specific transformation I'm trying to find is the one that simplifies the goal fromλ x, y = λ x, z to y = z

#### Jalex Stark (Jun 13 2020 at 11:20):

you can #print a lemma to see the term

#### Jalex Stark (Jun 13 2020 at 11:20):

to answer the question directly, i think you're looking for the name funext

#### Eric Wieser (Jun 13 2020 at 11:20):

But I don't know the lemma to print - ext1 is picking a lemma for me, isn't it?

#### Patrick Massot (Jun 13 2020 at 11:21):

example (y z : ℕ) : (λ x : ℕ, y) = λ x, z :=
begin
show_term{ ext1 },
sorry
end


#### Eric Wieser (Jun 13 2020 at 11:21):

Excellent, thanks!

#### Eric Wieser (Jun 13 2020 at 11:23):

How do I go from that term-mode expression to a tactic-mode line I can replace ext1 with?

#### Jalex Stark (Jun 13 2020 at 11:24):

are you asking the general question "how i do enter a term into a tactic mode proof?" I think the answer is exact

#### Eric Wieser (Jun 13 2020 at 11:24):

That only works as the terminal step of a proof though, right?

#### Eric Wieser (Jun 13 2020 at 11:25):

For now, I'm looking for a way to replace the tactic ext1 with something more precise.

#### Eric Wieser (Jun 13 2020 at 11:25):

apply funext doesn't quite seem to be the same.

#### Jalex Stark (Jun 13 2020 at 11:25):

Well here is the full term mode proof

#### Jalex Stark (Jun 13 2020 at 11:25):

lemma mwe (α β : Type*) (y z : α) (h : y = z) :
(λ x:β, y) = (λ x:β, z) :=
begin
ext,
exact h,
end

#print mwe


#### Jalex Stark (Jun 13 2020 at 11:26):

the output of the print is

theorem mwe : ∀ (α : Type u_1) (β : Type u_2) (y z : α), y = z → ((λ (x : β), y) = λ (x : β), z) :=
λ (α : Type u_1) (β : Type u_2) (y z : α) (h : y = z), funext (λ (x : β), h)


#### Jalex Stark (Jun 13 2020 at 11:26):

the heart of the proof is the term funext (λ (x : β), h)

#### Eric Wieser (Jun 13 2020 at 11:28):

I think in this particular case, I was looking for the answer

apply funext,
intro x_1,


as the equivalent of what ext1 was doing

#### Jalex Stark (Jun 13 2020 at 11:29):

yes, I think the #print statement tells you that

#### Eric Wieser (Jun 13 2020 at 11:30):

Thanks for the help, anyway.

#### Jalex Stark (Jun 13 2020 at 11:30):

there's no general algorithm for translating a term-mode proof into an "idiomatic" tactic proof

#### Jalex Stark (Jun 13 2020 at 11:32):

i think most people here only care about proofs up to an equivalence relation "how fast does it run, how well can you understand what's happening by reading it, how robust is it to minor changes in the underlying libraries"
(I might be missing something)

#### Jalex Stark (Jun 13 2020 at 11:34):

(so we have good tooling to answer those kinds of questions, and may not have good tooling to answer other kinds of questions about proofs)

#### Scott Morrison (Jun 13 2020 at 11:52):

show_term will print terms with placeholders, so if it's it isn't the final step in a proof, you can use refine ..., replacing ... with the output of show_term.

#### Scott Morrison (Jun 13 2020 at 11:52):

Of course, many tactics will produce proof terms that you would not want to copy and paste.

#### Eric Wieser (Jun 13 2020 at 11:57):

I'm finding some irritating behavior with show_term. I'd assumed that if I have a term like
(begin show_term{ some, tactics, } end), then I can replace the whole thing with the output of show_term. In my case though, doing so gives an error

#### Jalex Stark (Jun 13 2020 at 11:59):

well you don't want to place a raw term inside of your tactic script. is the problem that you can't make it work even with refine?

#### Jalex Stark (Jun 13 2020 at 11:59):

do you want to show an example?

#### Jalex Stark (Jun 13 2020 at 12:00):

oh, i see, you got to the end of the proof and show_term isn't giving you a complete proof

#### Eric Wieser (Jun 13 2020 at 12:01):

Yeah, was just constructing the MWE

import tactic
variables {α : Type*}

def comp (τ σ : α → α → Prop) :=
λ a b : α, ∃ c : α, τ a c ∧ σ c b
notation τ ∘ σ := comp τ σ

/- Prove that composition is associative -/
theorem comp_assoc : @associative (α → α → Prop) comp :=
λ a b c, funext (λ a_1, funext (λ b_1, (iff.to_eq $iff.intro (begin show_term{ rintros ⟨z, ⟨y, rxy, syz⟩, tzw⟩, exact (exists.intro y$ and.intro rxy $exists.intro z$ and.intro syz tzw)
}
end)
(begin
rintros ⟨y, rxy, z, syz, tzw⟩,
exact (exists.intro z $and.intro (exists.intro y$ and.intro rxy syz) tzw)
end)
)))


If I replace the first (begin ... end) with the result of the show_term within it:

λ (a_2 : ((a ∘ b) ∘ c) a_1 b_1),
Exists.dcases_on a_2
(λ (z : α) (a_2_h : (a ∘ b) a_1 z ∧ c z b_1),
a_2_h.dcases_on
(λ (a_2_h_left : (a ∘ b) a_1 z) (tzw : c z b_1),
Exists.dcases_on a_2_h_left
(λ (y : α) (a_2_h_left_h : a a_1 y ∧ b y z),
a_2_h_left_h.dcases_on
(λ (rxy : a a_1 y) (syz : b y z), exists.intro y ⟨rxy, exists.intro z ⟨syz, tzw⟩⟩))))


I get the error

invalid 'Exists.dcases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables


(deleted)

#### Eric Wieser (Jun 13 2020 at 12:07):

This is taken from https://www.codewars.com/kata/5ea9b14c9b7bf50001b88e55/train/lean, where I don't appear to have rintros available to me, so I was trying to work out the replacement.

#### Reid Barton (Jun 13 2020 at 12:08):

rintros should work fine on codewars, as long as you have import tactic

#### Jalex Stark (Jun 13 2020 at 12:08):

disclaimer: I personally have spent no time trying to build long term proofs
I think the way that people build long term proofs is with holes

#### Jalex Stark (Jun 13 2020 at 12:09):

codewars is running... lean community 3.11? with the last mathlib that was published before 3.12?

#### Jalex Stark (Jun 13 2020 at 12:09):

rintros is a lot older than that I think

#### Eric Wieser (Jun 13 2020 at 12:10):

Whoops, typo as import tactics.

Still, would like to understand what rintros is doing for me in that example

#### Eric Wieser (Jun 13 2020 at 12:10):

But it's hard to do so when the supposed show_term replacement doesn't actually work

#### Jalex Stark (Jun 13 2020 at 12:10):

rintros is intros, rcases
(so you can make the terms a little shorter and get to the truth more quickly by focusing in on the rcases part)

#### Mario Carneiro (Jun 13 2020 at 12:25):

@Eric Wieser rcases is doing repeated cases. cases , even recursive cases, can be mimicked in term mode using let <x, y, z, ...> = proof in proof

#### Eric Wieser (Jun 13 2020 at 12:35):

Here's an even simpler reproduction of show_term failing:

import tactic
variables {α : Type*}

def comp (τ σ : α → α → Prop) :=
λ a b : α, ∃ c : α, τ a c ∧ σ c b
notation τ ∘ σ := comp τ σ

theorem show_term_doesnt_work (a b c : α → α → Prop) (a_1 b_1 : α) :
((a ∘ b) ∘ c) a_1 b_1 → (a ∘ b ∘ c) a_1 b_1 :=
(begin
show_term{
rintros ⟨z, ⟨y, rxy, syz⟩, tzw⟩,
exact (exists.intro y $and.intro rxy$ exists.intro z $and.intro syz tzw) } end)  The result of show_termis the same as above, but when you actually use the suggested term as import tactic variables {α : Type*} def comp (τ σ : α → α → Prop) := λ a b : α, ∃ c : α, τ a c ∧ σ c b notation τ ∘ σ := comp τ σ theorem show_term_doesnt_work (a b c : α → α → Prop) (a_1 b_1 : α) : ((a ∘ b) ∘ c) a_1 b_1 → (a ∘ b ∘ c) a_1 b_1 := (λ (a_2 : ((a ∘ b) ∘ c) a_1 b_1), Exists.dcases_on a_2 (λ (z : α) (a_2_h : (a ∘ b) a_1 z ∧ c z b_1), a_2_h.dcases_on (λ (a_2_h_left : (a ∘ b) a_1 z) (tzw : c z b_1), Exists.dcases_on a_2_h_left (λ (y : α) (a_2_h_left_h : a a_1 y ∧ b y z), a_2_h_left_h.dcases_on (λ (rxy : a a_1 y) (syz : b y z), exists.intro y ⟨rxy, exists.intro z ⟨syz, tzw⟩⟩)))))  You get the same error as above, invalid 'Exists.dcases_on' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables  #### Reid Barton (Jun 13 2020 at 12:36): It's not that show_term is failing--it printed what I assume is the actual proof term; it's just that Lean can't actually re-elaborate it #### Eric Wieser (Jun 13 2020 at 12:36): Can you explain why some terms can't be re-elaborated? #### Reid Barton (Jun 13 2020 at 12:36): Because the default is to hide implicit arguments like all the induction motives, but for whatever reason Lean can't re-infer them #### Reid Barton (Jun 13 2020 at 12:37): If you use set_option pp.all true then you would get a term more likely to round-trip #### Eric Wieser (Jun 13 2020 at 12:38): Thanks, that did the trick. It would be nice if show_term could only put in the information that lean needs to round-trip #### Reid Barton (Jun 13 2020 at 12:38): It's hard enough to consistently render a string that Lean will be able to re-elaborate, but by default it's trying to produce somthing vaguely human-readable as well and then the problem is basically impossible. #### Reid Barton (Jun 13 2020 at 12:41): Eric Wieser said: the information that lean needs to round-trip For this to be well-defined the elaboration has to have some kind of locality property which I'm not sure is true in practice. #### Reid Barton (Jun 13 2020 at 12:41): In other words: could adding more information in a deep sub-term affect the elaboration of some outer part of the structure? I suspect so, and then the search space for this kind of thing would be huge. #### Kevin Buzzard (Jun 13 2020 at 12:52): @Eric Wieser I thought you just wanted to see the term to see which lemmas had been used? Making the pretty printer an inverse of the elaborator is a much harder problem #### Mario Carneiro (Jun 13 2020 at 12:54): Actually, I think the specific problem here is that lean is using projection notation for elab_as_eliminator functions #### Mario Carneiro (Jun 13 2020 at 12:55): which basically never works #### Mario Carneiro (Jun 13 2020 at 12:55): you can locally fix this by setting some option #### Mario Carneiro (Jun 13 2020 at 12:57): import tactic variables {α : Type*} def comp (τ σ : α → α → Prop) := λ a b : α, ∃ c : α, τ a c ∧ σ c b notation τ ∘ σ := comp τ σ set_option pp.structure_projections false example (a b c : α → α → Prop) (a_1 b_1 : α) : ((a ∘ b) ∘ c) a_1 b_1 → (a ∘ b ∘ c) a_1 b_1 := (begin show_term{ rintros ⟨z, ⟨y, rxy, syz⟩, tzw⟩, exact (exists.intro y$ and.intro rxy $exists.intro z$ and.intro syz tzw)
}
end)

example (a b c : α → α → Prop) (a_1 b_1 : α) :
((a ∘ b) ∘ c) a_1 b_1 → (a ∘ b ∘ c) a_1 b_1 :=
λ (a_2 : ((a ∘ b) ∘ c) a_1 b_1),
Exists.dcases_on a_2
(λ (z : α) (a_2_h : (a ∘ b) a_1 z ∧ c z b_1),
and.dcases_on a_2_h
(λ (a_2_h_left : (a ∘ b) a_1 z) (tzw : c z b_1),
Exists.dcases_on a_2_h_left
(λ (y : α) (a_2_h_left_h : a a_1 y ∧ b y z),
and.dcases_on a_2_h_left_h
(λ (rxy : a a_1 y) (syz : b y z), exists.intro y ⟨rxy, exists.intro z ⟨syz, tzw⟩⟩))))


Last updated: May 11 2021 at 14:11 UTC