zibo yang (Jun 09 2021 at 12:02): 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]
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
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
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"]
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
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 = {}
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
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"]
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.
Mathias Fleury (Jun 09 2021 at 14:07):(*no from*)
have "a ≠ 0"
proof
assume "a = 0"
ok it works
Last updated: Apr 26 2024 at 12:28 UTC