Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving finiteness

Email Gateway (Aug 18 2022 at 13:40):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,

I wonder whether there is a cheap (best: fully automatic) way for
proving finiteness of sets of the form { f a1...an | a1...an. g a1...an
: S } if S is known to be finite.
Actually, I have some inductive datatype:
datatype ('a,'b,'c) test = A 'a 'b 'c | B 'a 'b

And need to prove the following:
lemma "finite S ==> finite { f a b c | a b c. A a b c : S }"

The only way I succeed to prove this, is to manually convert this into
the form: g ` ({s:S. P s}), where g and P are defined appropriately.
However, this is tedious and I wished to have an automatic way to prove
this.

Thanks in advance for any hints,
Peter

Email Gateway (Aug 18 2022 at 13:40):

From: Alexander Krauss <krauss@in.tum.de>
Hi Peter,

Hmmm... at least you will need to use the fact that g is injective
somehow, because otherwise it might not hold... Imagine g being a
constant function...

Alex

Email Gateway (Aug 18 2022 at 13:40):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Andreas Lochbihler wrote:

Hi Peter,

I wonder whether there is a cheap (best: fully automatic) way for
proving finiteness of sets of the form { f a1...an | a1...an. g a1...an
: S } if S is known to be finite.
In this general case, this is not true, e.g. if g is a constant
function, i.e. not injective, but datatype constructors are injective.

I suggest that you prove some nice lemmata such that the rewriting
works automatically.

Thank you very much, your finite_Collect - lemma is such a nice lemma,
that solved my problem!

Peter

Actually, I have some inductive datatype:
datatype ('a,'b,'c) test = A 'a 'b 'c | B 'a 'b

And need to prove the following:
lemma "finite S ==> finite { f a b c | a b c. A a b c : S }"

For this concrete example, try the following:

lemma Ex_contract:
"(\<exists>a b. P a b) = (\<exists>ab. P (fst ab) (snd ab))"
by auto

This will bundle the multiple existential quantifiers, that are
implicit in the Collect notation into a single one, to which one can
apply image_Collect subsequently. Then, you also need one to get rid
of the function application, e.g.

lemma finite_Collect:
assumes fin: "finite S" and inj: "inj f"
shows "finite {a. f a : S}"
proof -
def S' == "S \<inter> range f"
hence "{a. f a : S} = {a. f a : S'}" by auto
also have "... = (inv f) S'" proof show "{a. f a : S'} <= inv f S'"
using inj by(force intro: image_eqI)
show "inv f S' <= {a. f a : S'}" proof fix x assume "x : inv f S'"
then obtain y where "y : S'" "x = inv f y" by blast
moreover from y : S' obtain x' where "f x' = y"
unfolding S'_def by blast
hence "f (inv f y) = y" unfolding inv_def by(rule someI)
ultimately show "x : {a. f a : S'}" by simp
qed
qed
also have "finite S'" using fin unfolding S'_def by blast
ultimately show ?thesis by simp
qed

With these two lemmata, your lemma is very easy:

lemma "finite S ==> finite { f a b c | a b c. A a b c : S }"
apply(simp only: Ex_contract image_Collect[symmetric])
apply(fastsimp intro: finite_imageI finite_Collect inj_onI)
done

If you massage the simp_set a bit, you will probably be able to do it
in just one step.

Andreas

Email Gateway (Aug 18 2022 at 13:41):

From: Andreas Lochbihler <lochbihl@ipd.info.uni-karlsruhe.de>
Hi Peter,

I wonder whether there is a cheap (best: fully automatic) way for
proving finiteness of sets of the form { f a1...an | a1...an. g a1...an
: S } if S is known to be finite.
In this general case, this is not true, e.g. if g is a constant
function, i.e. not injective, but datatype constructors are injective.

I suggest that you prove some nice lemmata such that the rewriting works
automatically.

Actually, I have some inductive datatype:
datatype ('a,'b,'c) test = A 'a 'b 'c | B 'a 'b

And need to prove the following:
lemma "finite S ==> finite { f a b c | a b c. A a b c : S }"

For this concrete example, try the following:

lemma Ex_contract:
"(\<exists>a b. P a b) = (\<exists>ab. P (fst ab) (snd ab))"
by auto

This will bundle the multiple existential quantifiers, that are implicit
in the Collect notation into a single one, to which one can apply
image_Collect subsequently. Then, you also need one to get rid of the
function application, e.g.

lemma finite_Collect:
assumes fin: "finite S" and inj: "inj f"
shows "finite {a. f a : S}"
proof -
def S' == "S \<inter> range f"
hence "{a. f a : S} = {a. f a : S'}" by auto
also have "... = (inv f) S'" proof show "{a. f a : S'} <= inv f S'"
using inj by(force intro: image_eqI)
show "inv f S' <= {a. f a : S'}" proof fix x assume "x : inv f S'"
then obtain y where "y : S'" "x = inv f y" by blast
moreover from y : S' obtain x' where "f x' = y"
unfolding S'_def by blast
hence "f (inv f y) = y" unfolding inv_def by(rule someI)
ultimately show "x : {a. f a : S'}" by simp
qed
qed
also have "finite S'" using fin unfolding S'_def by blast
ultimately show ?thesis by simp
qed

With these two lemmata, your lemma is very easy:

lemma "finite S ==> finite { f a b c | a b c. A a b c : S }"
apply(simp only: Ex_contract image_Collect[symmetric])
apply(fastsimp intro: finite_imageI finite_Collect inj_onI)
done

If you massage the simp_set a bit, you will probably be able to do it in
just one step.

Andreas

Last updated: May 03 2024 at 04:19 UTC