Commit 2022-10-05 09:33 caf8c55f

feat(tactic/positivity): Handle a ≠ 0 assumptions (#16529) Make positivity handle a ≠ 0 assumptions. This involves

• adding a third constructor to positivity.strictness, that I've called nonzero. It is meant to hold proofs of a ≠ 0, not 0 ≠ a
• modifying the existing extensions to handle that new case.
• changing positivity.orelse' to account for the fact that if we can prove 0 ≤ a and a ≠ 0 then we can prove 0 < a.
• making compare_hyp handle eq and ne hypotheses.

Other changes

• Introduce tac1 ≤|≥ tac2 as notation for positivity.orelse' tac1 tac2. This has the same precedence as the <|> notation for orelse.
• Make positivity extensions fail with more informative error messages. This is useless when running positivity alone but:
  • It clearly marks within the code what each failure means
  • The errors can show up when calling an extension directly. Not sure why you would do that, but you could.
• Add a has_to_format strictness instance. This is mostly useful for debugging.