Ability to use sets in forall and exists

[byorgey]

We have considered and rejected some ideas to broadly identify types and sets (#290, #282, #348). However, I wonder if there are some more limited things we could do that would be convenient. One such idea is to allow using finite set values as the domain of a forall or exists (perhaps using a different syntax to distinguish them). Like this:

A : Set(N)
A = {1 .. 10}

b : Bool
b = forall a in A. a^2 <= 100

As opposed to forall x : T. e where T must be a type and the whole expression has type Prop, forall x in X. e would have the same type as e as long as X : Set(T) and e has type Bool or Prop under the assumption x : T.

This would certainly be convenient. Right now even if you write something like forall x : N. (x <= 10) -> ... it will still try a bunch of values of x greater than 10, and it won't be able to tell you that it has exhaustively tested all the possibilities. On the other hand this might just be confusing for students.

[byorgey]

Started thinking about this a bit. I immediately ran into the issue of how to represent this in the syntax: right now we unify lambdas, forall, and exists under the same umbrella, and binders are patterns. If we just allow this anywhere we could have stuff like \x in A. ... but I'm not sure what that should mean.

[byorgey]

What if we just make x in A be a pattern, which matches (binding x) on anything which is an element of A. Then \x in A. ... would actually make sense although we wouldn't really want to use it, I suppose.

Hmm... we would need to allow <var> in <expr> as a pattern, where <expr> could be any expression, not just a pattern. If e : Set(T) then x in e : T. Matching against x in e would desugar to something that evaluated e exactly once, binding the result to y, then used a guard with x elem y.

[byorgey]

I now have parsing and desugaring working in the feature/quantify-over-sets branch. However, testing doesn't work, and indeed, quantifiers with patterns don't really work at all. Currently, with the default desugaring, forall P(x). Q desugars to something like forall y:T. {? Q when y is P(x) ?} (where T is the type of the pattern P(x)), which does not have the right semantics. (exists has the same issue.) For example, forall x in {1,2,3}. x < 5 just tries all natural numbers and crashes when it happens to try a natural number that is not in the set {1,2,3}.

Clearly we need to treat patterns under forall and exists differently than patterns under lambdas. Should this happen in the desugarer?