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,

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

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

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: Dec 05 2021 at 23:19 UTC