Equations

Proving Equations

Old ask had equational reasoning as an afterthought, with other propositional connectives taking developer priority. It's a bit rough around the edges, to put it mildly. Key criticisms might well include:

• we would use the test strategy to request computation in accordance with definition and get more computation than we wanted;
• constructing a chain of equational steps involved the highly confusing Route rule, and got very wide very quickly;
• the fact that equality is a congruence was very awkwardly handled via the under strategy.

It's my view that addressing the ergonomics and legibility of equational proof is the single most important improvement I need to make.

Here's an old ask proof

proven a * (b + c) = a * b + a * c inductively b where
  proven a * (b + c) = a * b + a * c from b where
    given b = S x proven a * (S x + c) = a * S x + a * c tested where
      proven a + a * (x + c) = (a + a * x) + a * c
        by Route (a + (a * x + a * c)) where
        proven a + a * (x + c) = a + (a * x + a * c)
          under (+)

What would I like to write?

proven a * (b + c) = a * b + a * c inductively b where
  proven a * (b + c) = a * b + a * c from b where
    given b = S x, forall a c. a * (x + c) = a * x + a * c
      proven a * (S x + c)
           = a + [a * (x + c)]
           = a + [a * x + a * c]
           = [a + (a * x + a * c)]
           = [(a + a * x) + a * c]
           = a * S x + a * c 

Yes, it's longer, but it's way more scrutable, even before you know the following:

• square brackets [..] enclose subexpressions in focus
• an equational step may be "refocusing", allowing computation by definition and re-placement of focus (such steps are checked by ignoring foci and testing definitional equality)
• an equational step may be "rewriting", replacing subexpressions in focus by others to which they are provably equal

Once more, with commentary.

proven a * (b + c) = a * b + a * c inductively b where
  proven a * (b + c) = a * b + a * c from b where
    given b = S x,
          forall a c. a * (x + c) = a * x + a * c
          -- ask would never tell you the induction hypothesis
          -- and that was unpleasant cognitive loading
      proven a * (S x + c)
          -- refocus computing + and *
           = a + [a * (x + c)]
          -- rewrite by induction hypothesis
           = a + [a * x + a * c]
          -- refocus
           = [a + (a * x + a * c)]
          -- rewrite by associativity
           = [(a + a * x) + a * c]
          -- refocus computing *
           = a * S x + a * c 

It's ok to have multiple nonoverlapping foci. Rewriting steps should preserve what's not in focus and ensure that the subtems in corresponding foci are provably equal by exact substitution instances of known facts.

Another example. Old

proven (a * b) * c = a * (b * c) inductively c where
  proven a * b * c = a * (b * c) from c where
    given c = S x proven a * b * S x = a * (b * S x) tested where
      proven a * b + (a * b) * x = a * (b + b * x)
        by Route (a * b + a * (b * x)) where
        proven a * b + (a * b) * x = a * b + a * (b * x)
          under (+)

becomes

proven (a * b) * c = a * (b * c) inductively c where
  proven (a * b) * c = a * (b * c) from c where
    given c = S x, forall a b. (a * b) * x = a * (b * x)
      proven (a * b) * S x
           = a * b + [(a * b) * x]
           = a * b + [a * (b * x)]
           = [a * b + a * (b * x)]
           = [a * (b + b * x)]
           = a * (b * S x)

We seem to hit a pattern where we refocus between rewrites with no definitional computation. It might make sense to allow both foci. So

           =  a + [a * (x + c)]
           = [a + [a * x + a * c]]
           = [(a + a * x) + a * c]

and

           =  a * b + [(a * b) * x]
           = [a * b + [a * (b * x)]]
           = [a * (b + b * x)]