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

*To*: Kurt Lichtner <kurt@csg.uwaterloo.ca>*Subject*: Re: question on dependent typing*From*: Sam Owre <owre@csl.sri.com>*Date*: Wed, 24 Nov 1999 11:56:23 -0800*cc*: Sam Owre <owre@csl.sri.com>*Delivery-Date*: Wed Nov 24 11:55:41 1999*In-reply-to*: Your message of "Wed, 24 Nov 1999 09:09:27 EST." <383BF197.7A7AADF6@csg.uwaterloo.ca>

Kurt, 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: add_TCC2: OBLIGATION 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. Regards, Sam

**References**:**Re: question on dependent typing***From:*Kurt Lichtner <kurt@csg.uwaterloo.ca>

- Prev by Date:
**Re: question on dependent typing** - Next by Date:
**interactive and automatic** - Prev by thread:
**Re: question on dependent typing** - Next by thread:
**inspecting goal in strategy** - Index(es):