Zulip Chat Archive

Stream: new members

Topic: Determining the lemma applied by ext1


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:20):

you can #print a lemma to see the term

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:20):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Jun 13 2020 at 11:21):

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

view this post on Zulip Eric Wieser (Jun 13 2020 at 11:21):

Excellent, thanks!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jun 13 2020 at 11:24):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Jun 13 2020 at 11:25):

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

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:25):

Well here is the full term mode proof

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:26):

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

view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:29):

yes, I think the #print statement tells you that

view this post on Zulip Eric Wieser (Jun 13 2020 at 11:30):

Thanks for the help, anyway.

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:30):

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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Jun 13 2020 at 11:59):

do you want to show an example?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jun 13 2020 at 12:02):

(deleted)

view this post on Zulip 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.

view this post on Zulip Reid Barton (Jun 13 2020 at 12:08):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Jun 13 2020 at 12:09):

rintros is a lot older than that I think

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jun 13 2020 at 12:36):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:55):

which basically never works

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:55):

you can locally fix this by setting some option

view this post on Zulip 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