Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Nitpick generates a wrong counterexample for a...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:41):

From: Denis Nikiforov <denis.nikif@gmail.com>
Hi

Here is the lemma:

lemma list_all2_rtrancl2_example:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧ xs ys ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧ xs ys"
nitpick

Nitpick outputs the following:

Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample:

Free variables:
xs = [0]
ys = [2]

It's easy to show that the counterexample is wrong:

lemma list_all2_rtrancl2_example_0_2:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧ [0] [2] ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧ [0] [2]"
apply (rule_tac ?b="[1]" in converse_rtranclp_into_rtranclp; simp)
apply (rule_tac ?b="[2]" in converse_rtranclp_into_rtranclp; simp)
done

view this post on Zulip Email Gateway (Aug 22 2022 at 18:41):

From: Denis Nikiforov <denis.nikif@gmail.com>
Hi

Here is the lemma:

lemma list_all2_rtrancl2_example:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧ xs ys ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧ xs ys"
nitpick

Nitpick outputs the following:

Nitpicking formula...
Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
Nitpick found a counterexample:

Free variables:
xs = [0]
ys = [2]

It's easy to show that the counterexample is wrong:

lemma list_all2_rtrancl2_example_0_2:
"list_all2 (λx y. x = y ∨ Suc x = y)⇧ [0] [2] ⟹
(list_all2 (λx y. x = y ∨ Suc x = y))⇧ [0] [2]"
apply (rule_tac ?b="[1]" in converse_rtranclp_into_rtranclp; simp)
apply (rule_tac ?b="[2]" in converse_rtranclp_into_rtranclp; simp)
done


Last updated: Mar 29 2024 at 12:28 UTC