Proof of Tarski fixed point theorem (existence of least fixed point) for finite sets, using lemma functions.

Authors: Martin Clochard Léon Gondelman

module Tarski

  use set.Fset
  clone export relations.PartialOrder with axiom .

  constant a : fset t

  constant e : t
  axiom minimality: mem e a /\ forall x. mem x a -> rel e x

  function f t : t
  axiom range: forall x. mem x a -> mem (f x) a
  axiom monotone: forall x y. mem x a -> mem y a -> rel x y -> rel (f x) (f y)

  predicate fixpoint (x:t) = mem x a /\ f x = x

end

module Tarski_rec
  use set.Fset
  clone export Tarski with axiom .

  let lemma least_fix_point () : unit
   ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
   = let rec ghost aux (x: t) (b: fset t) : t
       requires { mem x a /\ subset b a }
       requires { forall y. mem y a -> rel x y -> mem y b }
       requires { forall y. fixpoint y -> rel x y }
       requires { rel x (f x) }
       ensures  { fixpoint result /\ forall x. fixpoint x -> rel result x }
       variant  { cardinal b }
     = let y = f x in if x = y then x else aux y (remove x b)
     in let _witness = aux e a in ()
end

module Tarski_while
  use set.Fset
  clone export Tarski with axiom .
  use ref.Ref

  let lemma least_fix_point () : unit
   ensures {exists mu. fixpoint mu /\ forall x. fixpoint x -> rel mu x }
   =
     let x = ref e in
     let b = ref a in
     while (f !x) <> !x do
      invariant { mem !x a /\ subset !b a}
      invariant { forall y. mem y a -> rel !x y -> mem y !b }
      invariant { forall y. fixpoint y -> rel !x y }
      invariant { rel !x (f !x) }
      variant   { cardinal !b }
      b := remove !x !b;
      x := f !x
     done

end