Taming meta implication in Isar proofs

Question

Proving a simple theorem I came across meta-level implications in the proof. Is it OK to have them or could they be avoided? If I should handle them, is this the right way to do so?

theory Sandbox
imports Main
begin

lemma "(x::nat) > 0 ∨ x = 0"
proof (cases x)
  assume "x = 0"
  show "0 < x ∨ x = 0" by (auto)
next
  have "x = Suc n ⟹ 0 < x" by (simp only: Nat.zero_less_Suc)
  then have "x = Suc n ⟹ 0 < x ∨ x = 0" by (auto)
  then show "⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0" by (auto)
qed

end

I guess this could be proved more easily but I wanted to have a structured proof.

Answer 1

In principle meta-implication ==> is nothing to be avoided (in fact its the "native" way to express inference rules in Isabelle). There is a canonical way that often allows us to avoid meta-implication when writing Isar proofs. E.g., for a general goal

"!!x. A ==> B"

we can write in Isar

fix x
assume "A"
...
show "B"

For your specific example, when looking at it in Isabelle/jEdit you might notice that the n of the second case is highlighted. The reason is that it is a free variable. While this is not a problem per se, it is more canonical to fix such variables locally (like the typical statement "for an arbitrary but fixed ..." in textbooks). E.g.,

next
  fix n
  assume "x = Suc n"
  then have "0 < x" by (simp only: Nat.zero_less_Suc)
  then show "0 < x ∨ x = 0" ..
qed

Here it can again be seen how fix/assume/show in Isar corresponds to the actual goal, i.e.,

1. ⋀nat. x = Suc nat ⟹ 0 < x ∨ x = 0

Answer 2

When writing structured proofs, it is best to avoid meta-implication (and quantification) for the outermost structure of the subgoal. I.e. instead of talking about

⋀x. P x ⟹ Q x ⟹ R x

you should use

fix x
assume "P x" "Q x"
...
show "R x"

If P x and Q x have some structure, it is fine to use meta-implication and -quantification for these.

There is a number of reasons to prefer fix/assumes over the meta-operators in structured proofs.

• Somewhat trivially, you do not have to state them again in every have and show statement.

• More important, when you use fix to quantify a variable, it stays the same in the whole proof. If you use ⋀, it is freshly quantified in each have statement (and doesn't exist outside). This makes it impossible to refer to this variable directly and often complicates the search space for automated tools. Similar things hold for assume vs ⟹.

• A more intricate point is the behaviour of show in the presence of meta-implications. Consider the following proof attempt:

  lemma "P ⟷ Q"
  proof
    show "P ⟹ Q" sorry
  next
    show "Q ⟹ P" sorry
  qed
  

  After the proof command, there are two subgoals: P ⟹ Q and Q ⟹ P. Nevertheless, the final qed fails. How did this happen?

  The first show applies the rule P ⟹ Q to the first applicable subgoal, namely P ⟹ Q. Using the usual rule resolution mechanism of Isabelle, this yields P ⟹ P (assume Pshow Q` would have removed the subgoal).

  The second show applies the rule Q ⟹ P to the first applicable subgoal: This is now P ⟹ P (as Q ⟹ P is the second subgoal), yielding P ⟹ Q again.

  As a result, we are still have the two subgoals P ⟹ Q and Q ⟹ P and qed cannot close the goal.

  In many cases, we don't notice this behaviour of show, as trivial subgoals like P ⟹ P can be solved by qed.

A few words on the behavior of show: As we have seen above, meta-implication in show does not correspond to assume. Instead, it corresponds to assumes lesser known brother, presume. presume allows you to introduce new assumptions, but requires you to discharge them afterwards. As an example, compare

lemma "P 2 ⟹ P 0"
proof -
  presume "P 1" then show "P 0" sorry
next
  assume "P 2" then show "P 1" sorry
qed

and

lemma "P 2 ⟹ P 0"
proof -
  show "P 1 ⟹ P 0" sorry
next
  assume "P 2" then show "P 1" sorry
qed