run tactic for x in list

Stream: general

[Johan Commelin]

I have the following tactic state:

abcd: ℝ
hd0: 0 < d
hdc: d ≤ c
hcb: c ≤ b
hba: b ≤ a
h1: a + b + c + d = 1
⊢ (a + 2 * b + 3 * c + 4 * d) * a ^ a * b ^ b * c ^ c * d ^ d < 1

I want to lift a, b, c, and d to nnreal. How do I do that? I feel like there could be a useful tactic similar to repeat and friends.

[Johan Commelin]

I tried do [`a, `b, `c, `d].mmap (λ x, `[lift x to nnreal, swap, linarith]) but this is entirely cargo-cult tactic hacking.

[Johan Commelin]

It would be nice if we could write something like

for x in [`a, `b, `c, `d], { lift %%x to nnreal, swap, linarith }

modulo syntax errors

[Anne Baanen]

Do antiquotations work in tactic quotations?

do [`a, `b, `c, `d].mmap (λ x, `[lift %%x to nnreal, swap, linarith])

[Johan Commelin]

The do also seems to kick me out of interactive mode

[Johan Commelin]

If I end that line with a , then I can't do ordinary tactic proving after it.

[Johan Commelin]

Also, the do-line gives the error

don't know how to synthesize placeholder
context:
a b c d : ℝ,
hd0 : 0 < d,
hdc : d ≤ c,
hcb : c ≤ b,
hba : b ≤ a,
h1 : a + b + c + d = 1
⊢ Type

[Mario Carneiro]

you have to put the entire do block in parentheses, or else the comma will continue the do block instead of the tactic block

[Mario Carneiro]

actually I think you can just leave off the do in anne's version

[Mario Carneiro]

#mwe

[Johan Commelin]

([`a, `b, `c, `d].mmap (λ x, `[lift %%x to nnreal, swap, linarith])),

gives the error

Failed to find a lift from name to nnreal. Provide an instance of
  can_lift name nnreal

[Johan Commelin]

So I must have some of the backticks and %% wrong

[Johan Commelin]

MWE:

import data.real.nnreal

example (a b c d : nnreal)
  (hba : b ≤ a)
  (hcb : c ≤ b)
  (hd0 : 0 < d)
  (hdc : d ≤ c)
  (h1 : a + b + c + d = 1) :
  a + 2 * b + 3 * c + 4 * d ≤ a + 3 * b + 3 * c + 3 * d :=
begin
  -- lift `a,b,c,d` to `nnreal` in a one liner...
end

[Anne Baanen]

I don't have Lean in front of me. Does this help?

([`(a), `(b), `(c), `(d)].mmap (λ x, `[lift %%x to nnreal, swap, linarith])),

[Mario Carneiro]

wait, can't lift nnreal to nnreal?

[Mario Carneiro]

your mwe was wrong

example (a b c d : ℝ)
  (hba : b ≤ a)
  (hcb : c ≤ b)
  (hd0 : 0 < d)
  (hdc : d ≤ c)
  (h1 : a + b + c + d = 1) :
  a + 2 * b + 3 * c + 4 * d ≤ a + 3 * b + 3 * c + 3 * d :=
begin
  ([```(a),```(b),```(c),```(d)].mmap $ λ x,
    `[lift %%x to nnreal, swap, linarith]),
  -- lift `a,b,c,d` to `nnreal` in a one liner...
end

[Anne Baanen]

Ah, triple-backquote.

[Johan Commelin]

Ooh, I had tried ``` , but without the ().

[Anne Baanen]

My reasoning to use `(a) was that `a gives a name and the error complained about name.

[Mario Carneiro]

See also https://leanprover-community.github.io/extras/tactic_writing.html#marios-backtick-cheat-sheet

[Johan Commelin]

I feel like this syntax isn't optimized for one-off hacks like this

[Johan Commelin]

As in, we probably wouldn't want this one-liner ending up in mathlib

[Mario Carneiro]

eh, it's fine

[Johan Commelin]

I wouldn't mind having something with less sigils

[Mario Carneiro]

it used to be single backtick but the assignments got swapped around

[Mario Carneiro]

because the expr version seemed more useful

[Mario Carneiro]

I'm sure lean 4 is doing something else

[Mario Carneiro]

alternatively:

  (do lc ← tactic.local_context, lc.mmap' $ λ x,
    `[try {lift %%x to nnreal, swap, linarith}]),

[Johan Commelin]

That certainly has fewer backticks :thumbs_up: