Stream: Beginner Questions

Topic: pending


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip zibo yang (Jun 09 2021 at 12:04):

So why it fails using show rather than have

view this post on Zulip Mathias Fleury (Jun 09 2021 at 12:51):

You should really read the Progprove tutorial...

view this post on Zulip Mathias Fleury (Jun 09 2021 at 12:51):

proof instead of proof -

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mathias Fleury (Jun 09 2021 at 13:13):

remove the extra assumptions and it will work

view this post on Zulip 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

view this post on Zulip 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 = {}

view this post on Zulip 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

view this post on Zulip zibo yang (Jun 09 2021 at 13:39):

"show" line still implies the same error as before

view this post on Zulip 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.

view this post on Zulip Mathias Fleury (Jun 09 2021 at 14:07):

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

view this post on Zulip zibo yang (Jun 09 2021 at 14:09):

ok it works


Last updated: Sep 25 2022 at 22:23 UTC