Email Gateway (Aug 18 2022 at 18:08): Email Gateway (Aug 18 2022 at 18:08):From: Christoph Feller <c_feller@informatik.uni-kl.de>
Hallo,
a colleague and I came to the conclusion that it would be nice to have
injectivity theorems for datatype constructors (example below). These
are really easily proven - but I think they could help sledgehammer or
tactics like auto/blast.
Our example:
datatype ident = Ident string
theorem infinite_idents:
"\<not> finite (UNIV :: ident set)"
apply clarify
apply (drule_tac h="inv Ident" in finite_imageI)
sledgehammer
This gives me a "metis line" that doesn't work (I only use E and
SPASS). But if I insert
lemma Ident_inj:
"inj Ident"
by (simp add:inj_on_def)
before our theorem both E and SPASS can find a working solution really
quickly. So I think it would help to add theorems like "inj
<Constructor>" to the theorems generated for datatypes. I know about
<type>.inject which basically contains "inj <Constructor>" but
automatic methods apparently don't find that connection.
Additionally I think that a lemma "inj f ==> inj_on f A" would be nice to have.
Regards,
Christoph Feller
Email Gateway (Aug 18 2022 at 18:08):From: Alexander Krauss <krauss@in.tum.de>
Hi Christoph,
a colleague and I came to the conclusion that it would be nice to have
injectivity theorems for datatype constructors (example below). These
are really easily proven - but I think they could help sledgehammer or
tactics like auto/blast.
Adding more automatically generated stuff is not for free in terms of
performance and scalability. So one would want some good empirical
evidence before doing something like that by default.
Our example:
datatype ident = Ident string
theorem infinite_idents:
"\<not> finite (UNIV :: ident set)"
apply clarify
apply (drule_tac h="inv Ident" in finite_imageI)
sledgehammerThis gives me a "metis line" that doesn't work (I only use E and
SPASS).
Sledgehammer has seen quite a bit of improvement recently. The current
development version gives me a metis call that completes in 94ms.
But if I insert
lemma Ident_inj:
"inj Ident"
by (simp add:inj_on_def)before our theorem both E and SPASS can find a working solution really
quickly.
In the development version I get the same metis call as above, so
nothing gained.
So I think it would help to add theorems like "inj
<Constructor>" to the theorems generated for datatypes. I know about
<type>.inject which basically contains "inj<Constructor>" but
automatic methods apparently don't find that connection.
It is very hard to make such statements in general. Also, (in)finiteness
proofs are a bit special. They are often trivial for humans but
automation is particularly weak there. Probably
Additionally I think that a lemma "inj f ==> inj_on f A" would be nice to have.
Well, this is just subset_inj_on[OF _ subset_UNIV]. A reason for having
it explicitly could be that people might search for it. Unfortunately,
even when it is present, a search for "inv inv_on" doesn't show it,
since inv is just an abbreviation... Too bad.
Alex
Last updated: Apr 26 2024 at 16:20 UTC