"where" clauses to give substitutions

[John Tang Boyland]

One of the more confusing things with proofs and with SASyLF is that a successful pattern match can cause a substitution to be applied to the input variables. While SASyLF will still keep track of the input variable's name (and its substitution), the user might not realize and cannot see the substitution. This makes new extensions such as "use inversion of eq on ..." mysterious, and even original SASyLF case rule will cause non-local effects.

Thus I propose that every inversion or case analysis be able to specify the substitutions with a where clause

  case rule
          e1': t0 -> t0'
          --------------------------- E-If
          _: if t0 then t1 else t2 -> if t0' then t1 else t2
    where t := if t0 then t1 else t2
    and  t' := if t0' then t1 else t2

For inversions, the where clause would be added after the resulting premises (if any) leaving syntax such as:
where t0 := t0' by inversion of eq on e2

If a flag --explicit is given, then lacking the where clauses would cause a warning. In the Eclipse plugin, a "Quick Fix" would be able to insert them.

[JonathanAldrich]

That makes sense to me!

[Michael Ariotti]

Hello! I am new to SASyLF, and am taking a type systems class with Dr. Boyland. I am also hoping to add some features to SASyLF as part of my studies (separate from the class).

I like this idea in general. I found myself making notes like this in comments (or on paper) when writing proofs about natural numbers. This would be especially helpful with nested case analyses, where multiple terms or propositions can be fixed to some (more) concrete value, depending on a given position in the code structure.

One potential downside is that I can see this taking up a lot of room in the code. In Eclipse at least, it might be helpful if these clauses could be collapsed/hidden away, or if such substitutions could be revealed in a tooltip somehow (sort of like what you get when hovering over "proof by unproved"; very helpful messages!). Forcing a student like me to write these where clauses himself from the outset, however, would probably make writing proofs with SASyLF easier to learn.