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