theory ToyLang_demo
imports Main
begin
\ \ This otherwise useless toy programming language is sufficient for us to get stuck
in interesting ways when doing inductive proofs. \
datatype toy_language =
Skip \ \ do nothing \
| Seq toy_language toy_language \ \ Seq p q = first do p then do q (p; q) \
| Do toy_language \ \ Keep doing p forever while(1) { p } \
\ \ semantics = "small-step transitions"
Intuitively, if semantics p q holds, then p can reduce to q in a single step
\
inductive semantics :: "toy_language \ toy_language \ bool" where
semantics_seq1: "\semantics p p'\ \ semantics (Seq p q) (Seq p' q)"
| semantics_seq2: "\p = Skip\ \ semantics (Seq p q) q"
| semantics_do: "semantics (Do p) (Seq p (Do p))"
\ \ Note: this is very similar to rtranclp!
Intuitively, if big_semantics p q, then
p reduces to q with a (possibly empty) sequence of semantics steps \
inductive big_semantics :: "toy_language \ toy_language \ bool" where
big_semantics1: "big_semantics p p"
| big_semantics2: "\semantics p q; big_semantics q r\ \ big_semantics p r"
\ \ A program is stuck if it can't take any further small steps \
definition stuck where "stuck p = (\q. semantics p q \ False)"
\ \ A program terminates if it can reach a state where it is stuck.
Our programming language is so basic that the only interesting observation
we can make about programs is whether they terminate or not.
\
definition terminates where
"terminates p = (\q. big_semantics p q \ stuck q)"
\ \ As a warm-up exercise, let's prove that Skip terminates \
lemma "terminates Skip"
unfolding terminates_def stuck_def
apply(rule exI[where x=Skip])
\ \ rule_tac x=Skip in exI would also work. \
apply(rule conjI)
apply(rule big_semantics1)
apply(rule allI)
apply(rule impI)
apply(erule semantics.cases)
apply simp+
done
\ \ Btw, this can all be automated:
apply(auto intro: big_semantics.intros elim: semantics.cases)
\
text \ Now, let's prove that Do p doesn't terminate.
The first step is to figure out what lemmas we'll need.
If you're not in a thinking mood, one option is to start
stepping through the proof to see what kind of goal we
get stuck on.
\
lemma "\terminates(Do p)"
unfolding terminates_def stuck_def
apply auto \ \This goal state looks like a suitable lemma, let's prove it!\
oops
text \ Since big_semantics is inductive, it's likely that we'll need to prove
this lemma by induction. But how should we set the induction?
There are many ways to do it, and many ways to go wrong.
We'll try the simplest possible induction first, see where we get stuck,
and try more advanced things as the need arises.
Here are some things to consider to determine if your induction proof is
on the right track:
1. Do the subgoals look true?
2. Are the subgoals simpler than the original statement?
3. Do the induction hypotheses look applicable?
\
text \ First try: structural induction \
lemma terminates_do_lemma:
"big_semantics (Do p) q \ Ex (semantics q)"
apply(induct p)
\ \ Is this a good place to be? Let's apply the tests above!
1. The first subgoal looks true enough: the "reduction orbit" of Do Skip is
Do Skip -> Seq Skip (Do Skip) -> Do Skip -> ...
so clearly another step is always possible.
The other subgoals also look true for similar reasons.
2. The new subgoals don't look simpler in any way: yes we have more structure on p,
but it's not at all obvious how that will help us reason about semantics and
big_semantics, since the semantics_do rule doesn't care what's in the loop body.
3. The induction hypotheses of the second and third subgoal are useless.
For example, neither Do p1 nor Do p2 are in the "reduction orbit" of
Do (Seq p1 p2), so starting from Do (Seq p1 p2) we'll never end up with a
program that looks like the one in the induction hypothesis.
\
oops
text \ Second try: rule induction \
lemma terminates_do_lemma:
"big_semantics (Do p) q \ Ex (semantics q)"
apply(induct rule: big_semantics.induct)
\ \ The second subgoal is easy.
Unfortunately, the first subgoal is clearly false: we need to prove
that every process reduces to something, but Skip doesn't.
It seems that induct ate the (important!) information that the first
argument to big_semantics is a Do.
\
oops
text \ Third try: rule induction but remember that we're starting from Do. \
lemma terminates_do_lemma:
"big_semantics (Do p) q \ Ex (semantics q)"
apply(induct "Do p" q rule: big_semantics.induct)
\ \ The first subgoal is easy. \
apply(force intro: semantics.intros)
\ \ For the second, subgoal, the induction hypothesis is inapplicable:
because we are inducting over things with the shape "Do p", the induction
hypothesis is only applicable if q = Do p. However, that will not be
the case, as we can see from stepping through the proofs a bit: \
apply(erule semantics.cases;clarsimp)
\ \ Maybe we can prove the remaining subgoal as yet another lemma though? \
oops
text \ Fourth try: similar induction, different hypothesis \
lemma terminates_do_lemma_lemma:
"big_semantics (Seq q (Do p)) r \ Ex (semantics r)"
apply(induct "Seq q (Do p)" r rule: big_semantics.induct)
\ \ The first case requires us to prove that a sequential composition can
always reduce, which is true.
However, two things go wrong here:
However, the induction hypothesis in the second case is inapplicable:
clearly, it will not be the case that qa is exactly Seq q (Do p), but
rather Seq q' (Do p) for some other q'.
\
oops
text \ Fifth try: preverse syntactic structure but with arbitrary contents. \
lemma terminates_do_lemma_lemma:
"big_semantics (Seq q (Do p)) r \ Ex (semantics r)"
apply(induct "Seq q (Do p)" r arbitrary: q rule: big_semantics.induct)
\ \ The first case still looks good. (Let's sorry it anyway) \
subgoal sorry
apply(erule semantics.cases;clarsimp) \ \ As for the second case... \
\ \ We solved the problem from the fourth try, but we've gone in
circles: we now require the original lemma after all!
Since these lemmas clearly depend on each other, maybe we can prove them
simultaneously?
\
oops
text \ Sixth try: third try \ fifth try \
\ \ This lemma seems useful for the first case we've had for the past few tries \
lemma nonskip_reduces:
"p \ Skip \ Ex (semantics p)"
apply(induct p)
apply simp
apply clarsimp
apply(case_tac "p1=Skip")
apply(force intro: semantics_seq2)
apply clarsimp
apply(force intro: semantics_seq1)
apply(force intro: semantics_do)
done
lemma terminates_do_lemma:
"big_semantics p s \ p = Seq q (Do r) \ p = Do r \ Ex (semantics s)"
\ \ This one actually goes through! \
apply(induct arbitrary: q r rule: big_semantics.induct)
apply(force intro: nonskip_reduces)
apply(erule disjE;clarsimp)
apply(erule semantics.cases;clarsimp)
apply(erule semantics.cases;clarsimp)
done
lemma "\terminates(Do p)"
unfolding terminates_def stuck_def
by(auto intro: terminates_do_lemma)
text \ Bonus content: "induction on q" path we pursued in the lecture \
lemma terminates_do_lemma_lemma:
"big_semantics (Do p) Skip \ False"
apply(cases rule: big_semantics.cases,assumption)
apply simp
apply(erule semantics.cases;clarsimp)
\ \ Here we'd really want an induction hypothesis. \
oops
\ \ My (Johannes') alternative from the lecture to the disjunction we ended up with above.
This was originally based on a confusion of mine: I was thinking that Do would reduce like this:
Seq (Do p) (Do q) --> Seq p (Seq (Do p) (Do q))
whereas in reality it works like this:
Seq (Do p) (Do q) --> Seq (Seq p Do p) (Do q))
hence the infinite descending chain of auxiliary lemmas I worried about in the lecture
does not in fact happen: the proof above shows that it stabilises after just one.
However, I still find this proof slightly more elegant, even though it turned out to
be overkill to introduce an auxiliary inductive relation:
\
primrec whiley
where "whiley Skip = False"
| "whiley(Do p) = True"
| "whiley(Seq p q) = whiley q"
lemma terminates_do_lemma_lemma:
"big_semantics p Skip \ whiley p \ False"
apply(induct p Skip rule: big_semantics.induct)
apply simp
apply(erule semantics.cases;clarsimp)
done
lemma semantics_whiley_pres:
"semantics p q \ whiley p \ whiley q"
apply(erule semantics.cases;clarsimp)
\ \ meth1;meth2 roughly:
first apply meth1, then apply meth2 to all new subgoals\
done
lemma terminates_do_lemma':
"big_semantics (Do p) q \ Ex (semantics q)"
apply(cases q;clarsimp)
apply(drule terminates_do_lemma_lemma)
apply simp
apply simp
apply(case_tac "x21=Skip")
apply clarify
apply(rule exI)
apply(rule semantics_seq2)
apply simp
apply(force dest: nonskip_reduces intro: semantics_seq1)
apply(force intro: semantics_do)
done
text \ Instead of cases on q, rule induction works well: \
lemma terminates_do_lemma'':
"big_semantics p q \ whiley p \ Ex (semantics q)"
apply(induct rule: big_semantics.induct)
apply(rule nonskip_reduces)
apply(rule ccontr)
apply simp
apply(drule semantics_whiley_pres,assumption)
\ \ meth1,meth2 roughly:
first apply meth1, then apply meth2 to the first subgoal\
apply simp
done
lemma "\terminates(Do p)"
unfolding terminates_def stuck_def
by(auto intro: terminates_do_lemma')
text \ Bonus content: proofs based on questions from the lectures. \
lemma big_semantics_is_rtranclp:
"big_semantics p q = semantics\<^sup>*\<^sup>* p q"
proof(rule iffI)
assume "big_semantics p q"
thus "semantics\<^sup>*\<^sup>* p q"
by(induct rule:big_semantics.induct) auto
next
assume "semantics\<^sup>*\<^sup>* p q"
thus "big_semantics p q"
\ \ The default induction principle (rtranclp.induct) would be supremely annoying to use here:
unlike big_semantics it has the "big step" to the left instead of to the right. \
by(induct rule: converse_rtranclp_induct) (auto intro: big_semantics.intros)
qed
lemma semantics_deterministic:
assumes "semantics p q"
and "semantics p r"
shows "r = q"
using assms
apply(induct arbitrary: r rule: semantics.induct)
apply(erule semantics.cases[where ?a1.0="Seq p q" for p q])
\ \ This highly specific instantiation prevents semantics.cases from being
applied to the first subgoal. \
apply clarsimp
apply(drule_tac x=p' in meta_spec)
apply clarsimp
apply(erule semantics.cases;clarsimp)
apply(drule_tac x=p' in meta_spec)
apply clarsimp
apply(erule semantics.cases;clarsimp)
apply(erule semantics.cases;clarsimp)
apply(erule semantics.cases;clarsimp)
done
text \ Bonus content: exercise \
lemma "terminates (Seq p q) = (terminates p \ terminates q)"
\ \ This will require a fair bit of work. \
oops
end