[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
imports "Refine_Monadic.Refine_Monadic"
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.