module Permutation

  use int.Int
  use map.Map

  predicate in_range (n: int) (f: int -> int) =
    forall i. 0 <= i < n -> 0 <= f i < n

  predicate injective (n: int) (f: int -> int) =
    forall i j. 0 <= i < n -> 0 <= j < n -> i <> j -> f i <> f j

  type permutation = {
    n: int;
    map: int -> int;
    inv: int -> int;
  } invariant { n >= 0 }
    invariant { in_range n map }
    invariant { in_range n inv }
    invariant { forall i. 0 <= i < n -> inv[map[i]] = i }
    invariant { forall i. 0 <= i < n -> map[inv[i]] = i }
  by { n = 0;
       map = (fun i -> i);
       inv = (fun i -> i); }

  meta coercion function map

  let function identity (n: int) : permutation
    requires { n >= 0 }
  =
  { n = n;
      map = (fun i -> i);
      inv = (fun i -> i); }

  let function compose_ranged_fun (n : int) (f1 f2 : int -> int) : int -> int
  requires { in_range n f1 }
  requires { in_range n f2 }
  ensures { in_range n result }
  = fun i -> f2 (f1 i)

  let function compose (p1 p2: permutation) : permutation
  requires { p1.n = p2.n }
  ensures { result.n = p1.n }
  ensures { result.map = compose_ranged_fun p1.n p1.map p2.map }
  = (

  let result =
    {
        n = p1.n ;
        map = compose_ranged_fun p1.n p1.map p2.map;
        inv = compose_ranged_fun p1.n p2.inv p1.inv;
      } in
      assert { result.n >= 0 };
      assert { in_range p1.n result.map };
      assert { in_range p1.n result.inv };
      result;
      )

  let function inverse (p: permutation) : (permutation) =
    { n = p.n; map = p.inv; inv = p.map; }

  let rec lemma from_map (n : int) (f : int -> int) : permutation
  requires { n >= 0 }
  requires { in_range n f }
  requires { injective n f }
  ensures { result.n = n  }
  ensures { result.map = f   }
  variant { n }
  =
  (
  if n = 0 then
    { n = 0; map = f; inv = f }
  else
    begin
    let x = f 0 in
    let rm = fun x k -> if k < x then k else k - 1 in
    let fx = fun k -> rm x (f (k+1)) in
    let invx = (from_map (n - 1) fx).inv in
    let insert0 = fun k -> if k < x then k else if k = x then 0 else k -1 in
      { n = n;
        map = f ;
        inv = fun k ->
          if k = x then 0
          else 1 + invx (rm x k)
        }
    end
  )

  let rec function first_not_id_rec (p : permutation) (i : int) : int
    requires { 0 <= i <= p.n }
    requires { forall k. 0<= k < i -> (p k) = k }
    ensures { 0 <= result <= p.n }
    ensures { forall k. 0<= k < result -> (p k) = k }
    ensures { result < p.n -> (p result) <> result }
    variant { p.n - i }
  =
    if i = p.n then
      p.n
    else if ((p.map i) <> i) then
      i
    else
      first_not_id_rec p (i+1)

  let function first_not_id (p : permutation) : int
    ensures { 0 <= result <= p.n }
    ensures { forall k. 0<= k < result -> p k = k }
    ensures { result < p.n -> p result <> result }
    ensures { result < p.n -> forall k. 0 <= k < p.n -> p k < result ->
              p (p k) = (p k)  < result }
    ensures { result < p.n -> forall k. 0 <= k < p.n -> p k < result ->
              k < result }
    ensures { result < p.n -> forall k. result <= k < p.n -> result <= p k }
  =
    first_not_id_rec p 0

   use seq.Seq

   let function permut (s : seq 'a) (p : permutation) : seq 'a
     requires { length s = p.n }
     ensures { length result = length s }
     ensures { forall k. 0 <= k < length s -> result[k] = s[p k] }
     ensures { forall k. 0 <= k < length s -> s[k] = result[p.inv k] }
   =
     create (length s) (fun k -> s[p.map k])
end

module Swap
  use int.Int
  use seq.Seq
  use Permutation

  let function fswap (i j k : int) : int =
    (if k = i then j else if k = j then i else k)

  let function transposition (n i j : int) : permutation
    requires { 0 <= i < n }
    requires { 0 <= j < n }
    ensures { result.n = n}
    ensures { result.map = fswap i j }
    ensures { result.inv = fswap i j }
  = { n = n; map = (fswap i j); inv = (fswap i j) }

  function swap (s:seq 'a) (i : int) (j : int) : seq 'a =
    permut s (transposition (length s) i j )

  let lemma swap_spec (s:seq 'a) (i : int) (j : int)
    requires{ 0 <= i < length s }
    requires{ 0 <= j < length s }
    ensures { length (swap s i j) = length s }
    ensures { (swap s i j)[i] = s[j] }
    ensures { (swap s i j)[j] = s[i] }
    ensures { forall k.
    	       0 <= k < length s ->
               k <> i ->
	       k <> j ->
    	      (swap s i j)[k] = s[k] }
   = ()
end

(* generated on Thu Nov 21 02:04:27 UTC 2024 from rev:  *)