CODEWITHSUNDEEP
isabelle
Patrick Stevens
Patrick Stevens

Reputation: 579

Isabelle failed to finish proof even though this is same as goal

My code is as follows. I expected it to work perfectly, and indeed by the end of the final "hence" line (which was found by Sledgehammer), Isabelle claims that this is ∀y. ∃x. P x y, and that its goal has one subgoal only which is ∀y. ∃x. P x y. These two expressions are identical, so I would have thought Isabelle would accept the proof as finished.

lemma assumes "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof -
 fix y
 assume "EX x. ALL f. P x f"
 then obtain x where "ALL f. P x f" by blast
 hence "P x y" by blast
 hence "ALL y. EX x. P x y" using `∀f. P x f` by blast
qed

What have I missed? I'm a beginner in Isabelle, as is probably evident.

Upvotes: 1

Views: 555

Answers (1)

Andreas Lochbihler
Andreas Lochbihler

Reputation: 5058

The commands have and hence only state intermediate facts that you wish to prove. You have to say explicitly that a statement is supposed to discharge a goal. To do that, you have to use show or thus instead of have or hence. So if you replace your last hence with thus, the proof should succeed (modulo the remarks below). You can also see in the Output buffer (or by hovering with the mouse over thus that you get a message saying Successful attempt to solve goal by exported rule .... This indicates that the goal was really discharged.

By the way, the proof will not work as expected. First, in the initial step where you write proof -, you actually want to do introduction for the universal quantifier (as you fix the y in the next step. Therefore, the - should be replaced with the appropriate rule application, namely (rule allI). Consequently, your show statement should then be EX x. P x y rather than ALL y. EX x. P x y.

Second, the assumes in the lemma statement already adds the assumption to the context. Therefore, there is no need to assume it once more inside the proof. In fact, Isabelle will complain at show or thus that it is unable to solve the goal. So you should delete the assume ... part and replace it with a reference to the assumption, e.g., using the predefined name assms.

Upvotes: 2

Related Questions