Email Gateway (Aug 18 2022 at 17:47): Email Gateway (Aug 18 2022 at 17:47):From: Dorka Tronix <dorkatronix@gmail.com>
Hi,
I'm a beginner with proof assistants. Apologies if this is the wrong mailing
list; I wasn't sure where to ask beginner questions. I'm trying to learn
Isabelle with some small examples of my own. I'm having problems with what
I thought would be a simple proof, and think I must be missing something
obvious.
I have a very simple recursive data type:
datatype "S" = Assert bool
| Assign bool
| Ite bool "S list" "S list" (* if then else statement *)
and a simple function:
fun "fse" :: "S list \<Rightarrow> bool \<Rightarrow> bool" where
"fse [] b = b" |
"fse (x#xs) b = (case x of
(Assert e) \<Rightarrow> fse xs (b \<and> e )
| (Assign e) \<Rightarrow> fse xs (b \<and> e)
| (Ite e s1 s2) \<Rightarrow> (fse xs (fse (s1) (b \<and> e)))
\<or> (fse xs (fse (s2) (b \<and> (\<not> e)))))"
This function should be doing something like forward symbolic execution of a
program. I'd like to prove the law of excluded miracle:
lemma law_of_excluded_miracle [simp] : "\<forall> s. \<not> (fse s False)"
My handwritten proof is via induction on the structure of an S list. The
empty list, Assert e, and Assign e cases are trivial. In my handwritten
proof I'm also applying the IH to ITE. Ite is causing the problem in
Isabelle. This case is recursively calling fse on the first branch s1 to
get a predicate, and then processing the rest of the list. Similar with the
second branch.
I can't seem to get past the ITE case. At first I thought I just needed a
size function so that isabelle knew that the list sizes were decreasing so
the IH would apply. That didn't work.
My ultimate goal is to prove:
lemma swap : "\<forall> s. \<forall> p. \<forall> q. (fse s p) \<and> q =
(fse s q) \<and> p"
This fails as well (I'm hoping that the law_of_excluded_miracle proof will
give insight into the swap proof).
I've attached the .thy file. Any help would be appreciated....I've spent
several days on both.
thanks!
simple-fse-lst-question.thy
Email Gateway (Aug 18 2022 at 17:47):From: Simon Winwood <sjw@cse.unsw.edu.au>
Hi, it looks like you are using the wrong induction rule for your
proof --- you are using List.induct, rather than fse.induct. I had a go
at the proof, attached, and found it a bit annoying. Given a slightly
more compact version of fse (my fse2) it goes away by induct, auto.
Simon
Test.thy
Last updated: Nov 21 2024 at 12:39 UTC