## Stream: Beginner Questions

### Topic: pending

#### zibo yang (Jun 09 2021 at 12:02):

`````` with ar_nonempty have "a ≠ 0"
proof-
assume "Ar ≠ {}" and "enat a = stop_at init x target" and "a = 0"
then have "0 ∈ reach_steps init x target"
using a_def stop_at.simps[of init x target]
infm.simps[of "reach_steps init x target"]
ar_nonempty
assms(2)
enat_0_iff[of a]
enat.inject[of a "⨅ reach_steps init x target"]
Inf_nat_def1[of Ar]
by auto
then have "geom_proc init x 0 ∈ {0,target}"
using reach_steps_def[of init x target]
then have "init ∈ {0,target}"
using geometric_process[of init x 0]
gambler_rand_walk.simps[of 1 "-1" init 0 x]
then have False
using assms by auto
then show False
``````

I have already proved False, but I still got the error message like:

``````proof (chain)
picking this:
False
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
(Ar ≠ {}) ⟹ (enat a = stop_at init x target) ⟹ (a = 0) ⟹ False
``````

#### zibo yang (Jun 09 2021 at 12:03):

The beginning proof goal is

``````proof (state)
goal (1 subgoal):
1. Ar ≠ {} ⟹ enat a = stop_at init x target ⟹ a ≠ 0
``````

#### zibo yang (Jun 09 2021 at 12:04):

So why it fails using show rather than have

#### Mathias Fleury (Jun 09 2021 at 12:51):

You should really read the Progprove tutorial...

#### Mathias Fleury (Jun 09 2021 at 12:51):

`proof` instead of `proof -`

#### Mathias Fleury (Jun 09 2021 at 12:52):

and why `"Ar ≠ {}" and "enat a = stop_at init x target"` instead of naming the two facts (`ar` is one name)

#### zibo yang (Jun 09 2021 at 13:05):

but It fails using proof rather than proof- like:

``````Failed to apply initial proof method:
using this:
Ar ≠ {}
enat a = stop_at init x target
goal (1 subgoal):
1. a ≠ 0
``````

#### Mathias Fleury (Jun 09 2021 at 13:13):

remove the extra assumptions and it will work

#### zibo yang (Jun 09 2021 at 13:35):

`````` assume ar_nonempty:"Ar ≠ {}"
obtain a::nat where a_def:"a = stop_at init x target"
unfolding stop_at.simps
using only_inf_infm[of Ar] ar_nonempty assms(2) not_infinity_eq[of "infm Ar"]
from ar_nonempty have "a ≠ 0"
proof
assume "Ar ≠ {}" and "a = 0"
then have "0 ∈ reach_steps init x target"
using a_def stop_at.simps[of init x target]
infm.simps[of "reach_steps init x target"]
ar_nonempty
assms(2)
enat_0_iff[of a]
enat.inject[of a "⨅ reach_steps init x target"]
Inf_nat_def1[of Ar]
by auto
then have "geom_proc init x 0 ∈ {0,target}"
using reach_steps_def[of init x target]
then have "init ∈ {0,target}"
using geometric_process[of init x 0]
gambler_rand_walk.simps[of 1 "-1" init 0 x]
then have False
using assms by auto
then show ?thesis
``````

It still doesn't work

#### zibo yang (Jun 09 2021 at 13:37):

the strange thing is that it indicates the proof goal is

``````proof (state)
goal (1 subgoal):
1. Ar ≠ {} ⟹ Ar = {}
``````

#### zibo yang (Jun 09 2021 at 13:38):

under adding "-" behind proof, the goal changes to

``````proof (state)
goal (1 subgoal):
1. Ar ≠ {} ⟹ a ≠ 0
``````

#### zibo yang (Jun 09 2021 at 13:39):

"show" line still implies the same error as before

#### zibo yang (Jun 09 2021 at 13:59):

I think the more straightforward simple question is that:

``````assume ar_nonempty:"Ar ≠ {}"
obtain a::nat where a_def:"a = stop_at init x target"
unfolding stop_at.simps
using only_inf_infm[of Ar] ar_nonempty assms(2) not_infinity_eq[of "infm Ar"]
from ‹Ar ≠ {}› have "a ≠ 0"
proof
assume"Ar ≠ {}" "a = 0"
then show False
``````

why the proof goal after "proof" is:

`````` Ar ≠ {} ⟹ Ar = {}
``````

and why it still shows "Failed to refine any pending goal " for the last line.

#### Mathias Fleury (Jun 09 2021 at 14:07):

``````(*no from*)
have "a ≠ 0"
proof
assume "a = 0"
``````

#### zibo yang (Jun 09 2021 at 14:09):

ok it works

Last updated: Dec 07 2023 at 20:16 UTC