Stream: Beginner Questions

Topic: Choice operator on sets?

view this post on Zulip Yiming Xu (Feb 06 2025 at 15:08):

I am aware of the Hilbert Choice operator Eps as in
https://www.isa-afp.org/browser_info/current/HOL/HOL/Hilbert_Choice.html

but I would prefer if there is something applying on sets, rather than predicates. But

find_consts "?'a set ⇒ ?'a"

does not give me that thing. So do we have a set version for Eps? Basically, I would like to take a image of the choice function of a set.

view this post on Zulip Yiming Xu (Feb 06 2025 at 15:32):

There are functions converting between sets and predicates:
Nunchaku.rmember :: "'a set ⇒ 'a ⇒ bool"
Predicate_Compile.contains ::
"'a set ⇒ 'a ⇒ bool"

view this post on Zulip Yiming Xu (Feb 06 2025 at 15:33):

I can compose it with Eps, but I do not know which one to pick, or if there is already something canonical (which makes sledgehammer happier).

view this post on Zulip Mathias Fleury (Feb 06 2025 at 16:07):

Eps has the fancy notation:SOME x. x \in S

view this post on Zulip Yiran Duan (Feb 06 2025 at 21:13):

Hi, though maybe you already did this -- in my very limited experience, proving that the set is not empty should help sledgehammer to get over one barrier

view this post on Zulip Yiming Xu (Feb 06 2025 at 21:26):

Mathias Fleury said:

Eps has the fancy notation:SOME x. x \in S

Thanks! I have confirmed that writing it as \lambda x. ... is indeed the standard way to do this.

view this post on Zulip Yiming Xu (Feb 06 2025 at 21:26):

Yiran Duan said:

Hi, though maybe you already did this -- in my very limited experience, proving that the set is not empty should help sledgehammer to get over one barrier

This is not only helpful, it is a requirement. Without proving the set is nonempty, you cannot do anything with the choice operator.

view this post on Zulip Yiming Xu (Feb 06 2025 at 21:29):

This is because the axiom of choice itself does not tell you that you can pick from the empty set. What sledgehammer does is (not precise!) Skolemization ( pretty much another way to call the axiom of choice). (Write it out just in case that you are not aware of this! In the case you do know about that, yes it is indeed helpful to state explicitly that the set you are picking from is nonempty.) Thanks for your attempt to help!

view this post on Zulip Yiran Duan (Feb 06 2025 at 21:55):

Yiming Xu said:

I have confirmed that writing it as \lambda x. ... is indeed the standard way to do this.

Could you please also expand a bit on this? I'm curious to see what a standard way would be: is it some alternative to e.g. SOME x. x∈A\text{SOME}\ x.\ x \in A?

view this post on Zulip Yiming Xu (Feb 07 2025 at 05:16):

Not essentially. This just means you can converting set membership as λx.x∈s\lambda x. x \in s into a predicate, and then call "Eps". So you can have Choice s defined as Eps (\lambda x. x \in s) to get the desired effect.

view this post on Zulip Mathias Fleury (Feb 07 2025 at 06:14):

Reminder here: choice is very very bad for automation (at least I have never seen someI-involving proofs by sledgehammer). So whenever possible, put the choice in a definition (like MyChoiceDefinition) and add lemmas (so usual assumption ==> MyChoiceDefinition \in s) to be picked up by Sledgehammer

view this post on Zulip Yiming Xu (Feb 07 2025 at 12:00):

Mathias Fleury said:

Reminder here: choice is very very bad for automation (at least I have never seen someI-involving proofs by sledgehammer). So whenever possible, put the choice in a definition (like MyChoiceDefinition) and add lemmas (so usual assumption ==> MyChoiceDefinition \in s) to be picked up by Sledgehammer

Thanks! I think I see it is very bad.

I want to show:

have
"⋀m fl v. ∃wl. asatis tM v (cDIAM m fl) ⟶
length wl = length fl ∧
rel tM m (v # wl) ∧
(∀w f. (w,f) ∈ set (zip wl fl) ⟶ asatis tM w f)"
unfolding asatis.simps
by blast
then obtain cwl where
"⋀m fl v. asatis tM v (cDIAM m fl) ⟹
length (cwl (cDIAM m fl) v) = length fl ∧
rel tM m (v # (cwl (cDIAM m fl) v)) ∧
(∀w f. (w,f) ∈ set (zip (cwl (cDIAM m fl) v) fl) ⟶ asatis tM w f)"
sledgehammer

Note that I only want a choice function from the existence. But sledgehammer does not prove it. How may I help it?

view this post on Zulip Yiming Xu (Feb 07 2025 at 12:01):

image.png
This is the colored goal.

view this post on Zulip Yiming Xu (Feb 07 2025 at 12:03):

Okay it likes this better:
then obtain cwl where
"⋀m fl v. asatis tM v (cDIAM m fl) ⟹
length (cwl m fl v) = length fl ∧
rel tM m (v # (cwl m fl v)) ∧
(∀w f. (w,f) ∈ set (zip (cwl m fl v) fl) ⟶
asatis tM w f)"

view this post on Zulip Mathias Fleury (Feb 07 2025 at 15:27):

wait does you goal hold?

view this post on Zulip Mathias Fleury (Feb 07 2025 at 15:27):

I mean this:

  assume ‹⋀l :: bool. (∃b. b = l)›
  then obtain b where ‹⋀l. b = l›
    sorry

does not hold

view this post on Zulip Mathias Fleury (Feb 07 2025 at 15:28):

As far as I understand, you goal holds if you take cwl m fl v to obtain, not a constant for all possible m, fl, and v

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:29):

Yes cwl is a function. takes three parameters instead of a value.

view this post on Zulip Mathias Fleury (Feb 07 2025 at 15:29):

Manuel wrote a post on how to do this: https://isabelle.zulipchat.com/#narrow/channel/238552-Beginner-Questions/topic/Proving.20lemma.20with.20definite.20description/near/291315915

view this post on Zulip Mathias Fleury (Feb 07 2025 at 15:30):

Yiming Xu said:

Yes cwl is a function. takes three parameters instead of a value.

ah yeah now I see that in your other post

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:31):

It is pretty unhappy if I prove it exists for all m and fl, but want it to give me a function that takes cDIAM m fl.

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:32):

I agree it is reasonable for sledgehammer to dislike it.

view this post on Zulip Mathias Fleury (Feb 07 2025 at 15:35):

hmm depends on cDIAM. If it is the function that ignores the arguments and always returns True, my intuition says that you cannot prove that

You want to have cwl (iDIAM m fl) v right?

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:48):

Yes.

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:49):

And if I obtain a function for cwl m fl v, then do it by hand on case analysis on formulas, and tell sledgehammer to prove that it has the correct effect on cDIAM m fl, then it gives me what I want.

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:50):

I mean, after obtain cwl m fl v, define cwl' by
"cwl ≡ λf. case f of cDIAM m0 fl0 ⇒ cwl0 m0 fl0
|_ ⇒ undefined"

view this post on Zulip Yiming Xu (Feb 07 2025 at 15:51):

That is the flow:

 have
  "⋀m fl v. ∃wl. asatis tM v (cDIAM m fl) ⟶
         length wl = length fl ∧
              rel tM m (v # wl) ∧
              (∀w f. (w,f) ∈ set (zip wl fl) ⟶ asatis tM w f)"
    unfolding asatis.simps
    by blast
  then obtain cwl0 where
  cwl0:"⋀m fl v. asatis tM v (cDIAM m fl) ⟹
           length (cwl0 m fl v) = length fl ∧
              rel tM m (v # (cwl0 m fl v)) ∧
              (∀w f. (w,f) ∈ set (zip (cwl0 m fl v) fl) ⟶
                asatis tM w f)"
  proof -
    assume "⋀cwl. (⋀m fl v. asatis tM v ♢m fl ⟹ length (cwl m fl v) = length fl ∧ rel tM m (v # cwl m fl v) ∧ (∀w f. (w, f) ∈ set (zip (cwl m fl v) fl) ⟶ asatis tM w f)) ⟹ thesis"
    then show ?thesis
      using ‹⋀v m fl. ∃wl. asatis tM v ♢m fl ⟶ length wl = length fl ∧ rel tM m (v # wl) ∧ (∀w f. (w, f) ∈ set (zip wl fl) ⟶ asatis tM w f)› by moura
  qed
  define cwl where "cwl ≡ λf. case f of cDIAM m0 fl0 ⇒ cwl0 m0 fl0
                                                    |_ ⇒ undefined"
  then have
  cwl:"⋀m fl v. asatis tM v (cDIAM m fl) ⟹
           length (cwl (cDIAM m fl) v) = length fl ∧
              rel tM m (v # (cwl (cDIAM m fl) v)) ∧
              (∀w f. (w,f) ∈ set (zip (cwl (cDIAM m fl) v) fl) ⟶
                asatis tM w f)"
    by (simp add: cwl0)

Last updated: Apr 18 2025 at 20:21 UTC