Zulip Chat Archive

Stream: general

Topic: linarith argument parsing


view this post on Zulip 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.

view this post on Zulip Rob Lewis (May 19 2019 at 13:49):

Any better ideas?

view this post on Zulip Mario Carneiro (May 19 2019 at 13:53):

why not always include the goal?

view this post on Zulip 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.

view this post on Zulip Rob Lewis (May 19 2019 at 13:58):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 19 2019 at 14:03):

the hypotheses are just a big grab bag by comparison

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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