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

*To*: Jonathan Ostroff <jonathan@xxxxxxxx>*Subject*: Re: [PVS-Help] Typred with grind/ground*From*: Sam Owre <owre@xxxxxxxxxxx>*Date*: Thu, 30 Jun 2016 12:41:37 -0700*Cc*: pvs-help@xxxxxxxxxxx*Comments*: In-reply-to Jonathan Ostroff <jonathan@xxxxxxxx> message dated "Thu, 30 Jun 2016 13:37:12 -0400."*In-reply-to*: <A7DE6813-3F17-4801-92A6-C8C6AFCB82A8@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> <A7DE6813-3F17-4801-92A6-C8C6AFCB82A8@yorku.ca>*Sender*: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Jonathan, Look into all-typepreds - it should do what you want. Regards, Sam Owre Jonathan Ostroff <jonathan@xxxxxxxx> wrote: > 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:*Jonathan Ostroff

**References**:**[PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand****From:*Ben Hocking

**Re: [PVS-Help] Defining a strategy that takes a list as an argument and uses it with expand****From:*Sam Owre

**[PVS-Help] Latex generation problem with TABLE construct***From:*Jonathan Ostroff

**[PVS-Help] Typred with grind/ground***From:*Jonathan Ostroff

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