## 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: Sep 11 2024 at 16:22 UTC