Email Gateway (Aug 18 2022 at 16:19): Email Gateway (Aug 18 2022 at 16:19):From: Makarius <makarius@sketis.net>
Just one note on the "The sad fact of life" about SML semantics.
The reference implementation http://www.mpi-sws.org/~rossberg/hamlet/ by
Andreas Rossberg can be understood as an executable version of that.
Nonetheless there are problems with it, because the static phase merely
checks that the problem is type-correct, without producing the resulting
type-assignment. As a consequence, the dynamic phase needs to be
implemented like a LISP interpreter, with explicit tags everywhere.
Makarius
Email Gateway (Aug 18 2022 at 16:31):From: Francisco Ferreira <ferrerif@iro.umontreal.ca>
Hello all,
I am just starting with Isabelle, my intention is to prove some simple
theorems of simply-typed lambda (from Pierce's TAPL book) calculus using
Nominal Isabelle.
I am using the tutorial and the isar reference as guides (and the
nominal_datatype_reference too)
I am starting nice and easy trying to do the determinism proof for a
very simple language of arithmetic expressions.
So far I have defined my datatype and the step by step semantics
relation, and I have formulated my theorem (I've attached the code as I
have it so far).
On my paper proof, I would proceed by induction on the structure of the
step relation but I don't know how to proceed in this case (apply (rule
step.induct) confuses me).
What I need is some help to start, and hopefully be able to keep the
momentum going.
How do I approach this proof? (are there any examples that I should check?)
Thanks in advance,
Francisco
arith.thy
Email Gateway (Aug 18 2022 at 16:31):From: Christian Urban <urbanc@in.tum.de>
Hi Francisco,
Below I have started your proof in the style
of Isabelle/Isar. Maybe this is of help for how
approaching this kind of proofs. However, once
I attempted the second case, I found out that
the lemma for your definition is not true. You
added a rule to Pierce's rules, which breaks the
property you are after. The counter example is
also included.
Hope this helps,
Christian
Quoting Francisco Ferreira <ferrerif@iro.umontreal.ca>:
Arith.thy
Email Gateway (Aug 18 2022 at 16:31):From: Francisco Ferreira <ferrerif@iro.umontreal.ca>
Thank you!
That was really helpful! But I am still having problems, I've checked the tutorial and the reference manual, but in the tutorial the Proof commands are not discussed, and I find the reference manual a bit too advanced, is there a tutorial on the proof command?
Regarding my example I eliminated the problematic rule, and now when I reach the proof of the Pred(Z) rule, I don't know how I prove that Z↓m' is not possible as no rule matches Z
Sorry for the continuos questions, and thanks again for your help,
Francisco
Arith2.thy
Email Gateway (Aug 18 2022 at 16:31):From: Lars Noschinski <noschinl@in.tum.de>
The "Tutorial on Isar"[1] covers the proof command.
-- Lars
[1] http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf
Email Gateway (Aug 18 2022 at 16:31):From: Lars Noschinski <noschinl@in.tum.de>
Start with proving which form the "n" in "n↓m" has (i.e.
"Succ n'" or "Pred n'"), instead of proving which form it does not have (Z).
-- Lars
Email Gateway (Aug 18 2022 at 16:32):From: Tobias Nipkow <nipkow@in.tum.de>
For beginners I would recommend some material I have just put together
for my Semantics course, where I use Isabelle:
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/
Under "Slides and files" you find a proof-pattern-oriented introduction
to Isabelle proofs. Simply stop reading when the Isabelle intro stops
and the Semantics material starts.
This is work in progress and any feedback is warmly appreciated!
Thanks
Tobias
Lars Noschinski schrieb:
Email Gateway (Aug 18 2022 at 16:32):From: Francisco Ferreira <ferrerif@iro.umontreal.ca>
Thank you all for your comments, the documents are really useful.
I really liked the slides, it seems to be a great course, I would totally enrol in such a course.
The first part with the motivation and the objectives presents the subject in an attractive, yet realistic way (with the "The Sad Facts of Life" slides). Additionally I liked the fact that the language that will be studied (IMP) is not a form lambda calculus, that is interesting
Isabelle is a powerful tool, no-one will deny it, but it is also very complex. To illustrate this, one of the demos(Isar_Demo.thy) uses the following tactic
let ?ys = "take n xs"
have "xs = ?ys @ xs!n # rev ?ys"
by (metis Suc_le_lessD length xs = Suc (n + n) add_Suc_right add_Suc_shift append_take_drop_id assms diff_add_inverse le_add1 nth_drop' rev_take)
thus ?thesis by blast
qed
That metis tactic is really scary (I hope that line is automatically generated by sledgehammer or something like that).
That said, I am sure all the complexity problems won't be such in a live course with demos and office hours. As I said, I'd enjoy the course. I am highly interested in the subject, and Isabelle seems like a great tool.
But, even with the documentation, and the fact that I am really trying to understand Isabelle, I just don't get it.
I can't even prove that "step (Pred Z) m ==> m = Z", probably I am just saturated and tired of going in circles.
Thanks,
Francisco
Arith2.thy
Email Gateway (Aug 18 2022 at 16:32):From: Tobias Nipkow <nipkow@in.tum.de>
let ?ys = "take n xs"
have "xs = ?ys @ xs!n # rev ?ys"
by (metis Suc_le_lessDlength xs = Suc (n + n)add_Suc_right add_Suc_shift append_take_drop_id assms diff_add_inverse le_add1 nth_drop' rev_take)
thus ?thesis by blast
qedThat metis tactic is really scary (I hope that line is automatically generated by sledgehammer or something like that).
Yes, it was found automatically by s/h.
That said, I am sure all the complexity problems won't be such in a live course with demos and office hours. As I said, I'd enjoy the course. I am highly interested in the subject, and Isabelle seems like a great tool.
But, even with the documentation, and the fact that I am really trying to understand Isabelle, I just don't get it.
I can't even prove that "step (Pred Z) m ==> m = Z", probably I am just saturated and tired of going in circles.
This lemma is trivial, on one level:
by(blast elim: step.cases)
My slides have carefully avoided explaining this idiom in the beginning,
because elimination rules (this is what "elim" stands for) and how to
modify blast, are advanced concepts. You find some of this under "Rule
inversion" in the IMP part of my slides. What I fail to explain there is
"step.cases". The latter is a case distinction rule: how can "step x y"
have been derived, i.e. like an induction but without the induction
hypothesis.
But my impression from your failed proof attempts is that you did not
quite realize that a case distinction on which rules derived "step (Pred
Z) m" is needed to perform the proof. Here is the structured proof that
exposes the 2 case distinctions you need:
lemma assumes "step (Pred Z) m" shows "m = Z"
using assms
proof cases
case s_pred_zero thus "m=Z" by simp
next
case (s_pred m')
from step Z m' have False
by cases --"there is no rule with conclusion step Z m"
thus "m=Z" by blast
qed
The "cases" proof method figures out which rules could have been used to
derive the incoming "step x y".
The assumes-shows-using contortion seems necessary, I could not get the
proof to work with "step (Pred Z) m ==> m = Z", except by making it an
induction instead of a case distinction, which would be misleading.
As a preview of coming attractions: The lemma can now be proved
automatically by s/h, but only with the latest link to smt solvers,
thanks to Jasmin, Sascha, Lukas and Z3!
by (smt arith.simps(5) arith.simps(2) arith.simps(4) arith.simps(8)
step.simps)
Yes, awesome!
Tobias
Thanks,
Francisco
On 2010-11-24, at 3:02 AM, Tobias Nipkow wrote:
For beginners I would recommend some material I have just put together
for my Semantics course, where I use Isabelle:
http://www4.in.tum.de/lehre/vorlesungen/semantik/WS1011/
Under "Slides and files" you find a proof-pattern-oriented introduction
to Isabelle proofs. Simply stop reading when the Isabelle intro stops
and the Semantics material starts.This is work in progress and any feedback is warmly appreciated!
Thanks
TobiasLars Noschinski schrieb:
On 24.11.2010 05:26, Francisco Ferreira wrote:
Thank you!
That was really helpful! But I am still having problems, I've checked
the tutorial and the reference manual, but in the tutorial the Proof
commands are not discussed, and I find the reference manual a bit too
advanced, is there a tutorial on the proof command?
The "Tutorial on Isar"[1] covers the proof command.-- Lars
[1] http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf
Last updated: Apr 26 2024 at 12:28 UTC