extensible `contradiction` tactic

Stream: lean4

[Asei Inoue]

Currently, no preprocessing can be added to the contradiction tactic. Thus, for example, even if a ≤ b and a > b are assumed, contradiction does not immediately close the goal.

Currently, this type of rule can be handled by simp. So, if we create a simp wrapper using register_simp_attr, we can make the contradiction tactic extendable with @[contradiction] tag. Implementation would probably be easy.

Is this a good idea? Let me know what you think.

[Asei Inoue]

Compared to simply registering in the simp rules, this would have the advantage of being easier to read and understand.

[Robin Arnez]

I don't think contradiction per se should be extensible, it's supposed to be a very fast tactic and adding too much would decrease performance. It might be better to use tactics that were made for specific circumstances, e.g. something like linarith or order perhaps for what you suggest here. As an example,linarith is also a tactic that tries to find a contradiction but in a more sophisticated way. Otherwise, you could make your own tactic which aims to be a slower but more powerful contradiction which maybe does simple preprocessing and then calls contradiction. Not sure how useful that'd be though

[Jovan Gerbscheid]

(deleted)

[Kyle Miller]

Possibly the future of a powerful contradiction will be the in-development grind tactic. #rss > Recent Commits to lean4:master @ 💬