Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Bug/usability-report: find_theorem and sledgeh...


view this post on Zulip Email Gateway (Aug 22 2022 at 18:02):

From: Peter Zeller <p_zeller@cs.uni-kl.de>
Hello *,

I wanted to report a small usability problem I face from time to time.
Here is a short example:

lemma
shows "P ⟶ R"
proof
  have a: "P ⟶ R"
    sorry ― ‹Assume there is some complex proof here.›

assume a: P
  show R
    find_theorems R ― ‹Finds nothing.›
    sledgehammer ― ‹Does not find proof.›
    using a and P ⟶ R by simp
qed

The problem is that I accidentally gave the same name to 2 local facts
and find_theorems and sledgehammer can no longer find the first fact,
although it is still referable with quotes.

I think it would be good for usability if those facts still appeared in
search and were found by sledgehammer. Alternatively it would also be
helpful to get a warning when shadowing other local facts.

When shadowing local variables there can also be problems, so a warning
would also be nice in that case.

Regards,
Peter


Last updated: Nov 21 2024 at 12:39 UTC