linarith argument parsing

Stream: general

[Rob Lewis]

While making some changes discussed in the -T50000 thread, I realized the linarith argument parsing is wrong:

constant f : ∀ x : ℤ, 0 < x
example (a : ℤ) (h : a ≤ 0) : false := by linarith h using [f a]

fails, I guess because using is confused for an identifier.

This is the opportunity to suggest a better pattern. I was thinking linarith [t1, t2, t3] could replace the current linarith using [t1, t2, t3], and linarith only [h1, h2, h3, t1, t2, t3] could be a working version of linarith h1 h2 h3 using [t1, t2, t3]. The only problem: linarith h1 h2 h3 doesn't include the goal by default, and I wanted to add |- for the option to do that. But linarith only [h1, h2, h3, |-] is a pattern we don't use anywhere else.

[Rob Lewis]

Any better ideas?

[Mario Carneiro]

why not always include the goal?

[Rob Lewis]

Just because, if the user says to only use certain hypotheses, it feels presumptuous to throw in the goal anyway. It's possible using the goal could slow things down. Although probably pretty rarely.

[Rob Lewis]

As far as the notation goes, that's the cleanest solution.

[Rob Lewis]

And I guess if you really don't want the goal then exfalso; linarith only [h1, h2] will get rid of it.

[Mario Carneiro]

It seems like the goal is the primary indicator of what it is you are trying to show

[Mario Carneiro]

the hypotheses are just a big grab bag by comparison

[Mario Carneiro]

I'm not even sure that using exfalso when the goal isn't an inequality is a good idea

[Rob Lewis]

There's a config option for that. I believe it was requested early on that the default should be exfalso := tt.

[Rob Lewis]

Incidentally, I was wrong at the start of the topic, by linarith h using [f a] parses just fine. It was a dumb mistake that was causing the failure.

[Rob Lewis]

I still like the look of linarith only [h, f a] though.