This PR computes triggers for :| operations ("assign such that", "let such that", binding if statements, and binding if case statements). It also improves the logic used to guess witnesses.

Main new features

• Compute trigger for all :| constructs
• For if and if-case statements with :|, output warning if there is no trigger
• For assign-such-that statements and let-such-that expressions, do not output warning, but if the proof to establish a witness fails, then include a hint in the error message that the failure may have stemmed from that no trigger was found
• In all :| constructs, support the same trigger attributes as for quantifiers, namely:
  • allow {:trigger <exprs>} to manually specify a trigger
  • allow {:trigger} to suppress any warning
  • allow {:nowarn} to change the warning into an information message

Related new features

A proof obligation associated with assign-such-that and let-such-that constructs x :| P(x) is to show that such an x exists. The general form of this is the proof obligation exists x :: P(x). However, Dafny also allows the proof obligation to be established from candidate witnesses that the verifier guesses. Thus, the proof obligation may have several disjuncts, for example:

P(0) || P(1) || exists x :: P(x)

This PR improves this machinery further; specifically:

• come up with a guess in the event that the type of x is a map
• in the event that P(x) has the form x in map[...] for some map display map[...], use the given keys as guesses (just like is done for other collection displays)
• distribute any initial disjuncts of P(x) that don't mention x to outside the existential, so that instead of exists x :: R || P(x), the proof obligation is R || exists x :: P(x) (for soundness, this is done only if the type of x is nonempty)

Notes for reviewers

The PR also contains smaller changes, namely:

• Change and/or/implies creation simplification to do more simplifications and to respect short-circuit evaluation.
• Allow BoundVar creation to indicate ghost status
• Fix pretty printing of guarded if statements to print the original :| syntax in the guard, rather than its desugaring
• Add LiteralExpr.IsFalse method
• Fix Java compiler to emit a necessary cast for map displays
• Fix compiler to support compilation of BlockByProofStmt statements
• Improve C# code in various places
• Fix typo in warning message
• Given a map type in compiler method Zero, return an empty map
• Let GuessWitnesses make more use of the Zero method

And regarding tests:

• The tests for the new features are found in triggers/TriggersForSuchThat.dfy (also relevant: wishlist/assign-such-that-antecedent.dfy)
• Many other test were updated to new expected output (in most cases to fix a typo in a warning message) or to add proof steps now that the :| constructs have specific triggers

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