module Inversions
  use int.Int
  use int.NumOf
  use int.Sum
  use seq.Seq
  use proofs.lib.pair.Pair
  use proofs.lib.sum2d.Sum2d
  use proofs.lib.sum2d.Permutation

  type t
  predicate lt t t

  clone relations.PartialStrictOrder with type t = t, predicate rel = lt, axiom .

  predicate inversion (s: seq t) (p : pair) =
    (0 <= p.i < p.j < length s) && (lt s[p.j] s[p.i])

  function  inversions_count  (s: seq t) (p : pair) : int =
    if inversion s p then 1 else 0

  function nb_inversions (s: seq t) : int =
    sum2d (inversions_count s) (length s) (length s)

  let lemma nb_inversions_empty_or_singleton (s : seq t)
    requires { 0 <= length s <= 1 }
    ensures { nb_inversions s = 0 }
  =
    ()

  let function swap (s:seq t) (p : pair) : seq t
    requires { 0 <= p.i < p.j < length s }
    ensures { length result = length s }
    ensures { result[p.i] = s[p.j] }
    ensures { result[p.j] = s[p.i] }
    ensures { forall k. (0 <= k < length s /\ k <> p.i /\ k <> p.j) -> result[k] = s[k] }
  =
    Seq.create (length s) (fun k -> s[if k = p.i then p.j else if k = p.j then p.i else k])

  let function phi (p0 p: pair) : pair
    requires { in_quadrant p0 }
  =
    if p.i < p0.i && p.j = p0.i then mkp p.i p0.j
    else if p.i < p0.i && p.j = p0.j then mkp p.i p0.i
    else if p.i = p0.i && p0.j < p.j then mkp p0.j p.j
    else if p.i = p0.j && p0.j < p.j then mkp p0.i p.j
    else p

  let lemma phi_is_involution (p0 : pair) (n : int)
    requires { in_quadrant_n p0 n }
    ensures {  is_involution (phi p0) n n }
  =
    ()

  let lemma inversions_inc (s : seq t) (p0 : pair)
    requires { in_quadrant p0 }
    requires { inversion s p0 }
    ensures { forall p. inversion (swap s p0) p -> inversion s (phi p0 p) }
  =
    ()

  use proofs.lib.sum2d.SemiLinearity

  let lemma inversions_less (s : seq t)(p0 : pair)
    requires { in_quadrant p0 }
    requires { inversion s p0 }
    ensures {
      let n = length s in
      let f = (inversions_count (swap s p0) ) in
      let g = ((inversions_count s) @ (phi p0)) in
      forall p. in_rect p n n -> f p <= g p
    }
  =
    inversions_inc s p0

  let lemma  inversions_dec (s : seq t) (p0 : pair)
    requires { in_quadrant p0 }
    requires { inversion s p0 }
    ensures { nb_inversions (swap s p0) < nb_inversions s }
  =
    let n = length s in
    assert { nb_inversions s = sum2d (inversions_count s) n n };
    sum_permut (inversions_count s) (phi p0) n n;
    assert { sum2d (inversions_count s) n n = sum2d ( (inversions_count s) @ (phi p0) ) n n };
    assert { (inversions_count (swap s p0) ) p0 < ((inversions_count s) @ (phi p0)) p0 };

    let f = (inversions_count (swap s p0) ) in
    let g = ((inversions_count s) @ (phi p0)) in
    inversions_less s p0;
    sum2d_lt f g n n p0
end

(* generated on Mon Dec  2 02:04:28 UTC 2024 from rev:  *)