Reference a part of an expression

Stream: Is there code for X?

[Patrick Johnson]

After unfolding/simplifying expressions, sometimes I end up with a very large and complicated expression appearing in multiple assumptions and in the goal. What I usually do is generalize h : copy_pasted_large_expression = x and then rw h at h1 h2 h3 .... Is it possible to avoid copying and pasting? Can we somehow describe the location of the expression we want to reference? For example, given an assumption like this:

h : P (f (g x y) (g x y)) (Q (g x y))

I would like to be able to reference g x y by describing its location inside the type of assumption h (something like an expression path, taking left/right choices while descending the function application/lambda expressions). It is probably possible to write a tactic, but is there something like this already in Lean/mathlib?

[Johan Commelin]

I'm not aware of anything like that atm

[Eric Wieser]

Can you give a #mwe to play around with?

[Eric Wieser]

I guess it's

example {α β γ δ ε} (g : α → β → γ) (f : γ → γ → δ) (P : δ → ε → Prop) (Q : γ → ε) (x: α) (y : β)
  (h : P (f (g x y) (g x y)) (Q (g x y))) : true :=
begin

end

[Kevin Buzzard]

@Reid Barton IIRC you once wrote some cute trick to extract the LHS of an equation from the equation. Do you remember what I'm talking about?

[Eric Wieser]

Does this do what you want?

import tactic  -- doesn't show `:= g x y` without this!?

example {α β γ δ ε} (g : α → β → γ) (f : γ → γ → δ) (P : δ → ε → Prop) (Q : γ → ε) (x: α) (y : β)
  (h : P (f (g x y) (g x y)) (Q (g x y))) : true :=
begin
  let G_expr := _,
  have : P (f G_expr G_expr) (Q G_expr) := h,
  trivial
end

[Eric Wieser]

Here lean fills out the _ for you, which is presumably the bit you didn't want to copy-paste

[Kyle Miller]

You can use conv mode to locate a particular expression, then there could be a conv tactic (maybe generalize_goal?) that would do the rest?

[Patrick Johnson]

Here lean fills out the _ for you, which is presumably the bit you didn't want to copy-paste

I'm really surprised that it works.

[Reid Barton]

Kevin Buzzard said:

Reid Barton IIRC you once wrote some cute trick to extract the LHS of an equation from the equation. Do you remember what I'm talking about?

Yes vaguely but I don't know how to find it. It involved some similar let with _ as body trick.

[Patrick Johnson]

Maybe this?

[Reid Barton]

Oh that's not what I was thinking of, but also good! Maybe what Kevin was thinking of

[Reid Barton]

I'm thinking of something more like (probably essentially the same as) what Eric wrote

[Joachim Breitner]

I tried to take @Eric Wieser ’s suggestion and re-do it using conv like this:

example {α β γ δ ε} (g : α → β → γ) (f : γ → γ → δ) (P : δ → ε → Prop) (Q : γ → ε) (x: α) (y : β)
  (h : P (f (g x y) (g x y)) (Q (g x y))) : true :=
begin
  let G_expr := _,
  conv at h in (Q _) { congr, change G_expr, }

end

but unfortunately, I get (with set_option trace.app_builder true on)

[app_builder] failed to create an 'eq'-application, failed to solve unification constraint for #1 argument (γ =?= ?m_1)

It does work if I manually specify G_expr’s type; after

example {α β γ δ ε} (g : α → β → γ) (f : γ → γ → δ) (P : δ → ε → Prop) (Q : γ → ε) (x: α) (y : β)
  (h : P (f (g x y) (g x y)) (Q (g x y))) : true :=
begin
  let G_expr : γ := _,
  conv at h { congr, skip, congr, change G_expr, },

I get a goal state of

G_expr: γ := g x y
h: P (f (g x y) (g x y)) (Q G_expr)

Oh, and oddly, I cannot use

  conv at h in (Q _) { congr, change G_expr, },

or

  conv at h { find (Q _) { congr, change G_expr, }, },

– maybe find prevents the unification from escaping?

[Joachim Breitner]

Fun, because of this problem(?) of find hiding the side-effects from unification, I can prove false, or at least believe I am proving it, until the end of the lemma:

example : false :=
begin
  have h : id (tt ≠ ff), simp,
  let b : bool := _,
  {
    conv at h in (id _) { congr, to_lhs, change b, skip, },
    conv at h in (id _) { congr, to_rhs, change b, skip, },
    have : b ≠ b := h,
    show false, exact this rfl,
  },
  exact tt,
end

Is this worth fixing?

[Kevin Buzzard]

ha, yeah, you might be able to trick the tactic monad but you can't trick the kernel :-)

[Kyle Miller]

@Joachim Breitner That seems worth looking into to me. I'm not sure whether it's a bug or a known limitation that the metavariables for the let binding don't get instantiated (I think that's the word).

[Eric Wieser]

I remember there being some nasty state bugs last time I looked at the find tactic

[Eric Wieser]

Namely that if I tried to preserve the state properly in the lean code, the VM would crash