examples/finite_tarski.mlw

   1 (**
   2
   3 Proof of Tarski fixed point theorem (existence of least fixed point)
   4 for finite sets, using lemma functions.
   5
   6 Authors:  Martin Clochard
   7           Léon Gondelman
   8 *)
   9
  10
  11 module Tarski
  12
  13   use set.Fset
  14   clone export relations.PartialOrder with axiom .
  15
  16   constant a : fset t
  17
  18   constant e : t
  19   axiom minimality: mem e a /\ forall x. mem x a -> rel e x
  20
  21   function f t : t
  22   axiom range: forall x. mem x a -> mem (f x) a
  23   axiom monotone: forall x y. mem x a -> mem y a -> rel x y -> rel (f x) (f y)
  24
  25   predicate fixpoint (x:t) = mem x a /\ f x = x
  26
  27 end
  28
  29 module Tarski_rec
  30   use set.Fset
  31   clone export Tarski with axiom .
  32
  33   let lemma least_fix_point () : unit
  34    ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
  35    = let rec ghost aux (x: t) (b: fset t) : t
  36        requires { mem x a /\ subset b a }
  37        requires { forall y. mem y a -> rel x y -> mem y b }
  38        requires { forall y. fixpoint y -> rel x y }
  39        requires { rel x (f x) }
  40        ensures  { fixpoint result /\ forall x. fixpoint x -> rel result x }
  41        variant  { cardinal b }
  42      = let y = f x in if x = y then x else aux y (remove x b)
  43      in let _witness = aux e a in ()
  44 end
  45
  46 module Tarski_while
  47   use set.Fset
  48   clone export Tarski with axiom .
  49   use ref.Ref
  50
  51   let lemma least_fix_point () : unit
  52    ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
  53    =
  54      let x = ref e in
  55      let b = ref a in
  56      while (f !x) <> !x do
  57       invariant { mem !x a /\ subset !b a}
  58       invariant { forall y. mem y a -> rel !x y -> mem y !b }
  59       invariant { forall y. fixpoint y -> rel !x y }
  60       invariant { rel !x (f !x) }
  61       variant   { cardinal !b }
  62       b := remove !x !b;
  63       x := f !x
  64      done
  65
  66 end