Email Gateway (Aug 18 2022 at 14:09): Email Gateway (Aug 18 2022 at 14:09):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I wanted to prove the following lemma:
lemma
fixes A :: "'a set"
assumes "finite A"
obtains f::"'a => nat" and n::"nat" where
"f`A = {i. i<n}"
"inj_on f A"
(* Sledgehammer found a proof: *)
apply (metis finite finite_imageD id_apply inj_on_inverseI
infinite_UNIV_char_0)
(* Here, Isabelle sais: No subgoals
However, when finnishing the proof: *)
done
(* I get the error:
*** Pending sort hypotheses: {finite,semiring_char_0}
*** At command "done".
*)
Ok, I wondered how to prove the theorem from the lemmas given to metis.
But what is happening here behind the scenes, how do these
typeclasses(?) enter the game?
Regards,
Peter
Email Gateway (Aug 18 2022 at 14:10):From: Tobias Nipkow <nipkow@in.tum.de>
I am surprised you got any answer from sledgehammer, I failed.
Unfortunately the proof you got is not a real proof: the ATPs are give a
problem with some type information omitted for efficiency reasons. This
allows them sometimes to find proofs that do not replay in Isabelle
because of typing problems. Yours is most likely of that kind.
The development version has a Settings item ATP: Full Types that gives
the ATPs the full type information which you can try in such situations.
It will avoid these unsound proofs but also reduces the success rate of
the ATPs. In you example I am sceptical that the ATPs will find a real
proof because of the non-trivial witnesses required.
Tobias
Peter Lammich schrieb:
Email Gateway (Aug 18 2022 at 14:10):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
Peter Lammich schrieb:
Pending sort hypothesis are sort constraints which a theorem's proof
relies one, but whose type variables do not occur in the theorem
proposition; the have to be given explicitly in the assumptions, e.g.
assumes "SORT_CONSTRAINT('a::{finite,semiring_char_0})"
or whatever type variable 'x they refer too.
Hope this helps
Florian
signature.asc
Email Gateway (Aug 18 2022 at 14:10):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
Hi Peter.
I agree with Tobias, it's highly unlikely that the automated theorem
provers will find an instantiation that solves your problem. I was
fiddling with your problem out of interest, and did find a proof, but
it's not especially elegant. The rule finite_distinct_list tells you
that a list exists which puts A in order, giving you (roughly) the
inverse of the function f you want. The problem is inverting back to f
since we don't have an injective function. To do this I had to extend
into the sum type to force injectivity - maybe someone can see an easier
way?
Yours,
Thomas.
lemma
fixes A :: "'a set"
assumes finA: "finite A"
obtains f::"'a => nat" and n::"nat" where
"f`A = {i. i<n}"
"inj_on f A"
proof -
obtain xs where dist: "distinct xs" and A: "A = set xs"
using finite_distinct_list[OF finA] by auto
obtain g where g_def: "g == (%n. if n < length xs then Inl (xs ! n)
else Inr n)" ..
obtain f where f_def: "f == inv g o Inl" ..
have inj_g: "inj g"
unfolding g_def
apply (rule inj_onI)
apply (auto simp: nth_eq_iff_index_eq[OF dist] split: split_if_asm)
done
have f_i: "!!i. i < length xs ==> f (xs ! i) = i"
unfolding f_def
apply (cut_tac x=i in inv_f_f[OF inj_g])
apply (clarsimp simp: g_def)
done
have f_im: "f ` A = {i. i < length xs}"
apply safe
apply (clarsimp simp: A in_set_conv_nth f_i)
apply (simp add: A)
apply (rule image_eqI[OF sym], erule f_i)
apply simp
done
have f_inj: "inj_on f A"
apply (rule inj_onI)
apply (auto simp: A in_set_conv_nth f_i)
done
show ?thesis
using prems f_im f_inj by auto
qed
Tobias Nipkow wrote:
Email Gateway (Aug 18 2022 at 14:11):From: Tobias Nipkow <nipkow@in.tum.de>
It would be nice to get a compact proof. Here is a condensed version of
Thomas's proof, getting rid of Inl/Inr:
lemma
fixes A :: "'a set"
assumes finA: "finite A"
obtains f::"'a => nat" and n::"nat" where
"fA = {i. i<n}"
"inj_on f A"
proof -
obtain xs where dist: "distinct xs" and A: "A = set xs"
using finite_distinct_list[OF finA] by auto
let ?I = "{i. i<size xs}"
def g == "%n. xs ! n"
def f == "Inv ?I g"
have inj_g: "inj_on g ?I"
unfolding g_def
apply (rule inj_onI)
apply (auto simp: nth_eq_iff_index_eq[OF dist] split: split_if_asm)
done
have f_i: "!!i. i : ?I ==> f (xs ! i) = i"
unfolding f_def by (metis Inv_f_f g_def inj_g)
have f_im: "f A = ?I"
apply(auto simp add:A in_set_conv_nth f_i)
apply (metis Collect_def f_i in_set_conv_nth rev_image_eqI mem_def)
done
have f_inj: "inj_on f A"
apply (rule inj_onI)
apply (auto simp: A in_set_conv_nth f_i)
done
show ?thesis using prems f_im f_inj by auto
qed
I am sure this can be improved further.
Tobias
Thomas Sewell wrote:
Email Gateway (Aug 18 2022 at 14:11):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi Thomas,
My hope was that ATP would find a proof based on the lemma
"finite_imp_nat_seg_image_inj_on" that is, in some sense, the inverse of
my lemma.
In the meantime, I proved the lemma directly with induction over the
finite set (no idea whether this is more elegant ;) ):
-- "Finite sets have an injective mapping to an initial segments of the
natural numbers"
lemma finite_imp_inj_to_nat_seg:
fixes A :: "'a set"
assumes A: "finite A"
obtains f::"'a \<Rightarrow> nat" and n::"nat" where
"f`A = {i. i<n}"
"inj_on f A"
proof -
from A have "\<exists>f (n::nat). fA = {i. i<n} \<and> inj_on f A"
proof (induct)
case empty thus ?case by auto
next
case (insert x A)
then obtain f and n::nat where
IH: "fA = {i. i<n}" "inj_on f A" by auto
let ?fs = "f(x:=n)"
from IH insert(2) have
"?fs`(insert x A) = {i. i<Suc n}"
"inj_on ?fs (insert x A)"
apply -
apply force
apply simp
apply (rule inj_onI)
apply (auto dest: inj_onD split: split_if_asm)
done
thus ?case by blast
qed
with that show ?thesis by blast
qed
regards,
Peter
Thomas Sewell wrote:
Email Gateway (Aug 18 2022 at 14:11):From: Tobias Nipkow <nipkow@in.tum.de>
It turns out that your intuition was right: sledgehammer can prove the
theorem, with a little help. This is the resulting proof (to go into the
library):
lemma finite_imp_inj_to_nat_seg:
"finite A ==> EX f n::nat. f`A = {i. i<n} & inj_on f A"
by (metis bij_betw_Inv bij_betw_def finite_imp_nat_seg_image_inj_on)
For a start, notice the formulation in terms of EX rather than
"obtains", which s/h seems to prefer. But still, s/h does not find a
proof. You need to tell it to use finite_imp_nat_seg_image_inj_on:
using finite_imp_nat_seg_image_inj_on
Now s/h finds the above proof.
Tobias
Lammich schrieb:
Email Gateway (Aug 18 2022 at 14:11):From: Peter Lammich <peter.lammich@uni-muenster.de>
Tobias Nipkow wrote:
It turns out that your intuition was right: sledgehammer can prove the
theorem, with a little help. This is the resulting proof (to go into the
library):lemma finite_imp_inj_to_nat_seg:
"finite A ==> EX f n::nat. f`A = {i. i<n} & inj_on f A"
by (metis bij_betw_Inv bij_betw_def finite_imp_nat_seg_image_inj_on)Is there any rule of thumb when to use EX and when to use obtains for
theorems (from a good-style viewpoint, not from the ATP viewpoint)?
Note that metis can also prove the theorem in obtains-style.
regards,
Peter
For a start, notice the formulation in terms of EX rather than
"obtains", which s/h seems to prefer. But still, s/h does not find a
proof. You need to tell it to use finite_imp_nat_seg_image_inj_on:
Last updated: Nov 21 2024 at 12:39 UTC