positivity with arguments

Stream: Is there code for X?

[Jireh Loreaux]

It seems that positivity does not accept a list of additional terms to use in proving the goal. I thought this had been implemented at some point. Am I wrong? It is very inconvenient to be forced to do have := foo; have := bar, just in order to do positivity, instead of positivity [foo, bar]. Also, I found out that positivity can't use hypotheses of the form ∀ x : α, 0 ≤ x. I assume the reasons for this are all performance-related.

[Yaël Dillies]

No, it never was implemented but there is an issue: #2427

[Jireh Loreaux]

okay, thanks for the pointer. I'll maybe look into the first one soon. What about the ∀?

[Yaël Dillies]

The ∀ is a thorny issue. I have thoughts, or at least I had thoughts six months ago, so maybe let me sleep on it and I can comment more precisely