Context for multiple examples

Stream: new members

[Gunnar Mein]

(if you are easily annoyed by what people do with your beautiful work, please look the other way for 5 minutes - thanks!)

I am trying to find a way to build up context that I can reuse in multiple examples, but I can't figure out how (or if it is possible). Here is what works:

import data.real.basic

variables s x t : real

example
(h1: s = 75)
(h2: x = s*t)
(h3: t = 1)
:
x = 75 :=
by nlinarith

But I would think that there is possibly some way to reuse h1, h2, h3 and have linarith still find them for another example:

axiom a1: s = 75
axiom a2: x = s*t
axiom a3: t = 1

example :
x = 75 :=
by nlinarith

example :
x > 70
by nlinarith

Thanks for any thoughts!

[Mario Carneiro]

It sounds like you want the variables command?

[Eric Wieser]

Along with possibly the include command

[Gunnar Mein]

Consider the second example part of the first script, so "variables" are declared.

[Kyle Miller]

They mean that you can have the hypotheses be variables, too.

[Kyle Miller]

import data.real.basic

variables (s x t : ℝ)
  (h1: s = 75)
  (h2: x = s*t)
  (h3: t = 1)

include h1 h2 h3

example : x = 75 :=
by nlinarith

[Gunnar Mein]

@Kyle tried that but it didn't do anything. But just found "include" in the docs, thank you!

[Kyle Miller]

If you want to misuse Lean, you can also have each example be a have block inside a tactic proof:

import data.real.basic

variables (s x t : ℝ)

example
  (h1 : s = 75)
  (h2 : x = s * t)
  (h3 : t = 1) :
  true :=
begin
  have : x = 75,
  { nlinarith },
  have : x > 70,
  { nlinarith },

  trivial
end

[Gunnar Mein]

Oh, that's pretty (or gross, depending on where you stand). I am looking for slight performance gains for verifying multiple steps in a calculation, will try that, thanks!

[Mario Carneiro]

None of these techniques will help with performance of nlinarith, it doesn't reuse work between invocations

[Mario Carneiro]

If you want to improve performance the simplest thing to do is not use nlinarith or find out what more targeted tactics work

[Gunnar Mein]

And I guess the added downside is that LEAN will stop processing a begin/end block when a tactic fails, but it will go on to other examples.

[Mario Carneiro]

it processes proofs in parallel too