LRI
Équipe MODHEL
Bât 650 Ada Lovelace, Université Paris Sud
Rue Noetzlin, 91190 Gif-sur-Yvette, France
Isabelle club meeting on May 11 2016

Personnes présentes

  • Chantal Keller
  • Safouan Taha
  • Benoit Valiron
  • Hai Nguyen Van
  • Lina Ye
  • Burkhart Wolff

Classes de types dans Isabelle

Benoit Valiron

theory Scratch
imports Main
begin

class enum = 
  fixes enc :: "'a ⇒ nat"
  and   dec :: "nat ⇒ 'a" 

class A  =
  fixes f :: "'a ⇒ 'a" 

(* version 1 *)

(* On peut maintenant faire une fonction nat ⇒ nat qui cache le 'a... *)

definition h1 :: "nat ⇒ nat" where
  "h1 x = (enc (f (dec x)))"

term "h1"
(** Produit
"h1"
  :: "'a itself ⇒ nat ⇒ nat"
*)

(* un nouveau type 'a est apparu: il n'apparait pas dans le type de h1 mais est necessaire 
   dans le typage de la definition. Le constructeur de type "itself" est predefini dans Pure
   et donne acces a un SOME restreint aux types "'a itself", sans avoir besoin de HOL:
   le constructeur TYPE(_) qui prend en entree un type
*)

term "TYPE(nat)"
(* :: nat itself *)
term "TYPE('a)"
(* :: "'a itself" *)
term "TYPE('a itself)"
(* :: 'a itself itself *)

(* Isabelle rajoute ce type manquant a la definition, et met un warning pour nous avertir *)



(* version 2, avec type explicite *) 

(* Si Isabelle nous aide en ajoutant pour nous le type manquant, on peut le mettre a la
   main comme suit (et le warning disparait) *)

definition h2 :: "('a::{A,enum}) itself ⇒ nat ⇒ nat" where
  "h2 y x = (enc ((f::'a ⇒ 'a) (dec x)))"

term "h2 TYPE('a::{A,enum})"
(** 
"h2 TYPE('a)"
  :: "nat ⇒ nat"
*)


(* version 3, sans itself... *)

(* Si on a accces a HOL, on peut se debarasser de itself, car SOME est present pour tous les 
   types (avec par exemple undefined) *)

definition h3 :: "('a::{A,enum}) ⇒ nat ⇒ nat" where
  "h3 y x = (enc ((f::'a ⇒ 'a) (dec x)))"

(** pour l'utiliser, on peut utiliser undefined, qui est 
    essentiellement SOME, mais uniquement disponible dans HOL *)

term "h3 (undefined::('a::{A,enum}))"

(* undefined se comporte comme cette definition *)

definition myUndefined :: "'a" where  
  "myUndefined ≡ SOME (x::'a).True"

end

Monads in Isabelle

Burkhart Wolff

Burkhart Wolff presented a theory of monads within Isabelle/HOL. This theory is used to model sequential calculus and enables Hoare-like reasoning. Burkhart presented one particular usage of this theory that is generating test cases for sequential code.

In general, a monad is a structure with a return and a bind satisfying the three following laws:

locale Monad =
fixes   returm :: "'a ⇒ 'am"  
  and   bind   :: "'am ⇒ ('a ⇒ 'am) ⇒ 'am" (infixr ">>=" 70)
assumes left_unit : "(returm x) >>= f = f x"
    and right_unit: "m >>= returm = m"
    and assoc     : "(m >>= f) >>= g = m >>= (λ x . f x >>= g)" 

A monad to model sequential instructions is state-based. Its "bind" is the sequence operator (commonly ";"). This monads theory gives simple definitions to the "assign" and the "if then else" instructions. It also supplies two instructions "assume" and "assert" to model Hoare-like contracts.

type_synonym ('o, 'σ) MON⇩S⇩E = "'σ ⇀ ('o × 'σ)" (* 'σ is the state type and 'o the output type*)       

definition assert_SE :: "('σ ⇒ bool) ⇒ (bool, 'σ)MON⇩S⇩E"
where     "assert_SE P = (λσ. if P σ then Some(True,σ) else None)"

definition assume_SE :: "('σ ⇒ bool) ⇒ (unit, 'σ)MON⇩S⇩E"
where     "assume_SE P = (λσ. if ∃σ . P σ then Some((), SOME σ . P σ) else None)"

definition assign :: "('σ ⇒ 'σ) ⇒ (unit,'σ)MON⇩S⇩E"
where     "assign f = (λσ. Some((), f σ))"

definition if_SE :: "['σ ⇒ bool, ('α, 'σ)MON⇩S⇩E, ('α, 'σ)MON⇩S⇩E] ⇒ ('α, 'σ)MON⇩S⇩E"
where     "if_SE c E F = (λσ. if c σ then E σ else F σ)" 

The remaining "while" instruction is harder to handle. Burkhart used the "Least fixed point" construct over sets that he adapted to monads using two features : Rel2Mon and Mon2Rel.

definition Γ :: "['σ ⇒ bool,('σ × 'σ) set] ⇒ (('σ × 'σ) set ⇒ ('σ × 'σ) set)" 
where     "Γ b cd = (λcw. {(s,t). if b s then (s, t) ∈ cd O cw else s = t})"

definition while_SE :: "['σ ⇒ bool, (unit, 'σ)MON⇩S⇩E] ⇒ (unit, 'σ)MON⇩S⇩E"
where     "while_SE c B ≡ (Rel2Mon(lfp(Γ c (Mon2Rel B))))"

As corollary, we obtain the "unfold" property of the while:

theorem while_SE_unfold:
"(while⇩S⇩E b do c od) = (if⇩S⇩E b then (c ;- (while⇩S⇩E b do c od)) else return () fi)"

After that Burkhart showed an application of this monads theory to run sequential code, unfold "while" instructions and then generate test cases. this was illustrated on a code computing the integer square-root:

record state = 
   tm    :: int
   i     :: int
   sqsum :: int
   a     :: int

lemma SquareRoot: "σ ⊨ assume⇩S⇩E(λσ. 0 ≤ a σ) ;- 
                    assign  (tm_update (λ_ . 1)) ;- 
                    assign  (sqsum_update (λ_ . 1)) ;- 
                    assign  (i_update (λ_ . 0)) ;- 
                   (while⇩S⇩E (λσ. (sqsum σ) <= (a σ)) do 
                      assign  (λσ. σ⦇ i := (i σ + 1)⦈) ;- 
                      assign  (λσ. σ⦇ tm := (tm σ + 2)⦈) ;-
                      assign  (λσ. σ⦇ sqsum := tm σ + sqsum σ⦈) 
                    od);- 
                    assert⇩S⇩E(λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1))"

Burkhart drives the proof, rather using automatic provers, using many tactics he defined to obtain the following proof subgoals that can be interpreted as test-cases. A test case fixes inputs domains and gives a post-condition to validate:

 1. ⋀σ. 0 ≤ a σ ⟹
         ¬ 1 ≤ a σ ⟹
         σ⦇tm := 1, sqsum := 1, i := 0⦈ ⊨
         assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1)) 
 2. ⋀σ. 1 ≤ a σ ⟹
         ¬ 4 ≤ a σ ⟹
         σ⦇i := 1, tm := 3, sqsum := 4⦈ ⊨
         assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1))
 3. ⋀σ. 4 ≤ a σ ⟹
         ¬ 9 ≤ a σ ⟹
         σ⦇i := 2, tm := 5, sqsum := 9⦈ ⊨
         assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1))
 4. ⋀σ. 9 ≤ a σ ⟹
         σ⦇i := 2, tm := 5, sqsum := 9⦈ ⊨
         assign (λσ. σ⦇i := i σ + 1⦈) ;-
         assign (λσ. σ⦇tm := tm σ + 2⦈) ;-
         assign (λσ. σ⦇sqsum := tm σ + sqsum σ⦈) ;-
         (while⇩S⇩E (λσ. sqsum σ
                         ≤ a σ) do assign (λσ. σ⦇i := i σ + 1⦈) ;-
                                    assign (λσ. σ⦇tm := tm σ + 2⦈) ;-
                                    assign (λσ. σ⦇sqsum := tm σ + sqsum σ⦈) od) ;-
         assert⇩S⇩E (λσ. i σ * i σ ≤ a σ ∧ a σ < (i σ + 1) * (i σ + 1))


Previous meeting -- Next meeting