Re: [isabelle] \<^bsub> and \<^esub>



The error message "Failed to refine any pending goal" usually comes from one of the following mistakes:

a) Your show statement does not match a conclusion of a goal (often there is a typo).
b) The assumption that you have "assume"d do not match the assumption of the goal that you are trying to show with "show".

In your case, it is mistake b). In the original lemma statement, the assumption "2 dvd (x::int)*x" was part of the goal, so you have to assume it inside the block. When you rewrite the statement to

lemma
  fixes x :: int
  assumes s: "2 dvd x*x"
  shows "2 dvd x"

then the assumption is already part of the context and no longer of the goal. You can observe this change also in the output buffer when you look at the raw goal state. Nevertheless, you still have the (now superfluous) assume 1: "2 dvd x*x" in your Isar proof. That is, you are making an assumption that is no longer part of the goal state, so you get an error upon show. If you delete this assume and use the assumption from the lemma statement instead, everything should work fine.

Andreas

On 25/02/15 00:41, W. Douglas Maurer wrote:
The annotations in square brackets are called attributes and they have a variety of
purposes. In the case of [algebra] and [presburger], they indeed indicate that these
rules should be used by these proof methods. From what I know, these two methods reason
abstractly, not for concrete numbers like 38. Moreover, I am not familiar with the
internals of try or try0. If you want to see whether algebra can solve this, just write
"by algebra" and see whether this works, too.

In Isabelle2013, try and try0 did not try "algebra", but in Isabelle2014 they do. In the
example I gave (lemma "even((38::int)) <--> ((2::int) dvd (38::int))"), try0 indicated
that this could be solved by presburger, force, simp, auto, or fastforce. I did try "by
algebra" and the error message is: "Failed to apply initial proof method: goal (1
subgoal): 1. even 38 = (2 dvd 38)". Perhaps "algebra" reasons only abstractly, even though
presburger does work on a concrete number like 38.
Now, to my next issue: I was finally able to get a forward proof by contradiction to work;
and then I tried rewriting it using fixes, assumes, and shows, and it no longer works. The
proof I wrote was:
lemma "2 dvd (x::int)*x ==> 2 dvd (x::int)"
proof (rule ccontr)
assume 1: "2 dvd (x::int)*x"
assume "\not ?thesis"
hence "odd(x)" by presburger
hence "odd(x*x)" by simp
hence "\not (2 dvd (x*x))" by presburger
with 1 show False by simp
qed
This proof went through (here ==> represents \Longrightarrow). (Part of the point of this
proof was to illustrate the power of presburger.) But then I tried rewriting the first
line of this using fixes, assumes, and shows, like this: lemma fixes x::"int" assumes s:
"2 dvd x*x" shows "2 dvd x" and now I get an error message under "show" on the last line
(with 1 show False by simp): "Failed to refine any pending goal / Local statement fails to
refine any pending goal / Failed attempt to solve goal by exported rule: (2 dvd x * x) ==>
(\not 2 dvd x) ==> False". It looks as if "with 1" is not picking up the preceding
statement any more, or else that would have been cited as part of the exported rule. Or am
I misunderstanding this? And in any event, what do I have to do to get this to work?
Thanks! -WDMaurer
--
Prof. W. Douglas Maurer       Washington, DC 20052, USA
Department of Computer Science         Tel. (1-202)994-5921
The George Washington University Fax  (1-202)994-4875




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.