Commit 2024-02-12 13:42 5bb66741

refactor(Tactic/Positivity): use stricter Qq matching (#10196) The previous code often discarded the safety features of Qq by casting quoted terms to Expr and back. This is far from an exhaustive replacement. This makes use of a bug fix in Lean 4.6.0rc1 that allows us to write things like

match u, α, e with
| 0, ~q(ℤ), ~q(@Int.floor $α' $i $j $a) =>

Previously these matches did not generalize u correctly. To make Qq happy, we introduce a few more assertInstancesCommute that were not previously here. Without them, there is a higher risk that positivity produces an ill-typed proof in weird situations. Like every assertInstancesCommute, this comes at a small performance cost that could be eliminated by using the unsafe assumeInstancesCommute instead. Another very small performance hit here is from the (possibly unnecessary) defeq check of the types before checking defeq of the values. On the other hand, this might actually increase performance when the match fails due to a type mismatch. There is probably some boilerplate that can be extracted from the repetition here; but I am declaring that out of scope for this PR: the goal is to establish a canonical spelling for this sort of matching, so that future extensions copy-pasted from these extensions inherit the spelling automatically.