Zulip Chat Archive

Stream: new members

Topic: apply a term to all assumptions?


view this post on Zulip Chris M (Jul 22 2020 at 04:32):

The following is a working proof, but it's slightly verbose to have to apply ` to hfa, hfb, nng separately. Is it possible to just say: "apply x` to all assumptions"?

import data.real.basic
import tactic

example (hfa : fn_ub f a) (hfb : fn_ub g b)
    (nng : fn_lb g 0) (nna : 0  a) :
  fn_ub (λ x, f x * g x) (a * b) :=
begin
  dunfold fn_ub fn_lb at *,
  intro x,
  have h1:= hfa x,
  have h1:= hfb x,
  have h3:= nng x,
  nlinarith
end

view this post on Zulip Alex J. Best (Jul 22 2020 at 04:48):

This doesn't exactly answer your question, but you can do

example (hfa : fn_ub f a) (hfb : fn_ub g b)
    (nng : fn_lb g 0) (nna : 0  a) :
  fn_ub (λ x, f x * g x) (a * b) :=
begin
  dunfold fn_ub fn_lb at *,
  intro x,
  nlinarith [hfa x, hfb x, nng x],
end

to avoid typing have a lot

view this post on Zulip Chris M (Jul 22 2020 at 04:50):

Yeah that's good but not exactly what I was after.
In fact, it would be nice to replace hfa, hfb, nng with hfa x, hfb x, nng x respectively, so that one has a cleaner goal state.

view this post on Zulip Alex J. Best (Jul 22 2020 at 04:51):

For that you can use specialize

example (hfa : fn_ub f a) (hfb : fn_ub g b)
    (nng : fn_lb g 0) (nna : 0  a) :
  fn_ub (λ x, f x * g x) (a * b) :=
begin
  dunfold fn_ub fn_lb at *,
  intro x,
  specialize hfa x,
  specialize hfb x,
  specialize nng x,
  nlinarith,
end

Last updated: May 08 2021 at 09:11 UTC