Allow passing functions to `forall` and `exists`

[keyboardDrummer]

Summary

Allow passing unapplied functions to forall and exists, to reduce the learning curve for using forall and exists expressions.

Background and Motivation

The syntax for forall and exists expressions, forall x: int | Q(x) :: Z(x), does not extend from other syntax in the Dafny language, so Dafny users need to learn and remember this syntax just for using those quantifiers.

Secondly, a quantifier instantiation can create terms that lead to new instantiations, and this can negatively affect performance. By hiding a function P, we can be sure that instantiating forall P for a particular P(x) does not lead to further instantiations.

Proposed Feature

Given

predicate Z(x: int)
predicate P(x: int) requires Q(x) {
  Z(x)
}

Allow writing

lemma ForallP() ensures forall P

which would have the same meaning as

lemma ForallP() ensures forall x: int | Q(x) :: Z(x)

---

This idea needs more work, but we could also consider allowing assert P; to mean assert forall P;, and we could consider letting hide P then preventing the entire forall from being instantiated.

Alternatives

No response