[Why3-club] Is this goal really (un)tractable ?

Frédéric Besson frederic.besson at inria.fr
Wed Feb 22 15:53:07 CET 2012


Hello,

I am trying to prove simple properties about an interpreter of a simple language.
My goals, which (to me) are straightforward, are not discharged by provers [alt-ergo, cvc3,eprover,vampire,yices].

This is the case for the following simplistic theory.

Theory T
 use import int.Int
 use import option.Option

type location 
type value = Int int | Loc location  
type pc = int

function evalcond (p:pc)  (x:value) (jmp:pc) : option pc = 
     match x with
      | Loc _ -> None
      | Int i -> if i >= 0 then Some p else Some jmp
    end

goal eval_case : forall p p':pc, x:value. 
   evalcond 1  x 4 = Some p' -> 
   p' = 1 \/ p' = 4

end

Could you tell me what I am doing wrong ?
This is so simple, I almost suspect a bug...

Actually, I also have a non-monotonicity problem.
* Provers do not discharge my initial problem
* Provers do discharge a cut-down version [alt-ergo.cvc3]
* Provers do not discharge the previous minimal goal

Are there known tricks to minimize the source of such erratic behaviors ?
Are there ways to provide hints to the provers.
For instance, is there a way to instruct the prover to
* recursively inline certain definitions (something like the simpl Coq tactic)
* when it is done, do a case analysis over the match statements

A that point, the previous goal is quantifier-free and falls in a decidable fragment...

I almost lost faith in those provers :(
Any insight would be much appreciated!

Best,

--
Frédéric Besson














More information about the Why3-club mailing list