Equality

Equality in ask

This feature is not yet implemented, but I'm hoping that trying to write the documentation will help me design it.

Equations are written lhs = rhs, and they live in type Prop.

Now because ask supports constructor overloading — a symbol may be a constructor of more than one type — it's not terribly helpful to write an equation between two constructor-headed terms. If you can (and you indeed can) avoid writing such equations, then ask will infer the type from one side and check the type of the other. Be assured that ask knows that constructors are injective and disjoint, so the only way that C s1 ... sn = D t1 ... tm can ever be true is if D is C, m is n and si = ti for i in 1 .. n. Correspondingly, constructor-constructor equations are always unpacked, whether as subgoals or as hypotheses.

Meanwhile, ask also has functions, so we admit

prove (=)@(s -> t) f g by FunExt where
  given x :: s prove f x = g x

not to mention propositions themselves, so we have

prove (=)@Prop p q by Equiv where
  given p prove q
  given q prove p

I'm using @ as the manual override for arguments usually left implicit. It's not unusual to write equivalences between constructor-headed propositions, so we take (<=>) = (=)@Prop to spare our blushes.

A further key rule is

prove p as q where
  prove q
  prove p = q

Now, with a bit of a stretch of the parser, we can allow multiple step equality proofs

prove t0
    = t1 method1 where
      justification1
    = t2 method2 where
      justification2
    ...
    = tn methodn where
      justificationn

which is seen as a justification of t0 = tn. An equation is given if its structural mismatches can be repaired by equations which are given, up to symmetry. Note that for non-constructor forms, we should check if equations between wholes are given before checking the parts. E.g., if we want to see whether x + y = a + b is given, we should look for x + y = a + b and a + b = x + y before resorting to seeing if x = a and y = b are given, because the latter is not the only way the equation can be proven. The upshot of this is that you can make an equation obvious by proving it in a handy local where clause and ask will figure out where to slot it in.

Here's another funny thing: ask allows you to fix up types by proving equations. If ever ask infers a type s while checking type t, it will demand a proof of s = t! Operationally, it plugs in a coercion operator from s to t which computes only when they have matching head constructors.