Email Gateway (Aug 22 2022 at 10:40): Email Gateway (Aug 22 2022 at 10:40):From: Matthew Fernandez <matthew.fernandez@nicta.com.au>
While we're on the topic of quickcheck, why does it fail to show a counterexample for this?
lemma "set [(1::nat)] ⊆ set [2]"
quickcheck
(* Outputs the following, but no actual example:
* Quickchecking...
* Testing conjecture with Quickcheck-exhaustive...
* Quickcheck found a counterexample:
*)
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 22 2022 at 10:41):From: Lars Noschinski <noschinl@in.tum.de>
-- Lars
Email Gateway (Aug 22 2022 at 10:45):From: Andrew Gacek <andrew.gacek@gmail.com>
You could do this to get a 'counterexample' in this case:
lemma "set [(1::nat)] ⊆ set [2]"
apply rule
quickcheck
Then it works on "!!x. x \in set [1] ==> x \in set [2]" and finds the
counterexample "x = 1".
-Andrew
Email Gateway (Aug 22 2022 at 10:46):From: Jason Dagit <dagitj@gmail.com>
On Wed, Jul 1, 2015 at 11:14 PM, Tobias Nipkow <nipkow@in.tum.de> wrote:
On 02/07/2015 07:48, Jason Dagit wrote:
I forgot to add a type annotation and ended up with the following
(Isabelle
2015 on Windows 7):lemma "3 < 4" quickcheck
No type constraints. Because 3, 4 and < are polymorphic, quickcheck is
free to build a type/model with an interpretation for < where 3 < 4 does
not hold.
I see. Thanks!
There used to be a time when the interface alerted you to polymorphic
numerals, which are almost always not what one wants. But we have moved on
from that.
I think I've been bitten by this several times. Most recently (and where I
discovered the above example), I was proving the follow lemma, using the
induction lemma described in [1]:
lemma "(n::nat) > 1 ⟹ n⇧2 > n + 1"
In the case of n = 2, I had this:
case 2
show "2 + 1 < 2⇧2" by auto
This was giving me a message saying:
show 2 + 1 < 2⇧2
Successful attempt to solve goal by exported rule:
(1 < 2) ⟹ 2 + 1 < 2⇧2
But also saying:
Failed to finish proof⌂:
goal (1 subgoal):
Of course, if I manually simplified the expression in my show to match
the goal, then I get an error about refining the goal.
As you might have already guessed, the solution is rather simple, I have to
add a type annotation somewhere in the show. So having an alert about
polymorphic numerals would have been helpful here for this beginner. Lesson
learned.
[1]
http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/10660
Email Gateway (Aug 22 2022 at 10:46):From: Makarius <makarius@sketis.net>
There are many more possibilities to get into trouble with types that are
more general than expected. It used to be a really hard problem to figure
that out in the past. Today you just need to C-hover over subspicious
variables in the Prover IDE, to get the type information. You have to
become active yourself, though.
One day in the future, the Prover IDE might hilight such suspicious
positions spontaneously. (And users will probably run into other problems
instead.)
Makarius
Email Gateway (Aug 22 2022 at 10:50):From: Jason Dagit <dagitj@gmail.com>
I forgot to add a type annotation and ended up with the following (Isabelle
2015 on Windows 7):
lemma "3 < 4" quickcheck
Quickchecking...
For instantiation with default_type Enum.finite_1:
Enum.finite_1 to be substituted for variable 'a does not have sort
{numeral,ord}
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:
Compared with the type annotation:
lemma "(3::nat) < 4" quickcheck
Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found no counterexample.
Note: in the first case it says there is a counter example but that is the
end of the output in the "Output" tab of jEdit.
Is this to be expected when no types are given? As a new Isabelle user it
quite surprised me.
Thanks,
Jason
Email Gateway (Aug 22 2022 at 10:51):From: Tobias Nipkow <nipkow@in.tum.de>
On 02/07/2015 07:48, Jason Dagit wrote:
I forgot to add a type annotation and ended up with the following (Isabelle
2015 on Windows 7):lemma "3 < 4" quickcheck
No type constraints. Because 3, 4 and < are polymorphic, quickcheck is free to
build a type/model with an interpretation for < where 3 < 4 does not hold.
There used to be a time when the interface alerted you to polymorphic numerals,
which are almost always not what one wants. But we have moved on from that.
The fact that you are not shown the model is because only the interpretation of
the free variables is shown, but there are none.
Tobias
Quickchecking...
For instantiation with default_type Enum.finite_1:
Enum.finite_1 to be substituted for variable 'a does not have sort
{numeral,ord}
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found a counterexample:Compared with the type annotation:
lemma "(3::nat) < 4" quickcheck
Quickchecking...
Testing conjecture with Quickcheck-exhaustive...
Quickcheck found no counterexample.Note: in the first case it says there is a counter example but that is the
end of the output in the "Output" tab of jEdit.Is this to be expected when no types are given? As a new Isabelle user it
quite surprised me.Thanks,
Jason
Email Gateway (Aug 22 2022 at 10:52):From: Manuel Eberl <eberlm@in.tum.de>
Should it not at least show the interpretation of the free type variable?
Manuel
Email Gateway (Aug 22 2022 at 10:53):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Showing the instantiations for the type variables would be sensible. However, if one knows
how quickcheck works, the search scope is pretty small. With the default setup in
Isabelle2015, quickcheck with exhaustive search tries only the types Enum.finite_1,
Enum.finite_2, and Enum.finite_3.
In this case, its the type finite_2 which produces a counterexample. Interestingly,
quickcheck does not find a counterexample for "4 < 5" (because only Enum.finite_2
instantiates the numeral type class and there it holds).
Andreas
Last updated: Apr 23 2024 at 16:19 UTC