Stream: Beginner Questions

Topic: uniqueness proof


view this post on Zulip Artem Khovanov (Aug 01 2022 at 14:07):

I'm trying to prove the following statement (uniqueness in division lemma):

context euclidean_domain
begin

lemma div_unique:
  assumes "a ∈ carrier R - { 𝟬 }" "b ∈ carrier R - { 𝟬 }"
  shows "βˆƒ!q. βˆƒ!r. q ∈ carrier R ∧ r ∈ carrier R ∧ a = (b βŠ— q) βŠ• r ∧ ((r = 𝟬) ∨ (Ο† r < Ο† b))"
    (is "βˆƒ!q. βˆƒ!r. ?quot_rem q r")
proof
  obtain q where "βˆƒr. ?quot_rem q r" using euclidean_function assms by presburger
  show "βˆƒ!r. ?quot_rem q r" sorry
  show "β‹€q'. βˆƒ!r.?quot_rem q' r ⟹ q' = q" sorry
qed

end

The automatic proof rule (sensibly) gives goals
βˆƒ!r. ?quot_rem ?q r and β‹€q'. βˆƒ!r. ?quot_rem q' r ⟹ q' = ?q.
However, when I attempt to pass in the obtained variable q for ?q as above, I get the error
Result contains obtained parameters: q. Local statement fails to refine any pending goal
What am I doing wrong? How can I pass the variable from an existential operator into another proof?

view this post on Zulip Artem Khovanov (Aug 01 2022 at 14:10):

Here's a more minimal (trivial) example of the issue:

lemma test:
  assumes "βˆƒ x. P x"
  shows "βˆƒx. P x"
proof
  obtain x where "P x" using assms by auto
  thus "P x" by auto
qed

gives the same error at thus.

view this post on Zulip Fabian Huch (Aug 01 2022 at 14:20):

An easy fix for that is to first have your property with the obtained variable, then show the existence statement from that:

proof -
  obtain x where "P x" using assms by auto
  then have "P x" by auto
  thus "βˆƒx. P x" by auto
qed

I don't know if there is a more elegant way though.

view this post on Zulip Artem Khovanov (Aug 01 2022 at 14:22):

Fabian Huch said:

An easy fix for that is to first have your property with the obtained variable, then show the existence statement from that:

proof -
  obtain x where "P x" using assms by auto
  then have "P x" by auto
  thus "βˆƒx. P x" by auto
qed

I don't know if there is a more elegant way though.

Hmm.. but then in the first (existence + uniqueness) case I can't unpack the operator into existence and uniqueness bits, because then it'll unpack the existence part too far for this fix to work.

view this post on Zulip Artem Khovanov (Aug 01 2022 at 14:25):

For example, if I would like to prove

lemma test:
  assumes "βˆƒ x. P x" "⟦P a; P b⟧ ⟹ a = b"
  shows "βˆƒ!x. P x"
proof
  obtain x where "P x" using assms by auto
  show "P x" by auto
  thus "β‹€x'. P x' ⟹ x' = x" by auto
qed

view this post on Zulip Fabian Huch (Aug 01 2022 at 14:32):

Well you can do the same thing:

  have "P x" sorry
  moreover have "β‹€y. P y ⟹ y = x" sorry
  ultimately have "βˆƒ!x. P x" by blast

Ultimately, it shouldn't matter except for style - you can always first have what you show.

view this post on Zulip Artem Khovanov (Aug 01 2022 at 14:33):

Fabian Huch said:

Well you can do the same thing:

  have "P x" sorry
  moreover have "β‹€y. P y ⟹ y = x" sorry
  ultimately have "βˆƒ!x. P x" by blast

Ultimately, it shouldn't matter except for style - you can always first have what you show.

Ah right yep thanks!

view this post on Zulip Artem Khovanov (Aug 01 2022 at 14:56):

Here is another workaround I found (it looks silly here, but is good for longer proofs):

lemma test:
  assumes "βˆƒ x. P x"
  shows "βˆƒx. P x"
proof-
  obtain x where "P x" using assms by auto
  show "βˆƒx. P x"
  proof
    show "P x" using `P x` .
  qed
qed

view this post on Zulip Jan van BrΓΌgge (Aug 01 2022 at 15:21):

This is maybe a bit shorter:

lemma test:
  assumes "βˆƒ x. P x"
  shows "βˆƒx. P x"
proof-
  obtain x where "P x" (is "?P x") using assms by auto
  show "βˆƒx. P x" by (rule exI[of ?P, OF `?P x`])
qed

Last updated: Feb 27 2024 at 08:17 UTC