[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: question on dependent typing


This is essentially the same problem as before.
In c, the domain has been extended by the addition of d,
which is as you gave.  However, the value given to c in the
WITH expression should reflect its value before, so I
started by changing it to:

add(d,t) : a_type = t with [b := add(d, t`b),
                            c := {x:(add(d, t`b)) | t`c(x)}

Minor note: since you're declaring c to be a set, I used set
notation instead of a lambda.  It's just syntactic sugar, but
I find it more readable.

This leads to the unprovable TCC

add_TCC1: OBLIGATION FORALL (d, t, x: (add[int](d, t`b))): t`b(x);

The problem is that if x=d, then we can't prove that x is in
b.  So we need to exclude d:

add(d,t) : a_type = t with [b := add(d, t`b),
                            c := {x:(add(d, t`b)) |
                                    x /= d AND t`c(x)}

Now the first TCC is provable (using grind), but the second isn't:

  FORALL (d, t):
    FORALL (x1: int):
      t`b(x1) AND t`c(x1) IFF add[int](d, t`b)(x1) AND x1 /= d AND t`c(x1);

If you run grind on this, you end up with the sequent

{-1}  integer_pred(d!1)
{-2}  t!1`b(d!1)
{-3}  t!1`c(d!1)
{-4}  (x1!1 = d!1)

In a sequent like this, you need to find a contradiction in
the hypotheses.  If you stare at it for awhile, you realize
that there is no contradiction.  If d was already in b, then
it should not be excluded from the value for c (in this case
add(d, t`b) = t`b).  So the final result is

add(d,t) : a_type = t with [b := add(d, t`b),
                            c := {x:(add(d, t`b)) |
                                    (t`b(d) OR x /= d) AND t`c(x)}

and now both TCCs prove with grind.

I hope this wasn't too pedantic, I was trying to capture the
process rather than just give the final result.