Email Gateway (Aug 22 2022 at 18:31): Email Gateway (Aug 22 2022 at 18:31):From: xanonec xyz <xanonec@gmail.com>
Dear All,
There may be a bug in nitpick. The example below exposes the problem. In
particular, lemma "bug_example_proof" can be proved. However, nitpick finds
a counterexample for the identical lemma "bug_counterexample": "n::nat =
1::nat". Many other theorems about intmod2 seem to have the same issue. The
problem occurs in Isabelle2017 and Isabelle2018 (macOS).
theory bug_1
imports Complex_Main
"HOL-Algebra.Group"
begin
declare [[show_types]]
declare [[show_sorts]]
declare [[show_consts]]
definition qintrel2 :: "int ⇒ int ⇒ bool"
where "qintrel2 = (λx y. 2 dvd (x - y))"
quotient_type intmod2 = "int" / "qintrel2"
morphisms Rep_IntegMod2 Abs_IntegMod2
proof (rule equivpI)
show "reflp qintrel2" by (auto simp: qintrel2_def reflp_def)
show "symp qintrel2" by (auto simp: qintrel2_def symp_def)
show "transp qintrel2" by (auto simp: qintrel2_def transp_def)
qed
instantiation intmod2 :: comm_ring_1
begin
lift_definition zero_intmod2 :: "intmod2" is "0" .
lift_definition one_intmod2 :: "intmod2" is "1" .
lift_definition plus_intmod2 :: "intmod2 ⇒ intmod2 ⇒ intmod2"
is "λx y. x + y"
by (simp add: qintrel2_def)
lift_definition uminus_intmod2 :: "intmod2 ⇒ intmod2"
is "λx. -x"
by (simp add: qintrel2_def)
lift_definition minus_intmod2 :: "intmod2 ⇒ intmod2 ⇒ intmod2"
is "λx y. x + (-y)"
by (simp add: qintrel2_def)
lift_definition times_intmod2 :: "intmod2 ⇒ intmod2 ⇒ intmod2"
is "λx y. x*y"
by (simp add: qintrel2_def)
instance
by standard (transfer; simp add: qintrel2_def; presburger)+
end
lemma bug_example_proof: "of_int (int n) = (0::intmod2) ⟹ of_int (int (Suc
n)) = (1::intmod2)"
by simp
lemma bug_counterexample: "of_int (int n) = (0::intmod2) ⟹ of_int (int (Suc
n)) = (1::intmod2)"
by nitpick
end
xanonec
Last updated: Nov 21 2024 at 12:39 UTC