Stream: Beginner Questions

Topic: Why unfolding Bex_def, bex_triv does not work here?

Yiming Xu (Dec 07 2024 at 15:43):

I have a goal looks like this:

⋀a b. ∃x. x ∈ s ∧ a = cVAR x ⟹
           ∃x. x ∈ tau ∧ (∃xa. xa ∈ {fl. ∀f. f ∈ set fl ⟶ f ∈ DPM n s tau} ∧ b = ♢x xa) ⟹
           (a, b) ∉ cequivr TYPE('a)

I want to eliminate:

(∃xa. xa ∈ {fl. ∀f. f ∈ set fl ⟶ f ∈ DPM n s tau} ∧ b = ♢x xa)

But I tried both bex_triv and Bex_def and none of them works.

As a reminder:

  Set.Bex_def: Bex ?A ?P = (∃x. x ∈ ?A ∧ ?P x)
  Set.bex_triv: (∃x∈?A. ?P) = ((∃x. x ∈ ?A) ∧ ?P)

May I please ask why unfolding bex_triv Bex_def does not make change on this goal?

Mathias Fleury (Dec 07 2024 at 15:54):

Side remark: there is no Bex in (∃xa. xa ∈ {fl. ∀f. f ∈ set fl ⟶ f ∈ DPM n s tau} ∧ b = ♢x xa), so unfolding will not (and cannot) do anything.

Mathias Fleury (Dec 07 2024 at 15:55):

Side remark 2: unfolding is not what you want. You want to replace ∃x. P x ==> thesis by !!x. P x ==> thesis. This is not something unfolding can do (not equivalence preserving).

Mathias Fleury (Dec 07 2024 at 15:57):

And now you know that you want an elim rule and not an unfolding: apply (elim exE)

Mathias Fleury (Dec 07 2024 at 15:59):

There is a bexE with the meaning you can guess if you a bex instead of an ex quantifier

Yiming Xu (Dec 07 2024 at 16:05):

Oh I did not note that I have already eliminated the Bex! Silly me! Alles klar.

Yiming Xu (Dec 07 2024 at 16:06):

But as for "elim exE", I am repeatedly told to avoid apply. And I would do the unfolding before opening a proof-qed block.

Yiming Xu (Dec 07 2024 at 16:06):

Let me try to find an iff thm that does this for me.

Yiming Xu (Dec 07 2024 at 16:08):

I find this:

  HOL.atomize_exL: (⋀x. ?P x ⟹ ?Q) ≡ (∃x. ?P x ⟹ ?Q)

Yiming Xu (Dec 07 2024 at 16:09):

I like this one but its direction is wrong for unfolding. Is that any function that flips an equality that I can call without go to ML level?

irvin (Dec 07 2024 at 16:10):

Yiming Xu said:

But as for "elim exE", I am repeatedly told to avoid apply. And I would do the unfolding before opening a proof-qed block.

Can't you do
proof(elim exE)
....

Yiming Xu (Dec 07 2024 at 16:11):

Mathias Fleury said:

Side remark 2: unfolding is not what you want. You want to replace ∃x. P x ==> thesis by !!x. P x ==> thesis. This is not something unfolding can do (not equivalence preserving).

I think this is "((?x. P x) ==> ?thesis)\equiv (!!x. P x ==> ?thesis)", so we can retrieve an equivalence.

irvin (Dec 07 2024 at 16:13):

If you want an isar block you can also do something like
lemma"∃x. P x"
proof -
fix x
have "P x"
by sorry
then show "∃x. P x"
by(rule exI)
qed

Yiming Xu (Dec 07 2024 at 16:13):

irvin said:

Yiming Xu said:

But as for "elim exE", I am repeatedly told to avoid apply. And I would do the unfolding before opening a proof-qed block.

Can't you do
proof(elim exE)
....

I can do that as well. Thank you! Using more equivalence might just be my personal preference.

Yiming Xu (Dec 07 2024 at 16:14):

Since the HOL4 style tends to prefer simplification (i.e. iff) than implication...

Yiming Xu (Dec 07 2024 at 16:17):

After 3 months, I find the style I prefer in Isar is to avoid opening a proof block once possible and keep using equality for reasoning. I tend to believe that looks neater. (Sadly I need more time to actually achieve this...)

Mathias Fleury (Dec 07 2024 at 16:21):

irvin said:

If you want an isar block you can also do something like
lemma"∃x. P x"
proof -
fix x
have "P x"
by sorry
then show "∃x. P x"
by(rule exI)
qed

obtain x where "P x" is the syntax you are looking for.

irvin (Dec 07 2024 at 16:24):

Mathias Fleury said:

irvin said:

If you want an isar block you can also do something like
lemma"∃x. P x"
proof -
fix x
have "P x"
by sorry
then show "∃x. P x"
by(rule exI)
qed

obtain x where "P x" is the syntax you are looking for.

oh my bad yup mathias is right
for clarification

lemma
  "∃x. P x ⟹ Q"
proof -
  assume "∃x. P x"
  then obtain x where "P x" ..

  then show "Q"
    by sorry
qed

Mathias Fleury (Dec 07 2024 at 16:25):

Yiming Xu said:

Mathias Fleury said:

Side remark 2: unfolding is not what you want. You want to replace ∃x. P x ==> thesis by !!x. P x ==> thesis. This is not something unfolding can do (not equivalence preserving).

I think this is "((?x. P x) ==> ?thesis)\equiv (!!x. P x ==> ?thesis)", so we can retrieve an equivalence.

Yeah you are right that it is equivalent, but the scope of x changes from only P x to the entire formula.

Mathias Fleury (Dec 07 2024 at 16:26):

This is the equivalence you are looking for:

unfolding ex_neg_all_pos

Mathias Fleury (Dec 07 2024 at 16:28):

irvin said:
for clarification

lemma
  "∃x. P x ⟹ Q"
proof -
  assume "∃x. P x"
  then obtain x where "P x" ..

  then show "Q"
    by sorry
qed

If you go for Isar, let's use full Isar:

lemma
  assumes P: "∃x. P x"
  shows "Q"
proof -
  obtain x where "P x" using P ..

  then show "Q"
    sorry
qed

Yiming Xu (Dec 07 2024 at 18:13):

irvin said:

Mathias Fleury said:

irvin said:

If you want an isar block you can also do something like
lemma"∃x. P x"
proof -
fix x
have "P x"
by sorry
then show "∃x. P x"
by(rule exI)
qed

obtain x where "P x" is the syntax you are looking for.

oh my bad yup mathias is right
for clarification

lemma
  "∃x. P x ⟹ Q"
proof -
  assume "∃x. P x"
  then obtain x where "P x" ..

  then show "Q"
    by sorry
qed

Incidently, I would like to ask about the difference between "rule" and "intro". Sometimes "intro thm" works but "rule thm" does not. Why is the case?

Yiming Xu (Dec 07 2024 at 18:15):

Mathias Fleury said:

Yiming Xu said:

Mathias Fleury said:

Side remark 2: unfolding is not what you want. You want to replace ∃x. P x ==> thesis by !!x. P x ==> thesis. This is not something unfolding can do (not equivalence preserving).

I think this is "((?x. P x) ==> ?thesis)\equiv (!!x. P x ==> ?thesis)", so we can retrieve an equivalence.

Yeah you are right that it is equivalent, but the scope of x changes from only P x to the entire formula.

Yes, you can omit the brackets because the meta implication separates its LHS and RHS.

Mathias Fleury (Dec 07 2024 at 18:22):

Yiming Xu said:

irvin said:

Mathias Fleury said:

irvin said:

If you want an isar block you can also do something like
lemma"∃x. P x"
proof -
fix x
have "P x"
by sorry
then show "∃x. P x"
by(rule exI)
qed

obtain x where "P x" is the syntax you are looking for.

oh my bad yup mathias is right
for clarification

lemma
  "∃x. P x ⟹ Q"
proof -
  assume "∃x. P x"
  then obtain x where "P x" ..

  then show "Q"
    by sorry
qed

Incidently, I would like to ask about the difference between "rule" and "intro". Sometimes "intro thm" works but "rule thm" does not. Why is the case?

IIRC the main difference comes from the handling of the facts in the context: using YY apply (rule X) requires X to generate an assumption that can be matched with YY

Yiming Xu (Dec 07 2024 at 22:52):

Mathias Fleury said:

Yiming Xu said:

irvin said:

Mathias Fleury said:

irvin said:

If you want an isar block you can also do something like
lemma"∃x. P x"
proof -
fix x
have "P x"
by sorry
then show "∃x. P x"
by(rule exI)
qed

obtain x where "P x" is the syntax you are looking for.

oh my bad yup mathias is right
for clarification

lemma
  "∃x. P x ⟹ Q"
proof -
  assume "∃x. P x"
  then obtain x where "P x" ..

  then show "Q"
    by sorry
qed

Incidently, I would like to ask about the difference between "rule" and "intro". Sometimes "intro thm" works but "rule thm" does not. Why is the case?

IIRC the main difference comes from the handling of the facts in the context: using YY apply (rule X) requires X to generate an assumption that can be matched with YY

So, in the case that there is no assumption in the context at all, does it mean that I cannot use rule at all?

Mathias Fleury (Dec 08 2024 at 06:26):

You can. But if you have one, it must match.

Mathias Fleury (Dec 08 2024 at 06:27):

Try this with and without the using P:

lemma
  assumes P: "∃x. P x"
  shows "Q ⟶ Q"
  using P
  apply (rule impI)

Mathias Fleury (Dec 08 2024 at 06:27):

And then replace the rule by intro with the using P

Yiming Xu (Dec 08 2024 at 06:35):

Mathias Fleury said:

Try this with and without the using P:

lemma
  assumes P: "∃x. P x"
  shows "Q ⟶ Q"
  using P
  apply (rule impI)

With using P it does not work, it works only without using P.
I guess it it because with the P the goal is (?x. P x) ==> Q --> Q, so the top level is a ==>, not -->, so it does not find a match. (let me rethink.)

Yiming Xu (Dec 08 2024 at 06:36):

And for intro, both with and without P works.

Mathias Fleury (Dec 08 2024 at 06:39):

Yiming Xu said:

Mathias Fleury said:

Try this with and without the using P:

lemma
  assumes P: "∃x. P x"
  shows "Q ⟶ Q"
  using P
  apply (rule impI)

With using P it does not work, it works only without using P.
I guess it it because with the P the goal is (?x. P x) ==> Q --> Q, so the top level is a ==>, not -->, so it does not find a match. (let me rethink.)

No that is not it. Q --> Q is transformed by rule into Q ==> Q. So rule is now checking if (?x. P x) matches the first goal: it does not, so it is failing.

Here is a working example:

lemma
  assumes P: "∃x. P x"
  shows "(∃x. P x) ⟶ (∃x. P x)"
  using P
  apply (rule impI)

Yiming Xu (Dec 08 2024 at 06:39):

So, for using rule, with
impI: (P ⟹ Q) ⟹ P ⟶ Q
on the goal
(?x. P x) ==> Q --> Q
We want the application of the rule impI to generate an assumption that matches (?x. P x).
But the application will generate the assumption Q.

Yiming Xu (Dec 08 2024 at 06:40):

And Q is not an existential.

Yiming Xu (Dec 08 2024 at 06:41):

Mathias Fleury said:

Yiming Xu said:

Mathias Fleury said:

Try this with and without the using P:

lemma
  assumes P: "∃x. P x"
  shows "Q ⟶ Q"
  using P
  apply (rule impI)

With using P it does not work, it works only without using P.
I guess it it because with the P the goal is (?x. P x) ==> Q --> Q, so the top level is a ==>, not -->, so it does not find a match. (let me rethink.)

No that is not it. Q --> Q is transformed by rule into Q ==> Q. So rule is now checking if (?x. P x) matches the first goal: it does not, so it is failing.

Here is a working example:

lemma
  assumes P: "∃x. P x"
  shows "(∃x. P x) ⟶ (∃x. P x)"
  using P
  apply (rule impI)

Aha I think that is what I got just a few seconds ago! Now I think I get it!

Yiming Xu (Dec 08 2024 at 06:41):

Thanks a lot! These comparisons are always helpful.

Last updated: Dec 21 2024 at 16:20 UTC