Stream: Beginner Questions

Topic: uniqueness proof

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?

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.

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.

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.

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

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.

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!

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

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: Apr 25 2024 at 08:20 UTC