Zulip Chat Archive

Stream: new members

Topic: How do I get lamdas to apply outside of a lemma


view this post on Zulip Lars Ericson (Dec 24 2020 at 20:06):

I have a lemma which is defined as a particular term application which involves a lambda. If I apply the lemma, the lambda reduces. If I apply the term application, it does not. Is there a way to get the direct term application to reduce the lambda? Here is the sketch:

import algebra.ring.basic
import tactic

universe u
variables {α : Type u} [integral_domain α] {a b c d : α}

lemma foo : a = b + (c - d)  a + d = b + (c - d) + d := congr_arg (λ {a : α}, a + d)
#check @foo α _ a b c d
#check @congr_arg α α a (b+(c-d)) (λ {a : α}, a + d)

You can see the difference here:

lemma ex5dLR : a-b=c-d  a+d=b+c :=
begin
  intro h1,
  have h2 := @eq_add_of_sub_eq' α _ a b (c-d),
  have h3 := h2 h1,
  have h4 := @congr_arg α α a (b+(c-d)) (λ {a : α}, a + d),
  have h5 := h4 h3,
  have h4a := @foo α _ a b c d,
  have h5a := h4a h3,
end

where the state is

α : Type u,
_inst_1 : integral_domain α,
a b c d : α,
h1 : a - b = c - d,
h2 : a - b = c - d  a = b + (c - d),
h3 : a = b + (c - d),
h4 : a = b + (c - d)  ((λ {a : α}, a + d) = λ {a : α}, a + d),
h5 : (λ {a : α}, a + d) = λ {a : α}, a + d,
h4a : a = b + (c - d)  a + d = b + (c - d) + d,
h5a : a + d = b + (c - d) + d
 a + d = b + c

and h5a is nice and h5 has lambdas.

view this post on Zulip Eric Wieser (Dec 24 2020 at 20:22):

What exactly is your question? Do you want to turn h5 into h5a, vice versa, or something else?

view this post on Zulip Adam Topaz (Dec 24 2020 at 20:31):

I think you should take a look at the tactic apply_fun, it's a fun way to solve this example :wink:

view this post on Zulip Eric Wieser (Dec 24 2020 at 20:42):

Or is your question how to convert (λ a, f a) x to f x? If so, the answer is either "they're already equal by rfl", or tactic#delta

view this post on Zulip Lars Ericson (Dec 24 2020 at 21:01):

I am trying to avoid introducing extraneous lemmas, which is against the style guide. I wasn't able to figure out how to use apply_fun or delta in this example to avoid adding a few lemmas:

import algebra.ring.basic
import tactic
import tactic.apply_fun

universe u
variables {α : Type u} [integral_domain α] {a b c d : α}

lemma foo : a = b + (c - d)  a + d = b + (c - d) + d := congr_arg (λ {a : α}, a + d)

lemma bar : b + (c - d) + d = b + c :=
begin
  ring,
end

lemma ex5dLR : a-b=c-d  a+d=b+c :=
begin
  intro h1,
  have h2 := @eq_add_of_sub_eq' α _ a b (c-d),
  have h3 := h2 h1,
  have h4 := @foo α _ a b c d,
  have h5 := h4 h3,
  conv at h5
  begin
    to_rhs,
    rw bar,
  end,
  exact h5,
end

view this post on Zulip Adam Topaz (Dec 24 2020 at 21:05):

Here's an example to get you started:

import algebra
import tactic.apply_fun

example {α : Type*} [integral_domain α] (a b c : α) : a - c = b - c  a = b :=
begin
  intro h,
  apply_fun (λ t, t + c) at h,
  simp at h,
  assumption
end

view this post on Zulip Lars Ericson (Dec 24 2020 at 21:29):

Thanks. In this example:

example : a+d=b+c  a-b=c-d :=
begin
  intro h,
  apply_fun (λ t, t-b-d) at h,
  simp at h,
end

after the apply_fun I have

h: a + d - b - d = b + c - b - d

and I want it to simplify to

h: a - b = c - d

Instead the simp at h gives

h: a + d - b = c

If instead I got into conv mode and just try to simplify just the left hand side of h:

example : a+d=b+c  a-b=c-d :=
begin
  intro h,
  apply_fun (λ t, t-b-d) at h,
  conv at h
  begin
    to_lhs,
    simp,
  end
end

after the to_lhs my goal state is

1 goal
α : Type u,
_inst_1 : integral_domain α,
a b c d : α,
h : a + d - b - d = b + c - b - d
| a + d - b - d

after the simp but before exiting the conv block it becomes

state:
α : Type u,
_inst_1 : integral_domain α,
a b c d : α,
h : a + d - b - d = b + c - b - d
 a + d - b - d = ?m_1

and out of the conv block there is no change on h:

α: Type u
_inst_1: integral_domain α
abcd: α
h: a + d - b - d = b + c - b - d
 a - b = c - d

How do I apply simp to just left hand side or right hand side? I tried simp at h.left but that doesn't parse.

view this post on Zulip Eric Wieser (Dec 24 2020 at 21:54):

You can always use have to set an intermediate goal of the form you want and have simp solve that goal

view this post on Zulip Lars Ericson (Dec 25 2020 at 00:54):

DONE. The lesson learned is that a covering set of lemmas for common algebraic manipulations is in algebra.group.basic:

import algebra.ring.basic
import tactic
import tactic.apply_fun

universe u
variables {α : Type u} [integral_domain α] {a b c d : α}

lemma ex5d : a-b=c-d  a+d=b+c :=
begin
  split,
  {
    intro h,
    apply_fun (λ t, t+b+d) at h,
    conv at h
    begin
      to_lhs,
      rw sub_add_cancel,
    end,
    conv at h
    begin
      to_rhs,
      rw sub_add_eq_add_sub,
      rw sub_add,
      rw sub_self,
      rw sub_zero,
    end,
    have swap := add_comm c b,
    rw swap at h,
    assumption,
  },
  {
    intro h,
    apply_fun (λ t, t-b-d) at h,
    conv at h
    begin
      to_lhs,
      rw  sub_add_eq_add_sub,
      rw  add_sub,
      rw sub_self,
      rw add_zero,
    end,
    conv at h
    begin
      to_rhs,
      rw  sub_add_eq_add_sub,
      rw sub_self,
      rw zero_add,
    end,
    assumption,
  },
end

Last updated: May 13 2021 at 23:16 UTC