From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: *
X-Spam-Status: No, score=1.7 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM,FREEMAIL_REPLYTO,REPLYTO_WITHOUT_TO_CC autolearn=no
	autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,c032b2e4ea2d28a0
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.181.11.234 with SMTP id el10mr3223037wid.2.1347408891501;
        Tue, 11 Sep 2012 17:14:51 -0700 (PDT)
Path: 
 q11ni19572293wiw.1!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!94.232.116.11.MISMATCH!feed.xsnews.nl!border-1.ams.xsnews.nl!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border2.nntp.dca.giganews.com!border3.nntp.dca.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!newsgate.cuhk.edu.hk!goblin2!goblin.stu.neva.ru!news.stack.nl!dedekind.zen.co.uk!zen.net.uk!hamilton.zen.co.uk!reader01.nrc01.news.zen.net.uk.POSTED!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Proving B given that A >= 0 -> B and A < 0 -> B
Date: Tue, 4 Sep 2012 09:43:30 +0100
Message-ID: <MPG.2aafcf90a84312cc98969e@news.zen.co.uk>
References: <c05c6143-cbde-4916-8655-e16197981997@googlegroups.com>
Reply-To: phil.jpthornley@gmail.com
MIME-Version: 1.0
User-Agent: MicroPlanet-Gravity/3.0.4
Organization: Zen Internet
NNTP-Posting-Host: 3fb07317.news.zen.co.uk
X-Trace: 
 DXC=PL[_\0lZnWLI>27fALHYIJa0UP_O8AJoL=dR0\ckLKG@WeZ<[7LZNRF?lSQE90f19JUhLi?]0KG=Ki;3N437AmfBkML7B7EO:hJ
X-Complaints-To: abuse@zen.co.uk
Content-Type: text/plain; charset="iso-8859-15"
Content-Transfer-Encoding: 8bit
Date: 2012-09-04T09:43:30+01:00
List-Id: <comp.lang.ada>

In article <c05c6143-cbde-4916-8655-e16197981997@googlegroups.com>, 
benjaminhocking@gmail.com says...
> 
> I've run into this scenario a couple times and I have yet to come up with a simple solution. I have the following rule in my .rlu file:
>   combine_cases2: PREDB may_be_deduced_from [A >= 0 -> PREDB, A < 0 -> PREDB, goal(checktype(A, number))].
> (Evidently there's no boolean type in prolog, so I can't assert that PREDB is of type boolean. Correct me if I'm wrong on that.)
> 
> Unfortunately, this rule doesn't seem to be helping me on the following:
> ?
> H15:   x - a * (y - z) div b >= 0 -> 
>           my_fn(x - a * (y - z) div b)  <= c .
> H16:   x - a * (y - z) div b < 0 -> 
>           my_fn(x - a * (y - z) div b)  <= c .
> ?
>        ->
> C1:    my_fn(x - a * (y - z) div b) <= c .

The only thing I can see that might stop this rule working is if the 
expression in the lhs of the implications is not of type Number. (To 
confirm this look in the .fld file for the declarations for x, y, etc.)

I don't think that checking the type of PREDB as Boolean is necessary as 
it can only ever be matched to a boolean expression in a VC (assuming 
correct operation of the Examiner/Simplifier of course).

> 
> I'm also open to solving this problem using "checker", but I'm not sure what rules I would use on the .siv file, either.

You don't need any user rules to prove this VC in the Proof Checker, 
just try the commands:

prove c#1 by cases on A>=0 or A<0 where h#15=(A>=0 -> B).
simplify. (or: forwardchain h#15.)
done.
simplify. (or: forwardchain h#16.)
done.

Cheers,

Phil