Email Gateway (Aug 19 2022 at 08:26): Email Gateway (Aug 19 2022 at 08:26):From: Yuhui Lin <Y.H.Lin-2@sms.ed.ac.uk>
Hi all,
With the change of representation for set, quickcheck can find counter examples for the type like "nat set" now. When I use quickcheck for the following example,
definition
forwardcomp :: "('a * 'b) set ⇒ ('b * 'c) set ⇒ ('a * 'c) set" (infixl ";" 40)
where "p ; q ≡ {(x,y). ∃ z. (x,z) ∈ p ∧ (z,y) ∈ q}"
locale myspec =
fixes
v1 v2 v3 :: "(nat * nat) set"
lemma (in myspec)
"((v1 Un v2) ; v3) = ((v1 ; v3) Un (v2 ; v3))"
quickcheck
oops
it promote the error message
Wellsortedness error:
Type nat not of sort {enum,equal}
No type arity nat :: enum
What do I miss here ? Many thanks.
Best,
Yuhui Lin
Email Gateway (Aug 19 2022 at 08:26):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Yuhui,
the problem is the existential quantifier in the definition of forwardcomp.
Isabelle provides an executable implementation for types of whose elements it is
has a complete list (which is formalised in type class enum). Since lists are
finite, nat is not and cannot be an instance. As quickcheck relies on executable
implementations for all constants, this explains the error message.
If you want to quickcheck lemmas that depend on forwardcomp, you need to provide
an executable implementation yourself. By default, Isabelle2012 implements sets
as the list of its elements (or by the list of the set's complement). Hence, you
could prove the following code equation by "pattern-matching" on the
"implementation constructor" set.
lemma forwardcomp_code [code]:
"(set ps; set qs) =
set (concat (map (l(x, y). map (l(y', z'). (x, z')) (filter (l(y', z'). y =
y') qs)) ps))"
by(fastforce simp add: forwardcomp_def)
Then, you can quickcheck your lemma. Side remark: For a complete implementation,
you would probably want to cover all "implementation constructors" for 'a set,
which are "set" and "List.coset". But it will be more difficult to find
appropriate equations for List.coset.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 08:26):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hi Yuhui,
I had the same answer as Andreas in my pipeline.
Alternatively, it should also be possible to give a lemma that describes
forwardcomp in terms of relcomp, and annotate it with the code attribute.
Lukas
Email Gateway (Aug 19 2022 at 08:39):From: Yuhui Lin <Y.H.Lin-2@sms.ed.ac.uk>
Hi,
Now I've got a new problem to give a code attribute for the following function.
"funimage r x = (THE y. (x, y) ∈ r)"
I give a weaker version of code definition, i.e
(funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))
but I don't know how to represent it equivalently in list, because it addresses that y is unique and x : r, which returns boolean type.
I wonder if there is undefined value for list to represent the invalid case, e.g. return the invalid value when y is not unique. Also I'm trying to giving assumptions for the the code attribute, which is
"x : Domain (set ss) ==> functional (set ss) ==> (funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))"
Then I receive a warning "Not a equation".
How can I deal with it ? Thanks for helps.
best,
Yuhui
Email Gateway (Aug 19 2022 at 08:39):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Yuhui,
Now I've got a new problem to give a code attribute for the following function.
"funimage r x = (THE y. (x, y) ∈ r)"I give a weaker version of code definition, i.e
(funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))
This is neither weaker nor stronger. Moreover, your code definition is not a
proper specification at all - in fact it is unprovable. Otherwise, you would get
the following inconsistency
"0 = funimage (set [(0, 0), (0, 1)]) 0 = funimage (set [(0, 1), (0, 0)]) 0 = 1"
because "set [(0, 0), (0, 1)] = set [(0, 1), (0, 0)]". In effect, you try to
exploit additional structure of the list when there is no such in the type of sets.
I wonder if there is undefined value for list to represent the invalid case, e.g. return the invalid value when y is not unique. Also I'm trying to giving assumptions for the the code attribute, which is
"x : Domain (set ss) ==> functional (set ss) ==> (funimage (set ss) x) = snd (hd (filter (λ (x0, y0). x = x0) ss))"
Then I receive a warning "Not a equation".
Code equations must not make assumptions about the parameters. However, you can
move the assumptions into a test:
lemma [code]:
"funimage (set ss) x =
(if x : Domain (set ss) & functional (set ss)
then snd (hd (filter (λ (x0, y0). x = x0) ss))
else funimage (set ss) x)"
This should be provable and the code generator accepts it. If all your use
contexts ensure the preconditions themselves, then this equation is perfectly
fine. However, if you plan to use quickcheck, you will probably get into
non-termination very quickly.
Therefore, it is better to have the else branch raise an exception than to risk
non-termination. You can do so as follows:
definition funimage_not_unique :: "(unit => 'a) => 'a"
where [simp]: "funimage_not_unique f = f ()"
code_abort funimage_not_unique
lemma [code]:
"funimage (set ss) x =
(if x : Domain (set ss) & functional (set ss)
then snd (hd (filter (λ (x0, y0). x = x0) ss))
else funimage_not_unique (%_. funimage (set ss) x))"
code_abort funimage_not_unique
tells the code generator to raise an exeption with message "funimage_not_unique"
whenever the generated code executes funimage_not_unique.
The constant funimage_not_unique itself is almost the identity, i.e., it does
not change the else branch fundamentally. The unit closure ensures termination
in strict languages like ML, because it prohibits to evaluate the argument of
funimage_not_unique, which would recurse endlessly.
Some examples of this technique can be found in the HOL sources, e.g., in
Predicate.thy. In fact, Predicate already provides an executable definite
description operator (which has been described in [1]). Hence, the following
should also work (not tested!):
lemma
"funimage (set ss) x =
Predicate.the (pred_of_set (set (filter (λ (x0, y0). x = x0) ss)))"
Hope this helps,
Andreas
[1] Andreas Lochbihler, Lukas Bulwahn, Animating the Formalised Semantics of a
Java-like Language, Marko van Eekelen and Herman Geuvers and Julien Schmalz and
Freek Wiedijk (Ed.), Interactive Theorem Proving, pp. 216--232, Springer, 2011.
Email Gateway (Aug 19 2022 at 08:47):From: Yuhui Lin <Y.H.Lin-2@sms.ed.ac.uk>
Many thanks for the solution. I can run quick check on these user-defined operations code attributes. And I wonder for the following defitnion,
"Pow1 R = {S. S ≠ {} ∧ S ⊆ R}"
"domres R r = {(x, y) | x y. x ∈ R ∧ (x, y) ∈ r}"
there are no quantifiers, and the definitions look simple. I wonder why quick check can't execute them directly. More interestingly, if I unfolder the definition of Pow1, then quick check can work..
lemma "(S :: nat set) ~: Pow1 S"
lemma "(domres (s0::nat set) (v1:: (nat*nat set))) Un v2 = domres s0 (v1 Un v2)"
Best,
Yuhui
Email Gateway (Aug 19 2022 at 08:48):From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Dear Yuhui,
Since sets are represented as the list of their elements, the "Pow1 S" in your
first lemma needs to be computed explicitly. Now, Pow1 is defined as a set
comprehension, which is in general not executable. The default code setup
computes set comprehensions by taking the list of all elements of the type and
filtering each by checking the predicate of the set comprehension. If you unfold
the definition, your goal has the form ".. : {S. ...}" and there is a
preprocessing step in the code generator that simplifies this to "... ..", i.e.,
removes the set comprehension and membership.
For domres, there are quantifiers. "{(x, y) | x y. ...}" is a short-hand for
"{u. \exists x y. u = (x, y) & ...}". For tuples, you don't need to quantify
over x and y, so you could simplify the definition to
"domres R r = {(x, y). x ∈ R ∧ (x, y) ∈ r}"
Nevertheless, the trouble with set comprehensions remains, but you could prove
again a custom code equation:
lemma domres_code [code]:
"domres R (set rs) = set (filter (%(x, y). x : R) rs)"
by(auto simp add: domres_def)
Best,
Andreas
Email Gateway (Aug 19 2022 at 08:49):From: Lukas Bulwahn <bulwahn@in.tum.de>
Dear Yuhui,
On 09/03/2012 10:54 AM, Andreas Lochbihler wrote:
Dear Yuhui,
And I wonder for the following defitnion,
"Pow1 R = {S. S ≠ {} ∧ S ⊆ R}"
"domres R r = {(x, y) | x y. x ∈ R ∧ (x, y) ∈ r}"there are no quantifiers, and the definitions look simple. I wonder
why quick check can't execute them directly. More interestingly, if I
unfolder the definition of Pow1, then quick check can work..lemma "(S :: nat set) ~: Pow1 S"
lemma "(domres (s0::nat set) (v1:: (nat*nat set))) Un v2 = domres s0
(v1 Un v2)"Since sets are represented as the list of their elements, the "Pow1 S"
in your first lemma needs to be computed explicitly. Now, Pow1 is
defined as a set comprehension, which is in general not executable.
The default code setup computes set comprehensions by taking the list
of all elements of the type and filtering each by checking the
predicate of the set comprehension. If you unfold the definition, your
goal has the form ".. : {S. ...}" and there is a preprocessing step in
the code generator that simplifies this to "... ..", i.e., removes the
set comprehension and membership.For domres, there are quantifiers. "{(x, y) | x y. ...}" is a
short-hand for "{u. \exists x y. u = (x, y) & ...}". For tuples, you
don't need to quantify over x and y, so you could simplify the
definition to"domres R r = {(x, y). x ∈ R ∧ (x, y) ∈ r}"
Nevertheless, the trouble with set comprehensions remains, but you
could prove again a custom code equation:lemma domres_code [code]:
"domres R (set rs) = set (filter (%(x, y). x : R) rs)"
by(auto simp add: domres_def)Andreas is perfectly right with his explanations. It took me also a few
minutes to understand what Quickcheck is doing there and what not.
You can inspect the code setup with this type of template:
definition conjecture
where
"conjecture S = ((S :: nat set) ~: Pow1 S)"
code_thms conjecture
In this case, you see that it requires the constant Collect which uses
enum_class.enum.
In general, it somehow black magic (known to some wizards here and
there) to understand why something is not executable.
For the future, we are developing a rewriting procedure in the code
generator that should turn
"domres R r = {(x, y) | x y. x ∈ R ∧ (x, y) ∈ r}" into "(R \times UNIV)
\inter r" behind the scenes which can be executed with the code
generator (and therefore Quickcheck works).
If you write "Pow1 R = {S. S ≠ {} ∧ S ⊆ R}" as "Pow1 R = Pow R - {{}}"
it should also be executable (and Quickcheck works).
Lukas
Best,
Andreas
Last updated: Apr 25 2024 at 20:15 UTC