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?

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`

.

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.

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.

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
```

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`

.

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!

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
```

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