Transcript slides

Proving Facts About Programs
With a Proof Assistant
John Wallerius
An Example From:
Isabelle/HOL,
A Proof Assistant for Higher Order Logic,
By T. Nipkow, L Paulson and M. Wenzel
A Simple Example Using Lists
• Specify data types (e.g. polymorphic lists,
trees) using ML-like syntax:
datatype 'a list = Nil
("[]")
| Cons 'a “ 'a list " (infixr "#" 65)
Specify functions:
Append and Reverse
consts app :: “ 'a list => 'a list => 'a list"
rev :: “ 'a list => 'a list"
primrec
"[] @ ys
= ys"
"(x # xs) @ ys = x # (xs @ ys)"
primrec
"rev []
= []"
"rev (x # xs) = (rev xs) @ (x # [])"
(infixr "@" 65)
State a Theorem to Prove
• Simple Example: Reversing the reverse of a
list gives back the original list:
• theorem rev_rev [simp]: "rev(rev xs) = xs“
• This command names and states a theorem.
• When proved, future proofs will use it for
simplifications
Try a Proof Procedure: Induction
•
•
•
•
theorem rev_rev [simp]: "rev(rev xs) = xs“
Try induction on variable xs:
apply(induct_tac xs)
System responds with new proof state
subgoals:
– 1. rev (rev []) = []
– 2.  a list.
rev (rev list) = list  rev (rev(a # list)) = a # list
Simplify
• Current state
– 1. rev (rev []) = []
– 2.  a list.
rev (rev list) = list  rev (rev(a # list)) = a # list
• Invoke Simplifier:
• apply(auto)
• New state after first subgoal is completely solved
– 1.  a list.
rev (rev list) = list  rev (rev(a # list)) = a # list
A Simpler Lemma is Needed
• lemma rev_app [simp]:
"rev(xs @ ys) = (rev ys) @ (rev xs)“
• Actually, this can’t be proved immediately
either. We first need to prove a yet simpler
lemma:
• lemma app_Nil2 [simp]: "xs @ [] = xs“
• This one is proved by:
• apply(induct_tac xs); apply(auto)
The Final Proof
lemma app_Nil2 [simp]: "xs @ [] = xs"
lemma app_assoc [simp]:
"(xs @ ys) @ zs = xs @ (ys @ zs)"
lemma rev_app [simp]:
"rev(xs @ ys) = (rev ys) @ (rev xs)"
theorem rev_rev [simp]: "rev(rev xs) = xs"
Review
•
Standard proof procedure:
–
–
–
–
•
State a goal
Proceed until lemma is needed
Prove lemma
Return to original
Good strategy for functional programs:
1. Induction, then
2. All out simplification