Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Reporting nitpick counterexample where Isabell...

Email Gateway (Aug 18 2021 at 12:31):

From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Hello,

I'd like to report the following behaviour of nitpick stating it finds a
"potentially spurious counterexample" to the lemma below. Isabelle,
nevertheless, confirms that the lemma is true.

definition pairwise_union :: "'a set set ⇒ 'a set set ⇒ 'a set set" (infixl
"⊎" 70)
where "A ⊎ B = (λ(X, Y). X ∪ Y) ` (A × B)"

lemma pairwise_union_eq:
"A ⊎ B = {a ∪ b|a b. a ∈ A ∧ b ∈ B}"
by (auto simp: pairwise_union_def)

lemma "(λ(A, B, C). (A ∪ B) ∪ C) ` (X × Y × Z) = (X ⊎ Y) ⊎ Z"
nitpick (* ??? *)
by (auto simp: pairwise_union_eq)

Best regards,

Email Gateway (Aug 18 2021 at 19:51):

From: Tobias Nipkow <nipkow@in.tum.de>
On 18/08/2021 14:29, Jonathan Julián Huerta y Munive wrote:

Hello,

I'd like to report the following behaviour of nitpick stating it finds a
"potentially spurious counterexample" to the lemma below. Isabelle,
nevertheless, confirms that the lemma is true.

That's why nitpick warns you that it is "potentially spurious".

Tobias

definition pairwise_union :: "'a set set ⇒ 'a set set ⇒ 'a set set" (infixl "⊎" 70)
  where "A ⊎ B = (λ(X, Y). X ∪ Y) ` (A × B)"

lemma pairwise_union_eq:
  "A ⊎ B = {a ∪ b|a b. a ∈ A ∧ b ∈ B}"
  by (auto simp: pairwise_union_def)

lemma "(λ(A, B, C). (A ∪ B) ∪ C) ` (X × Y × Z) = (X ⊎ Y) ⊎ Z"
  nitpick (* ??? *)
  by (auto simp: pairwise_union_eq)

Best regards,
--
Jonathan Julián Huerta y Munive
Postdoc at the University of Copenhagen
smime.p7s

Email Gateway (Aug 20 2021 at 08:35):

From: David Cock <david.cock@inf.ethz.ch>
Jonathan,

Just to expand a little: This isn't anything to worry about. Tools like
nitpick are, by design, generally neither sound nor complete.  Their job
is to be fast, with the proof kernel as a gatekeeper to prevent unsound
results propagating.

David

Email Gateway (Aug 20 2021 at 11:11):

From: Jonathan Julián Huerta y Munive <jonjulian23@gmail.com>
Hello,

Thanks for explaining this. I was not worrying. I only assumed that whoever
is working on Nitpick, would like to have as many of these examples as
"test-cases" if and when they decide to improve in this direction.

Best regards,

Last updated: Jan 04 2025 at 20:18 UTC