Re: Proving B given that A >= 0 -> B and A < 0 -> B

[Phil Thornley <phil.jpthornley@gmail.com>]

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