CentraleSupélec LMF, UMR CNRS 9021
Département informatique Laboratoire Méthodes Formelles
Bât Breguet, 3 rue Joliot-Curie Bât 650 Ada Lovelace, Université Paris Sud
91190 Gif-sur-Yvette, France Rue Noetzlin, 91190 Gif-sur-Yvette, France
Tutoriel : types de données, fonctions et preuves en Isabelle

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.

fun snoc:: "'a list ⇒ 'a ⇒ 'a list"
where
    "snoc [] x = (*result*)"
  | "snoc (y # l) x = (*result*)"

fun rev_snoc:: "'a list ⇒ 'a list"
where
    "rev_snoc [] = (*result*)"
  | "rev_snoc (x # l) = (*result*)"

(* A useful lemma for proving rev_snoc = rev *)
lemma snoc_app_nil: "snoc l x = l @ (x # [])"
proof (induction l)
  case Nil show ?case sorry (* sorry avoids the proof, replace it by a real proof *)
next
  case (Cons y ll)
     thus ?case sorry
qed

theorem "rev_snoc l = rev l"
sorry

Vous pouvez utiliser la commande sledgehammer à la place d'une preuve. Cette commande utilise des solveurs externes pour essayer de trouver une preuve. En cas de succès, il ne reste qu'à remplacer l'appel à sledgehammer par la preuve qu'il a trouvée (il suffit pour cela de cliquer sur le texte de la preuve dans la console). Dans l'exemple ci-dessus, vous pouvez donc commencer par remplacer sorry par sledgehammer pour trouver les preuves.

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.

(* Inverting a list by accumulation *)
fun rev_acc:: "'a list ⇒ 'a list ⇒ 'a list"
where
    "rev_acc [] r = (*result*)"
  | "rev_acc (x # l) r = (*result*)" 

value "rev_acc l4 []"

(* A stronger induction hypothesis for proving the next theorem *)
lemma rev_acc_inv: "rev_acc l r = (rev l) @ r"
proof (induction l arbitrary: r)
  (* "arbitrary: r" makes r a free variable, which is necessary to use the IH with x # r *)
  case Nil show ?case sorry
next
  case (Cons x ll) thus ?case sorry
qed

(* Show that rev_acc does the same thing as rev *)
theorem rev_acc_is_rev: "rev_acc l [] = rev l"
proof (induction l)
  case Nil show ?case sorry
next
  case (Cons x ll) thus ?case sorry
qed

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