Implement a proof-by-contradiction attribute

[atomb]

Description

Allows a particular assertion to be marked as an intentional proof by contradiction, preventing --warn-contradictory-assumptions from flagging it.

Fixes #4778

How has this been tested?

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4778.dfy

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[MikaelMayer]

Interesting and useful. Could you perhaps do two things:

• When you report "proved by contradictory assumptions", could you also mention this {:contradiction} attribute so that it's easy to discover?
• Add one more line in docs/dev/news about that new attribute
• Add a line about the documentation of this new attributes in docs/DafnyRef/Attributes.md

[keyboardDrummer]

Could you document the attribute in the help of the --warn-contradictory-assumptions option?

[MikaelMayer]

Looks great! This is a good answer to the problem of being able to assert intermediate steps when the hypotheses already contradict.
I note that it won't help for preconditions in lemmas though, correct?

[atomb]

Looks great! This is a good answer to the problem of being able to assert intermediate steps when the hypotheses already contradict. I note that it won't help for preconditions in lemmas though, correct?

Are you thinking of the use case of trying to show that A and B are inconsistent using a lemma? So you'd write something like:

lemma L():
  requires A
  requires B
  ensures false
{}

If that's what you mean, then no, this PR doesn't support that use case. Perhaps it would be possible to allow the same attribute on an ensures clause, though, which would allow that.