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

Re: [PVS-Help] Very slow proveit/PVS proofs



Hi Sam,

That worked perfectly with my full regression test. All existing proofs worked, and the lookup table proofs worked quickly. As for the smooth_is_bounded proof, I had no reason to expect (grind) to work other than it's almost always my first strategy of choice (I'm lazy that way). This was the proof I ultimately used:
(skeep)
(expand "smooth")
(expand "min")
(expand "max")
(case "new_val > old_val")
(("1"
  (case "divisor < 1")
  (("1" (split) (("1" (lift-if) (grind)) ("2" (grind))))
   ("2"
    (grind)
    (("1"
      (field)
      (field 2)
      (grind)
      (case "divisor >= 1")
      (("1"
        (hide -2 1)
        (field)
        (case "(divisor - 1) * old_val <= (divisor - 1) * new_val")
        (("1" (field)) ("2" (hide 2) (field))))
       ("2" (smash))))
     ("2" (field 2))))))
 ("2"
  (grind)
  (("1" (field 3))
   ("2"
    (field 3)
    (case "divisor >= 1")
    (("1"
      (hide -2 2)
      (case "(divisor - 1) * new_val <= (divisor - 1) * old_val")
      (("1" (field)) ("2" (field))))
     ("2" (smash))))))))

Probably not as elegant as you would've done, but it got the job done. :)

Thanks for all of your help. I really appreciate it!

Best Regards,
Ben Hocking
ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx




> On Nov 19, 2014, at 9:55 PM, Sam Owre <owre@xxxxxxxxxxx> wrote:
> 
> Hi Ben,
> The patch had one other problem with it, it was calling one of the new
> functions I made for you from the wrong place.  Could you replace it with
> the following?  I believe this fixes both the earlier problem you sent and
> the smooth_is_bounded proof (though grind doesn't finish the proof - let
> me know if you believe it should).
> 
> And please don't worry about sending too much - if you see something wrong
> in PVS (or even merely annoying), I want to know about it.
> 
> Thanks,
> Sam
> 
> <patch-20141114.lisp>
> 
> Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:
> 
>> Hi Sam,
>> 
>> I managed to uncover a different error, using a nice simple theory:
>> example: THEORY                                                            
>> BEGIN                                                                      
>> 
>>  smooth(divisor: real, new_val: real, old_val: real): real =              
>>    (new_val - old_val) / max(divisor, 1) + old_val                        
>> 
>>  smooth_is_bounded: THEOREM                                               
>>    FORALL(divisor: real, new_val: real, old_val: real):                   
>>      LET result = smooth(divisor, new_val, old_val) IN                    
>>        min(new_val, old_val) <= result AND result <= max(new_val, old_val)
>> 
>> END example                                                                
>> 
>> 
>> If I try to prove “smooth_is_bounded” using (grind), I get the error:
>> Error: the assertion (= (length types1) (length types2)) failed.
>>  [condition type: simple-error]
>> 
>> Please let me know if I’m spamming you, and thanks for all of your help.
>> 
>> Best Regards,
>> Ben Hocking
>> ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx