Clever Geek Handbook

Taming the meta-implication in Isar proofs

Having proved a simple theorem, I ran into metalevel implications in the proof. Is it good for them to have them or can they be avoided? If I handle them, is this the correct way to do it?

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 think it could be proved more easily, but I wanted to have a structured proof.

+3


source to share


2 answers


Basically, meta-implication is ==>

nothing to avoid (in fact, this is the "native" way of expressing inference rules in Isabelle). There is a canonical way that often avoids meta-implication when writing Isar proofs. For example, for a general purpose

"!!x. A ==> B"

we can write to Isar

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


In your specific example, looking at it in Isabelle / jEdit, you may notice that the n

second case is highlighted. The reason is that it is a free variable. While this is not a problem in itself, it is more canonical to fix such variables locally (for example, the typical "for arbitrary but fixed ..." statement in textbooks). For example.

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 again you can see how fix

/ assume

/ show

in Isar matches the actual target, i.e.

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


source


When writing structured evidence, it is best to avoid meta-implication (and quantification) for the outermost subcell structure. That is, instead of talking about

⋀x. P x ⟹ Q x ⟹ R x

you must use

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

If P x

u Q x

have some structure, it is good to use meta-implication and -quantification for them.

There are several reasons to prefer fix

/ assumes

over metaoperators in structured proofs.



  • Somewhat trivial, you don't need to specify them again in every view and show them.

  • More importantly, when you use a fix

    variable to quantify, it remains the same throughout the evidence. If you use ⋀

    it will only count in each expression have

    (and doesn't exist outside). This makes it impossible to access this variable directly and often complicates the search space for automated tools. Similar things are saved for assume

    vs ⟹

    .

  • A more difficult point is the behavior show

    in the presence of meta-implications. Consider the following attempt at proof:

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

    After the command, proof

    there are two subtles: P ⟹ Q

    and Q ⟹ P

    . However, the final qed

    fails. How did this happen?

    The first show

    applies the rule P ⟹ Q

    to the first applicable sub-slice, viz P ⟹ Q

    . Using the usual Isabelle rule resolution mechanism this gives P ⟹ P

    ( assume P

    show Q` would remove the subheading).

    The second show

    applies the rule Q ⟹ P

    to the first applicable subgoal: now it is P ⟹ P

    (since it Q ⟹ P

    is the second subgoal) returning again P ⟹ Q

    .

    As a result, we still have two of fraud P ⟹ Q

    and Q ⟹ P

    and qed

    can not close the goal.

    In many cases, we do not notice this behavior show

    , since trivial subgoals such as P ⟹ P

    can be solved using qed

    .

A few words about behavior show

: As we saw above, the meta-implication show

does not match assume

. Instead, it corresponds to assume

less known brother presume

. presume

allows you to introduce new assumptions, but requires you to fulfill them. Compare as an example

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
+3


source






More articles:


All Articles