4

I found a surprising behaviour (for me) when using Isar. I try to use assume and sometimes Isar complains it cannot resolve pending goals, for example my most typical example is having a an assumption and not being able to assume it:

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

though the following does work:

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

which is not terribly surprising.

But the next one is surprising to me that it works given that my first example failed:

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

why is the first one different from the second one?

Error msg:

Failed to refine any pending goal 
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
  (A) ⟹ A
Charlie Parker
  • 5,884
  • 57
  • 198
  • 323

1 Answers1

4

You can find an answer in "Chapter 6: Proofs" of the document Isar-ref. Ideally, you wish to read through the introduction to the chapter, as well as sections 6.1 and 6.2 to fully resolve your concerns. Below, I present the most relevant passages:

The logical proof context consists of fixed variables and assumptions.

...

Similarly, introducing some assumption χ has two effects. On the one hand, a local theorem is created that may be used as a fact in subsequent proof steps. On the other hand, any result χ ⊢ φ exported from the context becomes conditional wrt. the assumption: ⊢ χ ==> φ. Thus, solving an enclosing goal using such a result would basically introduce a new subgoal stemming from the assumption. How this situation is handled depends on the version of assumption command used: while assume insists on solving the subgoal by unification with some premise of the goal, presume leaves the subgoal unchanged in order to be proved later by the user.

Let us look at your first example:

lemma 
  assumes "A"
  shows "A"
proof -
  assume "A"
  from this show "A" by (simp)
qed

There is only one subgoal with no premises: A. Given that there are no premises, 'unification with premises' is inapplicable.

In the second example,

lemma 
  shows "A⟹A"
proof -
  assume "A"
  from this show "A" by simp
qed

the subgoal is A⟹A with the premise A. Thus, you can use assume: unification can be performed.

Lastly,

lemma 
  assumes "A"
  shows "A"
proof -
  have "A" by (simp add: assms)
  from this show "A" by (simp)
qed

is different from the previous cases, because you do not introduce any assumptions. Therefore, you can use show to discharge the subgoal. It should be noted that from this show "A" by (simp) is identical to from assms show "A" by simp or, better yet, from this show "A".:

lemma 
  assumes "A"
  shows "A"
proof -
  from assms show "A".
qed
user9716869 - supports Ukraine
  • 1,911
  • 2
  • 14
  • 24
  • so basically if one does an `assume` there is a "state" within Isabelle itself that keeps track one what the next command is supposed to do? i.e. if I do `assume` then `show` the future `shows` would insist on doing unification of the assumptions of the goal to the assumed fact. Right? – Charlie Parker May 29 '20 at 18:24
  • If my understanding of your questions is correct, you are thinking along the right lines (modulo the wording/terminology). Indeed, if a given assumption can be unified with a premise in the first subgoal, but not in the subsequent subgoals, you need to start a fresh block in the sub-proof by using the command `next` (see section 6.1.2 in Isar-ref): this will reset the local proof context (including the assumptions stated using the command `assume`). Otherwise, you will not be able to proceed with the proof. – user9716869 - supports Ukraine May 29 '20 at 18:45
  • 1
    I don't understand why Isar is implemented this way. Who cares if there are a few extra assumptions. There are smart tactics (as simple as `simp`) that only use the relevant facts. Why can't that be the implementation and ignore whatever is irrelevant (that seems to be happening for `have`) – Charlie Parker May 29 '20 at 21:16
  • @CharlieParker I am not an authority on the implementation of Isar. You can read all about this topic in the PhD thesis of Makarius Wenzel, e.g. https://mediatum.ub.tum.de/doc/601724/601724.pdf. However, as a side note, overall, I have an impression that you simply did not yet get used to the way things work in Isabelle/Isar/HOL. It takes time to appreciate various aspects of the system. Once you can say with confidence that you understand all implementation details, then it may be worth trying to change some of them. Personally, I am not at this stage yet :). – user9716869 - supports Ukraine May 29 '20 at 21:30
  • I'm just a curious fellow :) Thanks for the feedback will check it out. I'm still very curious to what is wrong why my approach of introducing assumptions. I always thought `assume` was similar to just appending to the assumptions list `[| A1; ..., An |]` but there seems to be some subtly going on that I don't appreciate at this time. Thanks for the feedback! – Charlie Parker May 29 '20 at 22:01
  • let me try this question help me understand. What is the keyword `assume` really doing? – Charlie Parker May 29 '20 at 22:31
  • 1
    @CharlieParker The beginning of my answer contains a passage from the manual that explains this. `assume` creates a local fact φ ⊢ φ (by assumption) that may be used in subsequent proof steps. In essence, loosely, you use `assume` in a manner similar to the way you would apply a deduction theorem in a proof in predicte calculus (e.g. see https://en.wikipedia.org/wiki/Deduction_theorem). – user9716869 - supports Ukraine May 29 '20 at 23:43
  • @CharlieParker A general advice is to keep going through various examples, reading tutorials and books on the subject, trying to formalize proofs from textbooks. Understanding and intuition will come at some point in time. – user9716869 - supports Ukraine May 29 '20 at 23:47