# PVS Bug 625

Synopsis: Bug resolving use of overloaded function
Severity: serious
Priority: medium
Responsible: owre
State: analyzed
Class: sw-bug
Arrival-Date: Sat Dec 1 22:59:52 2001
Originator: Marcelo Glusman
Organization: csd.cs.technion.ac.il
Release: PVS 2.4
Environment:
System:
Architecture:
Description:
Hi,
I think I know how you can recreate the bug.
Here's a stupid example:
test: THEORY
BEGIN
IMPORTING finite_sets@finite_sets_minmax[nat,<=]
under10: set[nat] = {i:nat|i<10}
exists_max: THEOREM
EXISTS(n: nat): FORALL(m: (under10)): m<=n
END test
Of course one can prove the theorem by instatiating n with 9.
But if you start the proof with:
(inst + "max[nat,<=]({i:nat|i<10})")
You get a message that says that [nat->bool] should be a subtype
of [nat,nat].
I don't remember why in my original proof I used "max[nat,<=](...)"
I now removed this (calling max directly) and the bug doesn't happen.
You can decide if this is still a bug or not - it's certainly unexpected,
since PVS should realize that there are two max functions in that
theory.
Good luck,
Marcelo.
How-To-Repeat:
Fix:
Modified matching-actual-expr* to check for compatible types correctly.
Was using (some (lambda (x y) ...)) when it should have used
(some (lambda (x) (some (lambda (y) ...))))
The problem with the first form is that it compares the possible types as
ordered lists, rather than as sets.