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

Re: [PVS-Help] Proof by induction fails with geenric and library



Hi Jean-Claude,

It looks like you found a bug - anytime you see a "no methods applicable"
error it is most likely a bug.  Couls you send me your specs so that I can
recreate it?

Thanks,
Sam

Jean-Claude Royer <Jean-Claude.Royer@mines-nantes.fr> wrote:

> Hi all
> 
> I am trying to prove a theorem by induction but I got a problem.
> Not sure it is a bug, I did not succeed isolating the problem so I need some hints
> or better the solution.
> 
> I have some specifications, mainly a datatype World which is used in another
> library.
> In the second library I can type-check and even prove but induction is failing
> at the lisp level
> 
> The critical part is enclosed:
> 
> Test[S,W:TYPE] : THEORY
> BEGIN
> 	IMPORTING BASE@TheoryWorld[S, W]
> 
> 	 % does not work (but succeed in the BASE library)
> size_theorem2 : THEOREM FORALL (w:World[S,W]): size(w) > 0
> 
> 	     % BUGS ?
> END Test
> 
> Launching the prover I got the following message
> 
> pvs(1): 
> pvs(2): 
> Installing rewrite rule sets.singleton_rew (all instances)
> 
> size_theorem2 :  
> 
>   |-------
> {1}   FORALL (w: World[S, W]): b2n(size(w)) > 0
> 
> Rule? (induct "w")
> Error: No methods applicable for generic function
>        #<standard-generic-function add-usings-to-context*> with args
>        (nil ListMonitors[S, W]) of classes (null full-modname)
>   [condition type: program-error]
> 
> I suspect some problems with library, data type induction and parameter types.
> But may be it is a mistake in my specifications.
> regards
> 
> Jean-Claude.Royer@mines-nantes.fr
> ASCOLA, Mines de Nantes - INRIA
> + 33 2 51 85 82 05
> 
> 
> 
> 
> 
>