## Stream: general

### Topic: linarith argument parsing

#### Rob Lewis (May 19 2019 at 13:49):

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 (May 19 2019 at 13:49):

Any better ideas?

#### Mario Carneiro (May 19 2019 at 13:53):

why not always include the goal?

#### Rob Lewis (May 19 2019 at 13:58):

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 (May 19 2019 at 13:58):

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

#### Rob Lewis (May 19 2019 at 13:59):

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

#### Mario Carneiro (May 19 2019 at 14:03):

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

#### Mario Carneiro (May 19 2019 at 14:03):

the hypotheses are just a big grab bag by comparison

#### Mario Carneiro (May 19 2019 at 14:04):

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

#### Rob Lewis (May 19 2019 at 14:22):

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

#### Rob Lewis (May 19 2019 at 14:24):

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 (May 19 2019 at 14:24):

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

Last updated: May 11 2021 at 13:22 UTC