How do I get lamdas to apply outside of a lemma

Stream: new members

[Lars Ericson]

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.

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

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

[Lars Ericson]

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

[Adam Topaz]

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

[Lars Ericson]

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.

[Eric Wieser]

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

[Lars Ericson]

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