# [isabelle] Nitpick counterexample for true statement

```Hi list,

nitpick is a great tool, as long as it does not refute provable lemmas,
as in the case below.

By the way, nunchaku chokes on this with an internal error.

Tested with Isabelle2018 and 9a7f94ab4df9, the result is the same.

--
Peter

--------------------------------

theory Scratch
begin

definition [to_relAPP]: "lsr R ≡ ⟨R⟩list_rel O {(a,set a) | a. True}"

lemma
assumes "(xs⇩1@xs⇩2,s)∈⟨R⟩lsr"
shows "(∃s⇩1 s⇩2. s=s⇩1∪s⇩2 ∧ (xs⇩1,s⇩1)∈⟨R⟩lsr ∧
(xs⇩2,s⇩2)∈⟨R⟩lsr)"
nunchaku (* Error: broken invariant: variable v_ig_1/448 not bound
in scope (code 1) *)
nitpick (*
Kodkod warning: Matrix too large: requested capacity of
506623120463
Nitpick found a counterexample for card 'a = 3 and card 'b = 2:
*)

(* Here is the proof of this lemma: *)
using assms[unfolded lsr_def]
proof (clarsimp simp: )
fix ys
assume "(xs⇩1 @ xs⇩2, ys) ∈ ⟨R⟩list_rel"
then obtain ys⇩1 ys⇩2 where [simp]: "ys=ys⇩1@ys⇩2" and "(xs⇩1,
ys⇩1) ∈ ⟨R⟩list_rel" "(xs⇩2, ys⇩2) ∈ ⟨R⟩list_rel"
using list_rel_append1 by blast

have "(xs⇩1, set ys⇩1) ∈ ⟨R⟩lsr"
unfolding lsr_def using ‹(xs⇩1, ys⇩1) ∈ ⟨R⟩list_rel›
by (auto simp: )
moreover have "(xs⇩2, set ys⇩2) ∈ ⟨R⟩lsr"
unfolding lsr_def using ‹(xs⇩2, ys⇩2) ∈ ⟨R⟩list_rel›
by (auto simp: )
ultimately show "∃s⇩1 s⇩2. set ys = s⇩1 ∪ s⇩2 ∧ (xs⇩1, s⇩1) ∈
⟨R⟩lsr ∧ (xs⇩2, s⇩2) ∈ ⟨R⟩lsr"
by auto
qed

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.