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

*To*: pvs-help@xxxxxxxxxxx*Subject*: [PVS-Help] Typred with grind/ground*From*: Jonathan Ostroff <jonathan@xxxxxxxx>*Date*: Thu, 30 Jun 2016 13:37:12 -0400*Authentication-results*: symauth.service.identifier*In-reply-to*: <2CBA0709-2828-40D3-A4A1-1B44A26D6383@yorku.ca>*List-archive*: <http://mls.csl.sri.com/pipermail/pvs-help>*List-help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-id*: PVS-Help <pvs-help.csl.sri.com>*List-post*: <mailto:pvs-help@csl.sri.com>*List-subscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/listinfo/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-unsubscribe*: <https://mls.csl.sri.com/cgi-bin/mailman/options/pvs-help>, <mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*References*: <B7E71AD0-ECD4-4708-B234-F0420E1E02DF@dependablecomputing.com> <E1Zypq6-0002TF-Gn@ubi.csl.sri.com> <2CBA0709-2828-40D3-A4A1-1B44A26D6383@yorku.ca>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

I used predicate subtyping to define a type DIGIT. DIGIT: TYPE = {i: nat | i = 0 OR i = 1} CONTAINING 0 a,b,c,z: DIGIT Then, in the middle of a proof I was given the following sequent, which should have discharged automatically. [-1] (a + b + c >= 2) {-2} IF a = 1 AND b = 1 THEN 1 = d ELSE 0 = d ENDIF {-3} IF b = 1 AND c = 1 THEN 1 = e ELSE 0 = e ENDIF {-4} IF c = 1 AND a = 1 THEN 1 = f ELSE 0 = f ENDIF {-5} IF d = 1 OR e = 1 THEN 1 = g ELSE 0 = g ENDIF {-6} IF g = 1 OR f = 1 THEN 1 = z ELSE 0 = z ENDIF |------- [1] z = 1 However, without using (typepred a b c), the above would not prove. In fact, if I had done (typepred a b c) and then (grind) at a higher level, all would have proven automatically. We also could do (typepred a b c)(ground) in the above case. Is there some way to say (a) introduce all relevant type predicates whatever they are, and then (2) grind? (In this case, I knew that I needed a, b and c, but in many cases it is not obvious when ons starts out). Thanks, Jonathan |

**Follow-Ups**:**Re: [PVS-Help] Typred with grind/ground***From:*Sam Owre

**References**:

- Prev by Date:
**[PVS-Help] Latex generation problem with TABLE construct** - Next by Date:
**Re: [PVS-Help] Typred with grind/ground** - Previous by thread:
**[PVS-Help] Latex generation problem with TABLE construct** - Next by thread:
**Re: [PVS-Help] Typred with grind/ground** - Index(es):