Ce tutoriel présente les fonctionnalités de base que nous utiliserons pour définir la sémantique du langage Niklaus :
- définition de types de données
- définition de fonctions
- preuves par application de règles (apply) ou structurées (bloc proof/qed en Isar)
D'autres constructions seront présentées lorsqu'elles seront nécessaires.
Note : vous pouvez copier-coller le listing ci-dessous dans un fichier TutoList.thy pour l'utiliser dans Isabelle.
Installation d'Isabelle
Pour installer isabelle sur votre ordinateur, consultez https://isabelle.in.tum.de/
Exercice
Après avoir fait ce tutoriel, définissez une fonction snoc l x qui ajoute x à la fin de l, ainsi qu'une fonction rev_snoc l qui utilise snoc pour inverser l. Prouvez que rev_snoc l = rev l.
Un exercice plus difficile
Définissez une fonction rev_acc qui inverse une liste par accumulation dans un second argument, et prouvez que rev_acc l [] = rev l. Dans cette démonstration, l'hypothèse de récurrence est trop faible car elle ne traite que le cas ou le second argument de rev_acc est la liste vide. Il faut donc établir un lemme plus général qui permettra de faire le raisonnement par induction. De plus, pour démontrer ce lemme par induction, nous aurons besoin de l'utiliser avec une autre valeur du second argument de rev_acc, il faut donc indiquer que cet argument est une variable libre grâce à arbitrary: r si l'argument est r.
Code du tutoriel
À enregistrer dans un fichier de nom TutoList.thy.
theory TutoList
imports Main
begin
section ‹Technical stuff to make the tutorial easier›
text ‹
Definition of a data type "list of 'a", where 'a' is any type.
We hide the list type of HOL/Main as well as the associated notations
to avoid conflicts with our definition.
›
no_notation
Nil ("[]")
and Cons (infixr "#" 65)
and append (infixr "@" 65)
hide_type list
hide_const rev
section ‹Definition of a data type›
text ‹
We define a data type named list, which take a type 'a as parameter.
This data type has two constructors:
▪ Nil, a constant which corresponds to the empty list, and is also noted []
▪ Cons, which adds an item (of type 'a) in front of the list, and is also noted #
Such a type is an inductive data type because it is defined by induction on
its constants and constructors.
›
datatype 'a list =
Nil ("[]") (* notation for the empty list *)
| Cons 'a "'a list" (infixr "#" 65) (* infix right associative notation with priority 65 ( = is 50) *)
text ‹
Exemples of useful commands to find theorems and print known facts.
To see the result of a command, put the cursor just after the command,
and look in the "Output" panel. You may have to clock on the "Output" button below to make the panel appear.
Here, we see that "datatype" has generated a lot of theorems about the new type.
Among them are "list.induct" which allows us to make proofs by structural
induction on lists, and "list.simps" which gives the simplification rules
for list terms.
›
find_theorems name:"TutoList.list"
thm TutoList.list.induct
text ‹ Note that A ⟹ B ⟹ C ≡ (A and B) ⟹ C, also written ⟦A; B⟧ ⟹ C ›
text ‹Same theorem in a more readable form ›
print_statement TutoList.list.induct
text ‹
The list.induct theorem has been generated automatically from the
inductive definition of the "list" type.
It states that for any predicate P, if P holds for the empty list,
and if for any item x1 and any list x2, when P holds for x2,
it also holds for x1#x2, then P holds for any list.
›
text ‹Theorems that may be used by the simplifier›
thm TutoList.list.simps
section ‹About Curryfication›
text ‹
Curryfication is named after Haskell Curry.
In Isabelle, functions are in curryfied form:
f: A × B → C
(x, y) ↦ z
is written as:
f: A → (B → C)
x ↦ (λy. z)
so "f x" is a function which takes the second argument of f to provide the result,
and "f x y" is read as "(f x) y"
›
text ‹Define sum as the function which returns the sum of two integers›
definition sum:: "int ⇒ int ⇒ int"
where "sum m n = m + n"
text ‹Check that it works as expected›
value "sum 2 3"
text ‹We can partially apply sum to one argument to define the increment function›
abbreviation "inc ≡ sum 1"
value "inc 41"
section ‹Defining functions›
text ‹
To define a function on an inductive data type, it is sufficient
to define it for each of the constructors.
For a list, we have to define the function for the empty list and
for the list obtained by Cons from another list.
›
text ‹
Append a list to the end of another list (concatenation).
append(l1, l2) is written append l1 l2 (Curryfication).
Thanks to the infix notation, it can also be written l1@l2
›
fun append:: "'a list ⇒ 'a list ⇒ 'a list" (infixr "@" 65)
where
"[] @ l2 = l2"
| "(x # l1) @ l2 = x # (l1 @ l2)"
value "(a # b # c # []) @ (d # e # [])"
text ‹
You can see here that since a, b, c, d, and e are free variables, their type
is not known and is represented by the 'a type variable.
The list is therefore an 'a list.
Below, we set the type of the items to nat, so the list become a nat list.
Note that it is only necessary to set the type of one item because
all items in a list are of the same type. Here, we have to choose a type
for 1 because in Isabelle/HOL, 1 may be of any numeral type.
›
value "((1::nat) # 2 # 3 # []) @ (4 # 5 # [])"
text ‹Reverse a list›
fun rev:: "'a list ⇒ 'a list"
where
"rev [] = []"
| "rev (x # l) = (rev l) @ (x # [])"
text ‹"value" prints the value of a term.›
value "rev (a # b # c # [])"
text ‹
Defining a function automatically generates and proves theorems
that will be used by the simplifier.
›
thm rev.simps(1)
thm rev.simps(2)
text ‹Standard ML code is generated automatically from the definitions.›
ML ‹
val frev = @{code rev}; (* the ML function for rev *)
val fcons = @{code "Cons"};(* the ML function for Cons *)
val vnil = @{code "Nil"}; (* the ML value for Nil *)
(* Let's build a list *)
val l = fcons(1, fcons(2, fcons(3, fcons(4, vnil))));
(* and reverse it. *)
frev l;
›
section ‹Prooving facts›
text ‹
A lemma stating that appending the empty list to a list does nothing.
This lemma is proved automatically by induction on the list and then applying the
simplifier several times. 'simp' applies the simplifier, '+' means as many times
as necessary to prove all goals.
The "[simp]" modifier after the name of the lemma says that this lemma can be added
to the list of facts used by the simp method to simplify terms.
One should be careful when annotating lemmas with [simp]: the lemma
should really simplify a term, else the simplifier may enter infinite loops!
∗‹Check the "Proof state" box in the Output panel to see the different steps in the proof of a fact.›
›
lemma append_nil[simp]: "l @ [] = l"
by (induction l, simp+)
text ‹A structured proof of the same lemma›
text ‹
Structured proofs are enclosed between "proof" and "qed".
"proof" can be followed by a method to rewrite the goal. Here, we
use induction on l. If you do not give a method, Isabelle will
try to find a suitable one. If you want to work on the raw fact,
simply put "-" (minus) after "proof". The goal to prove is defined
as the ⬚‹?thesis› variable. The proof must end with ⬚‹show ?thesis by method›
(⬚‹thus› is a shortcut for ⬚‹from this show›).
Induction on l uses the @{thm list.induct} theorem to split the goal
in two cases. We can display these cases using the ⬚‹print_cases›
command. We have cases Nil and Cons. Writing ⬚‹case Nil› puts
us in the context of the Nil case, where the subgoal to prove
is defined as the ⬚‹?case› variable. You must write ⬚‹next› to close
a case before going to the next one.
Several patterns can be used in such proofs:
▪ ⬚‹from <fact1> have <fact2> by <method>›
This derives <fact2> from <fact1> using <method>. Method "simp"
uses facts marked as [simp] to rewrite <fact1>. Method "auto"
uses simp and tries to solve all pending goals. Instead of
⬚‹by <method>›, you can use "." when <fact1> and <fact2> are identical.
▪ ⬚‹have <fact2> using <fact1> by <method>›
This is identical to ⬚‹from <fact1> have <fact2> by <method>›
▪ The last result is known as "this". When you want to derive
a fact from this, you can write ⬚‹hence <fact2>› instead of
⬚‹from this have <fact2>›. You can also write ⬚‹with <fact1> have <fact2>›
instead of ⬚‹from <fact1> and this have <fact2>›.
▪ proving a fact by transitivity:
⬚‹have "x1 = x2" by <method>
also have "... = x3" by <method>
{* more steps here *}
also have "... = xn" by <method>
finally have "x1 = xn" by <method>›
▪ accumulating facts:
⬚‹have <fact1> by <method>
moreover have <fact2> by <method>
{* more steps here *}
moreover have <factn> by <method>
ultimately have <conclusion> by <method>›
You can use the "print_facts" command to display the known facts.
›
lemma "l @ [] = l"
proof (induction l) print_cases
case Nil thus ?case using append.simps(1) .
next
case (Cons x l) print_facts thm append.simps(2)
(* [of v1 v2 ... vn] substitutes terms v1 ... vn to the n first variables of a fact *)
from append.simps(2)[of "x" "l" "[]"] have "(x # l) @ [] = x # (l @ [])" .
also with Cons.IH have "... = (x # l)" by simp
finally show ?case .
qed
text ‹Associativity of append›
text ‹
Here, we illustrate another style of proof, where proof methods
are applied until all goals have been discharged.
The proof is closed by the "done" keyword.
›
lemma append_assoc: "(l1 @ l2) @ l3 = l1 @ (l2 @ l3)"
apply (induction l1)
(* The initial goal has been split into two goals: the base case and the inductive case *)
apply simp (* Here, simp gets rid of the base case *)
apply simp (* and the last goal is solved again by simp *)
done
text ‹This can be written is a more compact way. "simp+" means "apply simp as much as you can".›
lemma "(l1 @ l2) @ l3 = l1 @ (l2 @ l3)"
by (induction l1, simp+)
text ‹Structured proof of the same lemma›
lemma "(l1 @ l2) @ l3 = l1 @ (l2 @ l3)"
proof (induction l1) print_cases
case Nil
from append.simps(1) have "([] @ l2) = l2" .
hence "([] @ l2) @ l3 = l2 @ l3" by simp
(* [symmetric] applies symmetry to an equality *)
also from append.simps(1)[symmetric] have "... = [] @ l2 @ l3" .
finally show ?case .
next
case (Cons x l) print_facts
from append.simps(2) have "((x # l) @ l2) @ l3 = x # (l @ l2) @ l3" by simp
also from Cons.IH have "... = x # l @ (l2 @ l3)" by simp
finally show ?case by simp
qed
text ‹Lemma about reversing the concatenation of two lists›
lemma rev_append: "rev (l1 @ l2) = (rev l2) @ (rev l1)"
apply (induct l1)
apply simp
apply auto (* Here, auto simplifies the goal but does not solve it. *)
thm append_assoc (* This theorem about the associativity of '@' will solve the goal. *)
apply (rule append_assoc)
done
text ‹
Compact form, where ⬚‹auto simp add <rule>› means "apply auto,
adding <rule> to the rules the simplifier can use.
›
lemma "rev (l1 @ l2) = (rev l2) @ (rev l1)"
by (induction l1, auto simp add:append_assoc)
text ‹Detailed structured proof of the same lemma›
lemma "rev (l1 @ l2) = (rev l2) @ (rev l1)"
proof (induction l1) print_cases
case Nil
from append.simps(1)[of l2] have "rev ([] @ l2) = rev l2" by simp
also from append_nil[of "(rev l2)", symmetric] have "... = (rev l2) @ []" by simp
also from rev.simps(1) have "... = (rev l2) @ (rev [])" by simp
finally show ?case .
next
case (Cons x l) print_facts
from append.simps(2)[of x l l2] have "(x # l) @ l2 = x # (l @ l2)" .
hence "rev ((x # l) @ l2) = rev (x # (l @ l2))" by simp
also from rev.simps(2)[of x "l @ l2"] have "... = rev (l @ l2) @ x # []" .
also from Cons.IH have "... = (rev l2 @ rev l) @ x # []" by simp
also from append_assoc[of "rev l2" "rev l" "x # []"] have "... = rev l2 @ rev l @ x # []" .
also from rev.simps(2)[of x "[]", symmetric] and rev.simps(1) have "... = rev l2 @ rev (x # l)" by simp
finally show ?case .
qed
text ‹
Proof that rev is the inverse of itself, using the previous lemmas
Theorems and lemma are the same from the point of view of Isabelle.
Lemmas are just theorems of less importance to us.
›
theorem rev_rev: "rev (rev l) = l"
apply (induct l)
apply simp
apply (auto simp add: append_assoc rev_append)
done
text ‹Structured proof of the same theorem›
theorem "rev (rev l) = l"
proof (induction l) print_cases
case Nil (* show ?case by simp *)
from rev.simps(1) have "rev Nil = Nil" .
hence "rev (rev Nil) = Nil" by simp
thus ?case .
next
case (Cons x l) print_facts
have "rev (rev (x # l)) = rev ((rev l) @ (x # []))" by simp
also have "... = rev (x # []) @ rev (rev l)" using rev_append .
also from Cons.IH have "... = rev (x # []) @ l" using rev_rev by simp
also have "... = (rev [] @ (x # [])) @ l" by simp
also have "... = rev [] @ ((x # []) @ l)" using append_assoc by simp
also have "... = [] @ (x # []) @ l" by simp
also have "... = (x # []) @ l" by simp
also have "... = x # ([] @ l)" by simp
also have "... = x # l" by simp
finally show ?case .
qed
text ‹Length of a list›
fun len:: "'a list ⇒ nat"
where
"len [] = 0"
| "len (x # l) = Suc (len l)"
text ‹Show that the length of the concatenation of two lists is the sum of their lengths›
theorem append_len: "len (l1 @ l2) = (len l1) + (len l2)"
by (induction l1, simp+)
text ‹Structured proof, not very detailed›
theorem "len (l1 @ l2) = (len l1) + (len l2)"
proof (induction l1) print_cases
case Nil show ?case by simp
next
case Cons thus ?case by simp
qed
text ‹The usual "map" operation, which applies a function to the elements of a list›
fun map:: "('a ⇒ 'a) ⇒ 'a list ⇒ 'a list"
where
"map f [] = []"
| "map f (x # l) = (f x) # (map f l)"
text ‹"abbreviation" defines another name for a term›
abbreviation l4 :: "int list"
where "l4 ≡ 1 # 2 # 3 # 4 # []"
text ‹
Build the list of the squares of l4.
λx. x*x is the function which takes an argument and returns its square.
›
value "map (λx. x*x) l4"
text ‹Same thing with a function defined explicitly›
definition square:: "int ⇒ int"
where "square n = n * n"
value "map square l4"
end