Email Gateway (Aug 22 2022 at 17:16): Email Gateway (Aug 22 2022 at 17:16):From: Lars-Henrik Eriksson <lhe@it.uu.se>
Dear list,
Consider this lemma:
lemma assumes "rel_set R (insert C {}) (insert D {})" and "R A B"
shows "rel_set R (insert A (insert C {})) (insert B (insert D {}))"
"sledgehammer" produces this best proof: by (smt assms(1) assms(2) insert_iff rel_set_def)
while "using assms sledgehammer" produces this best proof: by (simp add: rel_set_def)
This difference surprises me. The Sledgehammer User's Guide doesn't mention that "using" has any effect other than directing the selection of relevant facts -- but Sledgehammer selected the facts needed by the second proof also without "using" -- as they were used in the first proof.
Are there any other effects of "using" in this context?
Lars-Henrik
Lars-Henrik Eriksson, Computing Science, Dept. of Information Technology, Uppsala University, Sweden
Email Gateway (Aug 22 2022 at 17:16):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars-Henrik,
I have to deeper knowledge of sledgehammer, but for the simplifier
»using P by simp« and »by (simp add: P)« makes a substantial difference.
From what you report I would guess that sledgehammer tries to find
rules to add to the simplifier »simp add: …« rather than facts to extend
to proof scope »using …«. Maybe an expert on sledgehammer can comment
on this.
Hope this helps,
Florian
signature.asc
Last updated: Apr 24 2024 at 20:16 UTC