Email Gateway (Mar 01 2024 at 12:27): Email Gateway (Mar 01 2024 at 12:27):From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Dear list,
Can I influence what name sledgehammer generated proofs use for a
theorem that goes by different names.
E.g., I have
lemma my_op_assoc: "..."
and further down the line, I have:
lemmas prep_fri_simps = my_op_assoc
The latter one is meant to be used for a specific task (and I expect
that it might get expanded in the future).
Now, sledgehammer's proof reconstruction seems to prefer the name
prep_fri_simps over my_op_assoc. Is there any way to tell sh to prefer
the other name?
Email Gateway (Mar 01 2024 at 13:52):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Peter,
There's no way unfortunately. I have some code that should make Sledgehammer prefer "foo" over "bar(7)", but somehow that code doesn't seem to work, as others have pointed out in the past. I need to look into this.
Best,
Jasmin
Email Gateway (Mar 06 2024 at 21:28):From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Peter,
you may want to try the (undocumented?) no_atp attribute to blacklist
the lemmas you do not want Sledgehammer to use.
From the src/HOL/HOL.thy file, where no_atp is defined.
Theorems blacklisted to Sledgehammer. These theorems typically
produce clauses
that are prolific (match too many equality or membership literals)
and relate to
seldom-used facts. Some duplicate other rules.
Cheers,
Martin
Email Gateway (Mar 06 2024 at 21:35):From: Peter Lammich <lammich@in.tum.de>
If I understand correctly the noatp will blacklist the fact, under any name it
comes with. I still want to use the fact, just with it's nice name.
Peter
Email Gateway (Mar 08 2024 at 09:45):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Peter is right: no_atp kills the theorem, not just the name, unfortunately.
Jasmin
Email Gateway (Mar 08 2024 at 09:57):From: Martin Desharnais <martin.desharnais@posteo.de>
Ah, I did not realized that. That is unfortunate.
An attribute to disable just the name should probably go on our
nice-to-have list. I also sometimes encounter situations similar to
Peter's one.
One such example is when a named collection of lemmas is introduced. e.g.
lemmas my_stuff_simps = foo_simp bar_simp baz_simp
I think it would be good to have a way to ensure that Sledgehammer uses,
e.g., bar_simp instead of my_stuff_simps(2).
Cheers,
Martin
Email Gateway (Mar 13 2024 at 18:25):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Jasmin &al.,
Peter is right: no_atp kills the theorem, not just the name, unfortunately.
good to learn about that, the official documentation in the source
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/HOL.thy$775
confirms that.
In recent times, when sorting out lemma duplicates etc. I tended to use
[no_atp] with the misleading assumption that it would rule out a
discouraged name rather than a whole proposition.
Is there any way to indicate to SH that some names are preferrable to
others?
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Mar 13 2024 at 18:30):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
A not directly related remark – there are two quite creative proof
incantations relying on no_atp:
reading
proof (intro no_atp(10)[OF subsetI subsetI])
…
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Mar 13 2024 at 18:42):From: Peter Lammich <lammich@in.tum.de>
Oh, nice... Find_theorem at it's best, from the old days when it didn't prefer
nice names?? Must be fixed, very fragile proof...
Email Gateway (Mar 14 2024 at 14:47):From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Is there any way to indicate to SH that some names are preferrable to others?
Unfortunately, there is not. If somebody wants to design and implement such a scheme, I'd be happy to help them.
Jasmin
Last updated: Jan 04 2025 at 20:18 UTC