## 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 `obtain`ed 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: Dec 07 2023 at 20:16 UTC