What’s an untutorial? A tutorial is written by an expert, to guide a beginner. An un-tutorial, on the other hand, is written by a beginner, in this case, me.
My aim is to use Isabelle to formalize some basic definitions and results from computability theory, say, about partial functions computed by goto programs, while programs, and mu recursion, decidable and enumerable sets, many-one reductions, etc.
I know this stuff (currently I even teach it) and I also have already “formalized” part of it, in the sense that I have Haskell code for the abstract syntax of these languages, and their interpreters, and these actually work, as part of an E-Learning/E-Assessment system that I have been developing for a long time.
All of this is, of course, just code, without any proofs. I do feel confident writing specifications, on paper, also as (smallcheck/quickcheck) executable test cases, and also as lemmas in Isabelle, but I want to learn how to prove things formally, which I have never done.
The stuff is comparable to Sections 7/8 (small step semantics, compiler) from Nipkow and Klein: Concrete Semantics, so I am pretty confident that it should be doable - because it’s already been done. The challenge is just for me to understand how.
This may be interesting for other Isabelle beginners (with similar background) as they may recognize their experience or mistakes. The point is that while writing this, it’s not clear that something a beginner tries, is a mistake, or why. That is why I not plan to re-edit this text “with hindisght”.
It may also be interesting for the experts, as it shows stumbling blocks for beginners that experts may have long forgotten.
In the following text, I include some rants on what appear to be rather harmless (user interface) design errors, and I hope that readers are more amused than Isabelle authors are offendended. Let’s try this at once in the next section:
I am using Isabelle2014 on a x86_64 machine with Fedora 21, running XMonad/Mate.
The recommended way of installing Isabelle is to unpack an archive file (Isabelle2014_linux.tar.gz) that is huge (328 MB). It is huge because it contains a (among others) complete JVM, which seems to be needed for the IDE, which seems to be mandatory (support for Proof General/Emacs was apparently dropped). Taking a closer look, we see that we get JDK twice (once for x86, once for x86_64), and more stuff. Looking at the ten largest sub-sub-dirs:
du -sb */* | sort -n | tail -n 10
5570342 contrib/e-1.8
14774964 contrib/z3-3.2-1
15259406 contrib/cvc3-2.4.1
16711851 src/Tools
27846882 contrib/z3-4.3.2pre-1
28733429 src/HOL
29997213 contrib/scala-2.11.2
45356169 contrib/polyml-5.5.2-1
229288283 heaps/polyml-5.5.2_x86-linux
514751472 contrib/jdk
That’s binaries for software that I already have on my system (in this case, jdk, scala, z3) or could easily install via the package manager (yum install polyml).
Maybe traditional practices for modular design and packaging appear obsolete because disk space appears cheap - but here I get plain 0.7 GB of just duplicates.
It’s a good thing they did not include their own Linux kernel as well with the package, just to be on the safe side.
Instructions say I can install whereever I want, but also that the installation directory needs to be writable on first start, “to build the required logic image”. Well, there was no problem including lots and lots of MB into the download, but this “image” did not fit? My problem is this: my instinct is to install software at something like /usr/local/share and make it owned by root, so I cannot ever accidentally destroy it during normal work days (when I’m not root). I am not sure whether I could just start Isabelle as root for the first time (to build the image) - and work non-root later.
The web site links to plenty of tutorial and reference documents - all are in pdf format. I would have preferred HMTL because this is much easier to navigate, to resize when viewing, to copy code from, and to bookmark.
Well. Just going by the name, I start by opening the “tutorial”, which is actually a 223 page document - I thought the name usually suggests a quick introduction.
The tutorial starts with a strange remark (second sentence of preface) “This tutorial is written for potential users rather than for our colleagues in the research world”. What? Are your colleagues distinguished by not being users of Isabelle?
Well. Since I plan to use partial functions and relations, I am looking up “relations” (Section 6.3). OK, the mathematics of this looks familiar. I still do not know about modules (what I need to import, for using these theorems) and namespaces (everything looks so global).
The tutorial show some theorems, which is fine, but I also want to look at their proofs, amd concepts that are referenced (e.g., natural numbers, the’re some Suc in there). All of this
could have been hyperlinked easily - if the whole thing was HTML instead of PDF.
(I am used to this from Haskell land: I can read a package’s types and documentation on hackage - but also “view source” directly from there.)
There are some actual proofs in this tutorial (e.g., in 6.3.3.) but they are using “apply style”, which I have heard is old-fashioned - I specifically want to learn the structured “Isar style” of presentation, which is, as I understand, the main unique feature of Isabelle.
But even in “Concrete Semantics”, Isar style is presented only from Chapter 5 onwards. Why do Chapters 1 - 4 present a style that is, in the authors’ words, “unreadable and hard to maintain”?
Now, I start up Isabelle, and I actually get a graphical editor “jedit”, with some predefined window panes and panels. I would have much preferred to work with the editor I know (emacs). I am somewhat relieved because it is actually possible to give a (theory) file name as command line argument when starting the IDE.
When Isabelle starts, it first presents a “splash screen”. Come on, do we really need this? At least make it look good, because at present, it does not - the perspective is not right, e.g., the “forall” sign is off axis, also the equals sign looks wrong. On the positive side, it is at least consistently wrong - look at the title pages of both the “old” and the “new” (Concrete Semantics) Isabelle book.
Starting a fresh theory, I know from the tutorial that the structure is “theory T; imports B1 B2 … ; begin … end” but the IDE shows a blank buffer, and strange error messages while typing. Since you want to go (down) the IDE path - Eclipse is your yardstick - they have templates for almost everything, and especially for making a class.
I am using the XMonad window manager, so I already know the following problem: it seems that Java bindings (or re-implementations) of windowing toolkits do not respect some aspects of protocol, so they are not working correctly with non-parenting managers (as XMonad). This shows, e.g., in the mouse position being off by a few centimeters on drop-down lists. There is a known work-around: execute “wmname LG3D” before starting the application.
I am still worried about namespaces, because I expect to be able to use hierarchical names. I will have several concepts of Programs, and I plan to put them into different modules (theories), say, Computability.Goto, Computability.While, Computatiblity.Recursive. The tutorial says (p. 14) “A theory is a named collection of types, .. much like a module in a programming language.” Fine. But languages I use have hierarchical modules. Because -
I plan to use some my theories at the same time, because I want to prove equivalences (that is, write compilers). In Haskell I would
import qualified Computability.Goto as G
import qualified Computability.While as W
compile :: G.Program -> W.ProgramI don’t see any mention of this in the tutorial. The concept “namespace” does not appear in the index. I found only accidentally that the tutorial has an index at all - it’s not visible in the list of contents.
So I fear I have to encode module information in names of identifiers (Goto_Program instead of Goto.Program). This is not helped by examples like “import Main List Relation Transitive_Closure” - this suggests that the namespace is flat and global.
I understand inductive definitions because to me, they look “just like Haskell”.
datatype Command = Inc nat | Dec nat | Stop | Goto nat | GotoZ nat natWell, actually it’s not exactly Haskell: while data constructors have their argument types trailing (GotoZ nat nat), type constructors have their arguments leading (Command is the argument for list).
type_synonym Program = "Command list"That is, of course, just a syntactic inconsistency.
Another aspect of the syntax that I don’t get is why and where I need to put double quotes. I hear it’s about “inner syntax” and “outer syntax” - but why would a beginner need to care? I know of no other (modern, programming) language that needs this.
The most striking argument against this is given by the Nipkow and Klein: they admit this excessive double quoting is a nuisance, in introduction to part 2 of “Concrete Semantics” (p.74): “We simplify Isabelle syntax in two aspects to improve readability: 1. we no longer enclose types and terms in quotation marks 2. we no longer separate clauses … with |”.
I hear you. But if you think it’s good for readers (and, I assume, writers) of books - then please be consistent and also allow this convenience for those that actually write code. You do want code to be written in the most readable way, do you?
An argument in favour of language-aware IDEs is that they help you with your typing. They show errors (after you typed something) and the help to prevent errors (by suggesting completions that are reasonable).
I am not sure how auto-completion is supposed to work, and what it is supposed to know. For instance, I have a lemma where I use “rtrancl”, which has the wrong type, and “rtranclp” would be right, but I only know this from looking at the source in a separate shell window.
Within the Isabelle editor window, I see no way of getting the declaration of “rtrancl” (I’d expect to see that by hovering over the identifier, as Eclipse does it for Java code), and no way of getting a list of identifiers that start the same. (Here, textual completion is just the weakest model that comes to mind, Eclipse does much more for Java code because its completion is type-aware.)
I perfectly understand notation for Peano numerals, and for lists, and statements and proofs of their more obvious properties. (Append is associative, Addition is commutative etc.)
I do not understand (at first sight) how can there be a function
nth :: 'a list => nat => 'abecause, what would be the value of “nth [1,2,3] 5”?
I know partial functions exist in Haskell (starting with head and tail), but it’s common advice not to use them (because when they are applied to an empty list, the runtime error message is basically useless).
Then my naive thinking is, Isabelle should be much more safe than Haskell - so how come they have “nth” like this?
Let us type in the Isabelle editor window (first line)
value "nth [1,2,3] 5 :: nat"
"[] ! Suc 0" :: "nat"so we see (output in the second line) that we do not get an exception (as I feared) but instead an expression (a term) of type “nat” that is not a constructor term, but cannot be reduced further. Presumably this means that I cannot prove anything about it (its top constructor is neither Suc nor 0).
While we’re at it:
value "0 * (nth [1,2,3] 5) :: nat"
"0" :: "nat"A-ha! So multiplication does not fully evaluate the second argument. This is understandable, assuming the standard recursive definition.
primrec times_nat where
mult_0: "0 * n = (0\<Colon>nat)"
| mult_Suc: "Suc m * n = n + (m * n)"(Which I’d like to be able to find, from the IDE, where I just typed "*". But I looked it up in HOL/Nat.thy) Indeed,
value "(nth [0,1,2] 4) * 0 :: nat"
"[] ! Suc 0 * 0" :: "nat"But multiplication is commutative, right? There is a lemma
lemma mult_0_right [simp]: "(m::nat) * 0 = 0"Does the example violate the lemma? No, I assume that “(m :: nat)” implies that we really have a value (a constructor term, and not just any term).
Actually I first made a typo in the above examples and wrote “int” for “nat”, and this gives a nice puzzle, for which I have no solution at the moment: why do both of these expressions
value "(nth [0,1,2] 4) * 0 :: int"
value "0 * (nth [0,1,2] 4) :: int"evaluate to “0 :: int”?
Both HOL/Nat.thy and HOL/Int.thy have multiplication in instantiations
instantiation nat :: comm_semiring_1_cancel
instantiation int :: comm_ring_1and perhaps there’s different rewrite rules hidden there.
Here’s another funny equality: this gives True:
value "(hd []) = (hd (tl [] :: nat list))"Well, in Haskell, you’d get bottoms (exceptions) on both sides, so it’s fine, but we just learned that there’s no such thing in Isabelle, just “stuck terms”, and they should be different.
But - and that’s the thing that’s really surprising here: the function “tl” is not what you (Haskell programmer) think, because
value "tl []"is actually (defined to be, by an extra clause in HOL/List.thy) “[]”. Why on earth?
And while I was typing the previous section, I wanted to copy the output from the “output” window pane, and sure enough, I notice another jedit quirk: it does not seem to respect the X Window mouse protocol, where you can select text by left-mousing over it - here I have to Ctrl-C also.
This is different from the “output” window to the main edit panel, where mouse-over selection seems to work.
Oh, and another nuisance is that I have to click into the editor window before it will accept my continued typing.
I was complaining about being forced away from my editor earlier, and such unexpected and inconsistent behaviour ist just one of the reasons.
Now for some actual modelling: I want to define the partial function computed by some Goto program. The computation is deterministic. This cannot work:
computes :: "Program => nat list => nat"because maybe we do not get a result. This also cannot work:
computes :: "Program => nat list => nat option"because we cannot know for sure whether we obtain a result. So this has to be modelled as a relation. In HOL/Relation.thy, relations are sets of pairs
computes :: "Program => (nat list \times nat) set"or, we can write the relation as a predicate
computes :: "Program => nat list => nat => bool"I will settle for that.
Note that the single step transition relation is computable, and its sharpest type would be
step :: Command => Config => Config optionFor consistency with the above, I will write this as a predicate. There are still several choices for the implemenation, I use
inductive step :: "Program ⇒ Config ⇒ Config ⇒ bool"
where "step p c1 (stepC (nth p (fst c1)) c1)"because that’s what’s in the book. Apparently it could also have been fun, definition, or abbreviation, and some of them with simp.
Anyway, writing this as a predicate, the type no longer has the information that “step” (and also “computes”) are partial functions.
So we have to (define and) prove this. I try
definition singlevalued :: " ( 'a ⇒ 'b ⇒ bool) ⇒ bool "
where "singlevalued r = ( ∀ x y z . (r x y ⟶ r x z ⟶ y = z )) "
lemma sv_step : "singlevalued (step p)"I have no idea how to prove this, but I apply sledgehammer, and indeed it produces, immediately
by (metis singlevalued_def step.cases)It’s nice that the machine can do this, but it would be much nicer if I could learn from this, that is, I want to see the (Isar-style) proof that I could have written instead.
Then, I think maybe I should use something from a library. I am grepping for “single_valued” through HOL/*.thy, and I find “single_valuedP” in HOL/Relation.thy. So, I replace my “singlevalued” definition by the official one, only to find that sledgehammer now cannot prove “single_valuedP (step p)”.