[Why3-club] Finite vs infinite sets

Andrei Paskevich andrei at lri.fr
Thu Nov 7 17:36:46 CET 2013


Hi Stefan,

"clone export SetGen" in the beginning of theory Fset means that the
generic theory SetGen (which is defined earlier in the file) is "cloned",
that is copied with a fresh set of symbols, in the beginning of Fset.
Notice that theory Set starts with the same instruction "clone export SetGen".
In other words, both Set and FSet start with the same declarations,
definitions, and axioms from SetGen, but for different (though homonymous)
type symbols, function symbols and predicate symbols. In yet other words,
the type (set 'a) provided by Set is not the same as the type (set 'a)
provided by FSet, and the cardinality-related functions and axioms only
exist for the latter.

It would be different, if Set and Fset started with "use export SetGen"
instead of "clone export SetGen". The "use" instruction does not produce a
local copy of a theory but refers directly to its symbols and properties.
Then Set and Fset would talk about the same type (set 'a) which would
therefore not be suitable for infinite sets.

Best,
Andrei


On 7 November 2013 17:23, Stefan Berghofer <berghofe at in.tum.de> wrote:

> Dear Why3-Club,
>
> I just stumbled upon the theory set.why declaring a type "set 'a" that,
> according to the
> comment following the declaration, may be either finite or infinite. Later
> on, there is a
> section introduced with the comment (** {2 Finite sets} *) containing
> axioms that are obviously
> not true for infinite sets, such as
>
>   axiom cardinal_remove:
>     forall x : 'a. forall s : set 'a.
>     mem x s -> cardinal s = 1 + cardinal (remove x s)
>
> I would have expected this axiom to either have an additional assumption
> such as "finite s",
> or to use a different type such as "fset 'a" denoting finite sets. Maybe I
> am just missing something?
>
> Greetings,
> Stefan
>
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131107/83e37d48/attachment.html>


More information about the Why3-club mailing list