Add a symmetric version of conv

Using sym in core trellys is painful because you have to fully type
annotate it.  The built in conv converts left to right.  Adding
another conv that converts right to left would eliminate any need for
sym, and would be much easier to use (by hand).

More precisely, let convlr be the current conv, then

  convlr : A -> (A = B) -> B

and I'm proposing adding a

  convrl : A -> (B = A) -> B

Now, this new convrl is technically unnecessary, and maybe useless
once we're compiling to trellys core from a surface language, but it
also provides an intermediate step in solving another problem:
backwards generated equalities.

Tim has suggested that most sym usage is due to equality proofs
generated in case matches being backwards: the equalities are from
general (on the left) to specific (on the right), but each case-match
body is specific, and must be conv'd to the general type of the whole
case expression.

For example, from NatElimination.trellys:

  -- Higher-order primitive recursion / nat
  -- elimination. Cf. Vecters.recvec.
  primrec : [p: (n:Nat) -> Type 0]
         -> (base:p 0)
         -> (step: (n:Nat) -> (pn:p n) -> p (Succ n))
         -> (n:Nat) -> p n
  primrec = \[p]. \base. \step. recnat pr n =
    case n [neq] of
      -- sym is evidence of backwards equality.
      Zero    -> conv base                  
                 by (sym Nat Nat n Zero      neq) 
                 at x.p x
      Succ n' -> conv step n' (pr n' [neq]) 
                 by (sym Nat Nat n (Succ n') neq) 
                 at x.p x

The problem is that neq : (n = Zero) or (n = Succ n'), whereas we want
to convert from Zero or Succ n' to n.

Changing trellys's generated equalities would be pretty easy, but it
would break much existing code.  However, if we added convrl and then
flipped the generated equalities, we could simply search and replace
all conv with convrl, and existing code would continue to work.  Then,
going forward, we could avoid usage of convrl if possible.  Later, if
it turned out we rarely needed convrl we could remove convrl.
Original issue reported on code.google.com by nathan.c...@gmail.com on 1 Jan 2011 at 3:55
sweirich / trellys

Add a symmetric version of conv #11
