```
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]
by (simp add: zero_enat_def)
then have "init ∈ {0,target}"
using geometric_process[of init x 0]
gambler_rand_walk.simps[of 1 "-1" init 0 x]
by (simp add: zero_enat_def)
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
```

The beginning proof goal is

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

So why it fails using show rather than have

You should really read the Progprove tutorial...

`proof`

instead of `proof -`

and why `"Ar ≠ {}" and "enat a = stop_at init x target"`

instead of naming the two facts (`ar`

is one name)

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

remove the extra assumptions and it will work

```
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"]
by (auto simp add: not_infinity_eq)
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]
by (simp add: zero_enat_def)
then have "init ∈ {0,target}"
using geometric_process[of init x 0]
gambler_rand_walk.simps[of 1 "-1" init 0 x]
by (simp add: zero_enat_def)
then have False
using assms by auto
then show ?thesis
```

It still doesn't work

the strange thing is that it indicates the proof goal is

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

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

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

"show" line still implies the same error as before

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"]
by (auto simp add: not_infinity_eq)
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.

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

ok it works

Last updated: Sep 11 2024 at 16:22 UTC