Re: [isabelle] Simpler theorem statements, and proofs for them [Re: Started auction theory toolbox; announcement, next steps, and questions]



Dear Christoph,

Consider the proofs:

lemma 1:
  "ALL i. i < length xs --> xs ! i = hd (drop i xs)"
proof
  fix i
  show "i < length xs --> xs ! i = hd (drop i xs)"
  proof
    assume "i < length xs"
    then show "xs ! i = hd (drop i xs)"
      by (induct i arbitrary: xs) (case_tac xs, simp_all)+
  qed
qed
thm 1
thm 1 [rule_format]


lemma 2:
  "!!i. i < length xs ==> xs ! i = hd (drop i xs)"
proof -
  fix i
  assume "i < length xs"
  then show "xs ! i = hd (drop i xs)"
    by (induct i arbitrary: xs) (case_tac xs, simp_all)+
qed
thm 2

lemma 3:
  assumes "i < length xs"
  shows "xs ! i = hd (drop i xs)"
  using assms
    by (induct i arbitrary: xs) (case_tac xs, simp_all)+
thm 3

I hope the example proofs still cover the structure that was important to you (I changed them only to have some lemma I could actually prove). Note the following points:

1) In lemma 3 we do not explicitly all-quantify i, thus it is handled as "arbitrary but fixed" throughout the proof (and implicitly all-quantified after the proof is finished; in fact "thm 2" and "thm 3" give exactly the same result). This can always be done when we do not need to vary/instantiate i inside the proof itself.

2) The attribute [rule_format] turns (some) HOL connectives into Pure connectives (which are used to present natural deduction style rules in Isabelle, hence the name).

3) For Isar proofs (i.e., structured proofs, as opposed to proof-scripts) the style of lemma 3 is the most idiomatic, if such a style is not possible (since we need to generalize a variable like i), then the style of lemma 2 is the next most idiomatic. As Larry already pointed out, the style of lemma 1 is the least idiomatic nowadays.

hope that helps,

chris

On 11/01/2012 10:20 AM, Christoph LANGE wrote:
2012-10-31 20:09 Lawrence Paulson:
On 31 Oct 2012, at 18:28, Christoph LANGE <c.lange at cs.bham.ac.uk> wrote:
* In statements such as "!x. p x --> q x" it is tedious (and always
the same) to break their structure down to a level where the actually
interesting work starts.

It is almost never necessary or helpful to state a theorem in that
format.

Thanks for your advice!  However simply changing my statements to …

I suggest

     lemma "p x ==> q x"

for a straightforward proof, or

     lemma assumes "p x" shows "q x"

for a more complicated structured proof.

… such a structure doesn't always work; I think the proofs will also
need some adaptation.

The following lemma (reduced to the structural outline) has a
(anti-)pattern that is typical for my formalisation:

lemma skip_index_keeps_non_negativity :
   fixes n::nat and v::real_vector
   assumes non_empty: "n > 0"
     and non_negative: "non_negative_real_vector n v"
   shows "\<forall>i::nat . in_range n i \<longrightarrow>
non_negative_real_vector (n-(1::nat)) (skip_index v i)"
proof
   fix i::nat
   show "in_range n i \<longrightarrow> non_negative_real_vector
(n-(1::nat)) (skip_index v i)"
   proof
     assume "in_range n i"
     ...
     show "non_negative_real_vector (n-(1::nat)) (skip_index v i)" sorry
   qed
qed

How would I have to adapt the proof when rephrasing the statement as
shows "in_range n i \<Longrightarrow> ..." ?

(I'll be happy to accept "RTFM" as an answer, if you could give me a
pointer.)

Cheers, and thanks,

Christoph







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