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

[Ben Hocking <benjaminhocking@gmail.com>]

On Monday, September 3, 2012 10:19:28 AM UTC-4, Ben Hocking wrote:
> 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 .
> 
> 
> 
> 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.
> 
> 
> 
> Thanks for any help or insight.
> 
> 
> 
> -Ben

Thanks, Phil.

That worked for me. I thought there should be some sort of command like "simplify." but I didn't remember it or hadn't encountered it yet.

-Ben