RFE: and judgments

[John Boyland]

Now that "and" is a reserved word, I'd like (not urgently) SASyLF to
support "and" predicates:
basically any number of judgments can be joined by "and". This would
replace things like

judgment extended: M{n} = T /\ Gamma;M |- m:M /\ M >= M

M'{n} = T
Gamma; M' |- m' : M'
M' >= M
--------------------------------------- extended-def
M'{n} = T /\ Gamma; M' |- m':M' /\ M' >= M


lemma allocate-preserves-extended:
forall o: Gamma; M |- m : M
forall d: Gamma; M |- t : T
forall a: m <- t = loc n!m'
exists M'{n} = T /\ Gamma;M' |- m':M' /\ M' >= M .
...
end lemma

Problems with tghis is that one has to declare this judgment in the
judgment section (not close to the lemma) and the judgment is
basically boilerplate. The only problem is remembering the name of
the rule. So with this proposal, one would write:

lemma allocate-preserves-extended:
forall o: Gamma; M |- m : M
forall d: Gamma; M |- t : T
forall a: m <- t = loc n!m'
exists M'{n} = T and Gamma;M' |- m':M' and M' >= M .
...
end lemma

There would be very little syntactic help[ for this. One would still
need to write things like:

_: M'{n} = T and Gamma;M' |- m':M' and M' >= M by case analysis
on d: ...

The easiest way for this to be done in SASyLF (I think!) would be to
have a polymorphic and rule:

x: a > b
y: b > c
z: a > b and b > c by rule and on x,y

Slightly nicer would be

z: a > b and b > b by x,y

To use such values, one could either (less sugar) allow normal case
analysis on and:

... by case analysis on z:
case rule
x: a > b
y: b > c
----------------------- and
_: a > b and b > c
is

But somewhat nicer would be something like

x: a > b by and inversion 1 on z
y: b > c by and inversion 2 on z

....

"or" could be handled by having rules or-1, or-2 etc generated
automatically.

[Jonathan Aldrich]

John,

Thanks a lot for your proposal...the existing workaround is indeed
somewhat annoying boilerplate. This is definitely on my list, but so
far stability and a basic feature set have come first. Your specific
examples and ideas about syntax is also very helpful...I will reply in
more detail when I get a chance.

Please keep the ideas coming!

Jonathan