Email Gateway (Aug 19 2022 at 15:57): Email Gateway (Aug 19 2022 at 15:57):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Hi all,
I've been using the book Concrete Semantics
(http://www21.in.tum.de/~nipkow/Concrete-Semantics/) as a tutorial.
Currently, I'm trying to prove the following.
"⟦(WHILE b DO c,s)⇒t⟧⟹(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
In other words, I want to prove that I can unroll the loop and end up in
the same final state.
At some point in the proof, I'm in a "subtree" (also another WHILE loop)
of the original WHILE b DO c. I want to be able to apply the induction
hypothesis and get an unrolled loop for that subtree.
I looked at some examples of rule induction on the web and in the
Programming and Proving book. I tried structuring the proofs that way
and also used cases, but am still stuck.
The version of the theory that I'm sending here uses "proof -". It helps
me being explicit what I'm trying to do since I'm new to Isabelle.
I've laid out the whole proof and skipped the parts where I needed the
induction hypothesis with "sorry".
Would anybody mind taking a look, please?
The code is below. I've marked the places that I need help with "(* NEED
INDUCTION HYPOTHESIS *)".
Thank you,
Amarin
========================
Semantics.thy
========================
theory Semantics imports Main begin
type_synonym vname = string
type_synonym val = int
type_synonym state = "vname ⇒ val"
datatype aexp = N int | V vname
fun aval :: "aexp ⇒ state ⇒ val" where
"aval (N n) s = n" |
"aval (V x) s = s x"
datatype bexp = Bc bool
fun bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) s = v"
datatype
com = SKIP
| Assign vname aexp ("_ ::= _" [1000, 61] 61)
| Seq com com ("_;;/ _" [60, 61] 60)
| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
inductive
big_step :: "com × state ⇒ state ⇒ bool" (infix "⇒" 55)
where
Skip: "(SKIP,s) ⇒ s" |
Assign: "(x ::= a,s) ⇒ s(x := aval a s)" |
Seq: "⟦ (c1,s1) ⇒ s2; (c2,s2) ⇒ s3 ⟧ ⟹ (c1;;c2, s1) ⇒ s3" |
IfTrue: "⟦ bval b s; (c1,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
IfFalse: "⟦ ¬bval b s; (c2,s) ⇒ t ⟧ ⟹ (IF b THEN c1 ELSE c2, s) ⇒ t" |
WhileFalse: "⟦¬bval b s⟧ ⟹ (WHILE b DO c,s) ⇒ s" |
WhileTrue: "⟦ bval b s1; (c,s1) ⇒ s2; (WHILE b DO c,s2) ⇒ s3 ⟧
⟹ (WHILE b DO c, s1) ⇒ s3"
declare big_step.intros [intro]
lemmas big_step_induct = big_step.induct[split_format(complete)]
inductive_cases SkipE[elim!]: "(SKIP,s) ⇒ t"
inductive_cases AssignE[elim!]: "(x ::= a,s) ⇒ t"
inductive_cases SeqE[elim!]: "(c1;;c2,s1) ⇒ s3"
inductive_cases IfE[elim!]: "(IF b THEN c1 ELSE c2,s) ⇒ t"
inductive_cases WhileE[elim]: "(WHILE b DO c,s) ⇒ t"
theorem big_step_determ: "⟦ (c,s) ⇒ t; (c,s) ⇒ u ⟧ ⟹ u = t"
by (induction arbitrary: u as3 rule: big_step_induct) blast+
lemma unroll_while:
"⟦(WHILE b DO c,s)⇒t⟧⟹(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
proof -
fix b s c t
assume assms: "(WHILE b DO c,s)⇒t"
let ?thesis = "(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t"
{
assume true1: "bval b s"
obtain i where i1:"(c,s)⇒i" and i2:"(WHILE b DO c,i)⇒t" using assms
true1 by auto
{
assume true2: "bval b i"
obtain i' where i3:"(c,i)⇒i'" and i4:"(WHILE b DO c,i')⇒t" using
i2 true2 by auto
have body:"(c;;IF b THEN c ELSE SKIP,s) ⇒ i'" using i1 i3 true2
by auto
have loop:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),i') ⇒ t" using i4
sorry (* NEED INDUCTION HYPOTHESIS *)
have ?thesis using body loop true1 by auto
} moreover
{
assume false2: "¬bval b i"
have body:"(c;;IF b THEN c ELSE SKIP,s) ⇒ i" using i1 false2 by auto
have loop:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),i) ⇒ t" using i2
sorry (* NEED INDUCTION HYPOTHESIS *)
have ?thesis using body loop true1 by auto
}
ultimately have "(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒t" by metis
} moreover {
assume false1: "¬bval b s"
have final1:"(WHILE b DO c,s)⇒s" using false1 by auto
have final2:"(WHILE b DO (c;;IF b THEN c ELSE SKIP),s)⇒s" using
false1 by auto
have eq:"s=t" using assms final1 big_step_determ by auto
have ?thesis using final2 eq by auto
} ultimately show ?thesis by metis
qed
end
Email Gateway (Aug 19 2022 at 15:57):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Amarin,
That is a nice little puzzle. I had not tried it before and needed some time to
find a solution (see below). The fine structure of the proofs remains obscure
and you may want to spell it out yourself. The main point is however not that
difficult: the lemma lem did not drop out of thin air but comes directly from
looking at the subgoal in the WhileTrue case. On the techical side it is
important to write the induction in the given form because the proposition you
induct on contains other subterms than just variables.
There may be other slicker ways of proving your goal but I could not see how to
complete your original attempt.
Tobias
lemma lem:
"⟦ (WHILE b DO (c;; IF b THEN c ELSE SKIP),s2) ⇒ s3; bval b s1; (c,s1) ⇒ s2 ⟧
⟹ (WHILE b DO (c;; IF b THEN c ELSE SKIP),s1) ⇒ s3"
apply(induction "WHILE b DO (c;; IF b THEN c ELSE SKIP)" s2 s3
arbitrary: s1 rule: big_step_induct)
apply auto
done
lemma "(WHILE b DO c,s) ⇒ t ⟹ (WHILE b DO (c;; IF b THEN c ELSE SKIP),s) ⇒ t"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by blast
next
case WhileTrue thus ?case using lem by blast
qed
Email Gateway (Aug 19 2022 at 15:58):From: Amarin Phaosawasdi <phaosaw2@illinois.edu>
Dear Tobias,
This helped tremendously. I spelled the proof out and it made perfect sense.
Thank you,
Amarin
Last updated: Nov 21 2024 at 12:39 UTC