Determining the lemma applied by ext1

Stream: new members

[Eric Wieser]

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]

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]

you can #print a lemma to see the term

[Jalex Stark]

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

[Eric Wieser]

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

[Patrick Massot]

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

[Eric Wieser]

Excellent, thanks!

[Eric Wieser]

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

[Jalex Stark]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Jalex Stark]

Well here is the full term mode proof

[Jalex Stark]

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

#print mwe

[Jalex Stark]

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]

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

[Eric Wieser]

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]

yes, I think the #print statement tells you that

[Eric Wieser]

Thanks for the help, anyway.

[Jalex Stark]

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

[Jalex Stark]

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]

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

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]

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

[Eric Wieser]

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]

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]

do you want to show an example?

[Jalex Stark]

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

[Eric Wieser]

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

[Eric Wieser]

(deleted)

[Eric Wieser]

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]

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

[Jalex Stark]

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]

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

[Jalex Stark]

rintros is a lot older than that I think

[Eric Wieser]

Whoops, typo as import tactics.

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

[Eric Wieser]

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

[Jalex Stark]

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]

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

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]

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]

Can you explain why some terms can't be re-elaborated?

[Reid Barton]

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]

If you use set_option pp.all true then you would get a term more likely to round-trip

[Eric Wieser]

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]

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]

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]

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]

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

Actually, I think the specific problem here is that lean is using projection notation for elab_as_eliminator functions

[Mario Carneiro]

which basically never works

[Mario Carneiro]

you can locally fix this by setting some option

[Mario Carneiro]

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⟩⟩))))