module Sum2d
  use int.Int
  use proofs.lib.pair.Pair
  use int.Sum

  function sum1d (f : pair -> int) (nj : int) : (int -> int) =
    fun i -> sum ( fun j ->  f (mkp i j)) 0 nj

  function sum2d (f : pair -> int) (ni nj : int) : int =
    sum (sum1d f nj) 0 ni

  let function prec (p : pair) (nj : int) : pair
  =
    if p.j = 0 then (mkp (p.i -1) (nj-1))
    else (mkp p.i (p.j-1))

  let function succ (p : pair) (ni nj : int) : pair
    requires { pair_lt p (mkp (ni-1) nj) }
  =
    if p.j = (nj-1) then (mkp (p.i + 1) 0 )
    else mkp p.i (p.j + 1)

  function minus (f g : pair -> int) : (pair -> int) =
    fun p -> (f p) - (g p)
end

module SumBasics
  use int.Int
  use int.Sum
  use proofs.lib.pair.Pair
  use export Sum2d

  let lemma sum2d_eq (f g : pair -> int) (ni nj : int)
    requires { forall p. 0 <= p.i < ni -> 0 <= p.j < nj -> f p = g p }
    ensures { sum2d f ni nj = sum2d g ni nj }
  =
    ()

  let lemma sum_pos (f : int -> int) (n : int)
    requires { forall i. 0<= i < n -> f i >= 0 }
    ensures { sum f 0 n >= 0 }
  =
    ()

  let lemma sum1d_pos (f : pair -> int) (nj : int)
    requires { forall p. f p >= 0 }
    ensures { forall i. sum1d f nj i >= 0 }
  =
    ()

  let lemma sum2d_pos (f : pair -> int) (ni nj : int)
    requires { forall i j. f (mkp i j) >= 0 }
    ensures { sum2d f ni nj >= 0 }
  =
    sum1d_pos f nj;
    sum_pos (fun i ->  sum1d f nj i) ni

  let lemma sum2d_small (f : pair -> int)
    requires { f (mkp 0 0) = 0 }
    ensures { sum2d f 1 1 = 0 }
  =
    assert { sum2d f 1 1 = f (mkp 0 0) }
end

module SumPath

  use int.Int
  use proofs.lib.pair.Pair
  use int.Sum
  use Sum2d

  let rec function sum_path (f : pair -> int) (ni nj : int) (pmin pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmax ni nj \/ (pmax.i = ni /\ pmax.j = 0) }
  requires { not pair_lt pmax pmin }
  variant { pmax.i, pmax.j }
  =
  if pair_eq pmin pmax then 0
  else f (prec pmax nj) + sum_path f ni nj pmin (prec pmax nj)

   function projection (f : pair -> int) (i : int) : (int -> int)
  = fun j ->  f (mkp i j)

  let lemma sum_proj (f : pair -> int) (i nj : int)
  ensures { sum (projection f i) 0 nj = (sum1d f nj) i } = ()

  let rec lemma sum_path_carac_aux (f : pair -> int) (ni nj : int) (pmin pmax: pair)
  requires {in_rect pmin ni nj}
  requires {in_rect pmax ni nj \/ pair_eq pmax (mkp ni 0)}
  requires { not pair_lt pmax pmin }
  ensures {
   sum_path f ni nj pmin pmax
  = sum (sum1d f nj) pmin.i pmax.i
  - sum (projection f pmin.i) 0 pmin.j
  + sum (projection f pmax.i) 0 pmax.j
  }
  variant { pmax.i, pmax.j }
  =
  (
  if not pair_eq pmin pmax then
  begin
  let sp = sum_path f ni nj pmin pmax in
  let pmax' = prec pmax nj in
  let sp' = sum_path f ni nj pmin pmax' in
  assert { sp = sp' + f pmax'};
  if pmax'.i = pmax.i then
  begin
    sum_path_carac_aux f ni nj pmin pmax';
    assert {
    sum (projection f pmax.i) 0 pmax.j =
    sum (projection f pmax'.i) 0 pmax'.j + f pmax'
    };
  end
  else if pair_lt (mkp 0 0) pmax then
  begin
    assert { pmax.j = 0 };
    assert { pmax'.i = pmax.i - 1 };

    assert { sum (fun j -> f (mkp pmax'.i j)) 0 nj
    = sum (projection f pmax'.i) 0 nj};
    let sl = sum (projection f pmin.i) 0 pmin.j in
    sum_path_carac_aux f ni nj pmin pmax';
    sum_proj f pmax'.i nj;
    assert {
      sp' + f pmax' =
      sum (sum1d f nj) pmin.i pmax'.i
      - sl
      + sum (projection f pmax'.i) 0 pmax'.j
      + f pmax'
      =
      sum (sum1d f nj) pmin.i pmax'.i
      - sl
      + sum (projection f pmax'.i) 0 nj
      =
      sum (sum1d f nj) pmin.i pmax'.i
      - sl
      + (sum1d f nj) pmax'.i
      =
      sum (sum1d f nj) pmin.i pmax.i
      - sl
    };
  end

  end
  )

  let rec lemma sum_path_carac (f : pair -> int) (ni nj : int)
  requires { 1 <= ni }
  requires { 1 <= nj }
  ensures { sum2d f ni nj = sum_path f ni nj (mkp 0 0) (mkp ni 0) }
  =
  (
  )

 let rec lemma sum_path_split (f : pair -> int) (ni nj : int) (pmin pmid pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmid ni nj }
  requires { in_rect pmax ni nj \/ (pmax.i = ni /\ pmax.j = 0) }
  requires { not pair_lt pmax pmid }
  requires { not pair_lt pmid pmin  }
  ensures {
  sum_path f ni nj pmin pmax
  = sum_path f ni nj pmin pmid
  + sum_path f ni nj pmid pmax }
  variant { pmax.i , pmax.j, ni - pmin.i, nj - pmin.j }
  =
  (
  if (not pair_eq pmid pmax) && (not pair_eq pmin pmid) then
  begin
    assert { pair_lt pmid pmax };
    assert { pair_lt pmin pmid };
    let pmax' = (prec pmax nj) in
    sum_path_split f ni nj pmin pmid pmax';
    assert { sum_path f ni nj pmin pmax =
    sum_path f ni nj pmin pmax' + f pmax'};
    assert {
  sum_path f ni nj pmin pmax
  = sum_path f ni nj pmin pmid
  + sum_path f ni nj pmid pmax }
  end
  )

  let lemma sum_path_split_pivot (f : pair -> int) (ni nj : int) (pmin pmid pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmid ni nj }
  requires { in_rect pmax ni nj \/ (pmax.i = ni /\ pmax.j = 0) }
  requires { not pair_lt pmid pmin }
  requires { pair_lt pmid pmax }
  ensures {
  let pmid' = (succ pmid ni nj) in
  sum_path f ni nj pmin pmax
  = sum_path f ni nj pmin pmid
  + f pmid
  + if pair_lt pmid' pmax
  then sum_path f ni nj pmid' pmax
  else 0
  }
  =
  (
    sum_path_split f ni nj pmin pmid pmax;
    if not (pmid.i = ni-1 && pmid.j = nj-1) then
    begin
    let pmid' = (succ pmid ni nj) in
    sum_path_split f ni nj pmid pmid' pmax;
    end
  )

  let rec lemma sum_path_non_neg (f : pair -> int) (ni nj : int) (pmin pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmax ni nj \/ (pair_eq pmax (mkp ni 0) )}
  requires { not pair_lt pmax pmin  }
  requires { forall p.
    in_rect p ni nj
    -> pair_lt p pmax
    -> not pair_lt p pmin
    -> f p >= 0
   }
  ensures { sum_path f ni nj pmin pmax >= 0 }
  variant { pmax.i, pmax.j }
  =
  (
  if pair_lt pmin pmax then
  begin
  let sp = sum_path f ni nj pmin pmax in
  let pmax' = prec pmax nj in
  let sp' = sum_path f ni nj pmin pmax' in
  assert { sp = sp' + f pmax'};
  assert { in_rect pmax' ni nj };
  assert { not pair_lt pmax' pmin };
  assert { pair_lt pmax' pmax };
  assert { f pmax' >= 0 };
  sum_path_non_neg f ni nj pmin (prec pmax nj);
  assert { sp' >= 0 };
  end
  )

  let rec lemma sum_path_minus (f g : pair -> int) (ni nj : int) (pmin pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmax ni nj \/ (pair_eq pmax (mkp ni 0) )}
  requires { not pair_lt pmax pmin  }
  ensures { sum_path (minus f g) ni nj pmin pmax
    = (sum_path f ni nj pmin pmax) - (sum_path g ni nj pmin pmax) }
  variant { pmax.i, pmax.j}
  =(
    if pair_lt pmin pmax then
      let pmax' = prec pmax nj in
        sum_path_minus f g ni nj pmin pmax'
  )

 let rec lemma sum_path_lte (f g : pair -> int) (ni nj : int) (pmin pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmax ni nj \/ (pair_eq pmax (mkp ni 0) )}
  requires { forall p.
    in_rect p ni nj
    -> not pair_lt p pmin
    -> pair_lt p pmax
    -> f p <= g p  }
  requires { not pair_lt pmax pmin }
  ensures { sum_path f ni nj pmin pmax <= sum_path g ni nj pmin pmax }
  =
  (
  sum_path_non_neg  (minus g f ) ni nj pmin pmax;
  assert { 0<= sum_path (minus g f ) ni nj pmin pmax };
  sum_path_minus g f ni nj pmin pmax;
  )

let rec lemma sum_path_eq (f g : pair -> int) (ni nj : int) (pmin pmax: pair)
  requires { in_rect pmin ni nj }
  requires { in_rect pmax ni nj \/ (pair_eq pmax (mkp ni 0) )}
  requires { forall p.
    in_rect p ni nj
    -> not pair_lt p pmin
    -> pair_lt p pmax
    -> f p = g p  }
  requires { not pair_lt pmax pmin }
  ensures { sum_path f ni nj pmin pmax = sum_path g ni nj pmin pmax }
  =
  (
  sum_path_lte f g ni nj pmin pmax;
  sum_path_lte g f ni nj pmin pmax;
  )

 end

module Linearity

  use int.Int
  use proofs.lib.pair.Pair
  use int.Sum
  use Sum2d
  use SumPath as SP

  let lemma sum2d_minus (f g : pair -> int) (ni nj : int)
  requires { 1 <= ni /\ 1 <= nj }
  ensures { sum2d (minus f g) ni nj = (sum2d f ni nj) - (sum2d g ni nj) }
  =
  (
    let pmin = mkp 0 0 in
    let pmax = mkp ni 0 in
    SP.sum_path_minus f g ni nj pmin pmax
  )

  let lemma sum2d_split (f : pair -> int) (ni nj : int) (p0 p1 : pair)
  requires { in_rect p0 ni nj /\ in_rect p1 ni nj }
  requires { pair_lt p0 p1 }
  ensures {
  let pmin = mkp 0 0 in
  let pmax = mkp ni 0 in
  let p0' = succ p0 ni nj in
  let p1' = succ p1 ni nj in
   sum2d f ni nj =
    SP.sum_path f ni nj pmin p0
    + f p0
    + SP.sum_path f ni nj p0' p1
    + f p1
    + if pair_lt p1' pmax
      then SP.sum_path f ni nj p1' pmax
      else 0
   }
   =(
   let pmin = mkp 0 0 in
   let pmax = mkp ni 0 in
   SP.sum_path_split_pivot f ni nj pmin p0 pmax;
   SP.sum_path_split_pivot f ni nj p0 p1 pmax;
   )

end

module SemiLinearity

  use int.Int
  use proofs.lib.pair.Pair
  use int.Sum
  use Sum2d
  use SumPath as SP

  let lemma sum2d_pos (f : pair -> int) (ni nj : int) (p0 : pair)
  requires { forall p. in_rect p ni nj -> 0 <= f p }
  requires { in_rect p0 ni nj /\ 0 < f p0 }
  ensures { 0 < sum2d f ni nj }
  =
  (
  let pmin = (mkp 0 0) in
  let pmax = (mkp ni 0) in
  SP.sum_path_non_neg f ni nj pmin p0;
  if pair_lt p0 (mkp (ni-1) (nj -1)) then
  begin
    let p0' = (succ p0 ni nj) in
    SP.sum_path_split_pivot f ni nj  pmin p0 pmax;
    SP.sum_path_non_neg f ni nj p0' pmax;
  end
  )

  let lemma sum2d_lte (f g : pair -> int) (ni nj : int)
  requires { 1 <= ni /\ 1 <= nj }
  requires { forall p. in_rect p ni nj -> f p <= g p  }
  ensures { sum2d f ni nj <= sum2d g ni nj }
  =
  (
    let pmin = (mkp 0 0) in
    let pmax = (mkp ni 0) in
    SP.sum_path_lte f g ni nj pmin pmax;
  )

  let rec lemma sum2d_lt (f g : pair -> int) (ni nj : int) (p0 : pair)
  requires { forall p. in_rect p ni nj -> f p <= g p  }
  requires { in_rect p0 ni nj /\ f p0 < g p0 }
  ensures { sum2d f ni nj < sum2d g ni nj }
  =
  (
    sum2d_pos (minus g f ) ni nj p0
  )

end

module Permutation

  use proofs.lib.pair.Pair
  use Sum2d
  use int.Int
  use Linearity as L
  use SemiLinearity as S
  use SumPath as SP

  predicate is_involution (phi : pair -> pair ) (ni nj : int)
  = forall p. in_rect p ni nj ->
  (in_rect (phi p) ni nj /\ phi (phi p) = p)

  let function (@) (f : pair -> int) (phi : pair -> pair)
  = fun p -> f (phi p)

  let function transpose (p0 p1 : pair) : (pair -> pair)
  = fun p -> if pair_eq p p0 then p1 else if pair_eq p p1 then p0 else p

  let function compose (phi1 phi2 : pair -> pair) : (pair -> pair)
  = fun p -> phi1 (phi2 p)

  let lemma sum_transp (f f' : pair -> int) (p0 p1 : pair) (ni nj : int)
  requires { in_rect p0 ni nj }
  requires { in_rect p1 ni nj }
  requires { pair_lt p0 p1 }
  requires { f' = f @ transpose p0 p1 }
  ensures { sum2d f ni nj = sum2d f' ni nj }
  =
  (

    let pmin = (mkp 0 0) in
    let pmax = (mkp ni 0) in
    let p0' = succ p0 ni nj in
    let p1' = succ p1 ni nj in

    assert {
    forall p.
    in_rect p ni nj
    /\ not pair_eq p p0
    /\ not pair_eq p p1
    -> f p = f' p };

    SP.sum_path_eq f f' ni nj pmin p0;
    SP.sum_path_eq f f' ni nj p0' p1;
    if pair_lt p1' pmax then
      SP.sum_path_eq f f' ni nj p1' pmax;

    L.sum2d_split f ni nj p0 p1;
    L.sum2d_split f' ni nj p0 p1;

     assert { f p0 = f' p1 };
     assert { f p1 = f' p0 };
     assert {
    sum2d f ni nj =
    SP.sum_path f ni nj pmin p0
    + f p0
    + SP.sum_path f ni nj p0' p1
    + f p1
    + (if pair_lt p1' pmax
      then SP.sum_path f ni nj p1' pmax
      else 0)
      =
    SP.sum_path f' ni nj pmin p0
    + f p0
    + SP.sum_path f' ni nj p0' p1
    + f p1
    + (if pair_lt p1' pmax
      then SP.sum_path f' ni nj p1' pmax
      else 0)
      =
    SP.sum_path f' ni nj pmin p0
    + f' p1
    + SP.sum_path f' ni nj p0' p1
    + f' p0
    + (if pair_lt p1' pmax
      then SP.sum_path f' ni nj p1' pmax
      else 0)
      =
    SP.sum_path f' ni nj pmin p0
    + f' p0
    + SP.sum_path f' ni nj p0' p1
    + f' p1
    + (if pair_lt p1' pmax
      then SP.sum_path f' ni nj p1' pmax
      else 0)
      =
      sum2d f' ni nj
      }

  )

   let function swap (phi : pair -> pair) (p0 : pair) : (pair -> pair)
  = compose phi (transpose p0 (phi p0))

  let lemma invol_swap (phi : pair -> pair) (p0 : pair) (ni nj : int)
  requires { in_rect p0 ni nj }
  requires { is_involution phi ni nj }
  ensures { is_involution (swap phi p0) ni nj }
  =
  ()

  let function umkp (p : pair) (ni nj: int) : int
  = (ni - p.i) * (nj+1) + (nj - p.j)

  let lemma mult_pos (i j: int)
  requires { i>= 0 && j >= 0 }
  ensures { i* j >= 0 }
  = ()

  let lemma umkp_dec (p0 p1 : pair) (ni nj: int)
  requires { in_rect p0 ni nj \/ pair_eq p0 (mkp ni 0) }
  requires { in_rect p1 ni nj }
  requires { pair_lt p1 p0 }
  ensures { 0 <= umkp p0 ni nj < umkp p1 ni nj }
    =(
          assert { p0.i > p1.i \/ (p0.i = p1.i /\ p0.j > p1.j) };
      if p0.i > p1.i then
      begin
      let a = (ni - p0.i + 1) in
      let b  = (ni - p1.i) in
      let x = (nj+1) in
        assert { 0 <= a <= b  };
        assert { 0 <= x } ;
        mult_pos a x;
        assert { 0 <= a * x  };
        assert { a * x <= b * x  };
        assert { a *x =    (ni - p0.i) * (nj+1) + (nj+1) };
        assert { b *x =    (ni - p1.i) * (nj+1) };
        assert { 0 <= (ni - p0.i) * (nj+1) + (nj+1) <= (ni - p1.i) * (nj+1) };
        assert { 0 <= (ni - p0.i) * (nj+1) + (nj - p0.j) < (ni - p1.i) * (nj+1)  };
        assert { 0 <= (ni - p0.i) * (nj+1) + (nj - p0.j) < (ni - p1.i) * (nj+1) + (nj - p1.j) };
      end

)

  let rec function first_diff (phi : pair -> pair) (ni nj : int) (p0 : pair) : pair
  requires { p0 = mkp ni 0 \/ in_rect p0 ni nj }
  requires { forall p. in_rect p ni nj -> pair_lt p p0 -> phi p = p }
  ensures { forall p. in_rect p ni nj -> pair_lt p result -> phi p = p  }
  ensures { result = mkp ni 0 \/ (in_rect result ni nj /\ phi result <> result)  }
  variant { ni - p0.i, nj - p0.j }
  =
  (
  if p0.i = ni && p0.j = 0  then p0
  else if pair_neq p0 (phi p0) then p0
  else if p0.j = nj-1 then first_diff phi ni nj (mkp (p0.i +1) 0)
  else first_diff phi ni nj (mkp p0.i (p0.j +1) )
  )

  let rec lemma sum_permut_aux (f : pair -> int) (g : pair -> pair) (ni nj: int)
  requires { is_involution g ni nj }
  ensures { sum2d f ni nj = sum2d ( f @ g ) ni nj }
  variant { umkp (first_diff g ni nj  (mkp 0 0) ) ni nj  }
  =
  (
  if ni > 0 && nj > 0 then
  begin
    let fdg = first_diff g ni nj (mkp 0 0) in
    if pair_eq fdg (mkp ni 0) then
    begin
      assert { forall p. in_rect p ni nj -> f p = (f @ g) p };
      S.sum2d_lte f (f@g) ni nj;
      assert { sum2d f ni nj <= sum2d ( f @ g ) ni nj };
      S.sum2d_lte (f@g) f ni nj;
      assert { sum2d ( f @ g ) ni nj <= sum2d f ni nj }
    end
    else
    begin
      let fdg' = g fdg in
      assert { g fdg <> fdg };
      assert { pair_lt fdg fdg' };
      let h = swap g fdg in
      assert { forall p. in_rect p ni nj -> pair_lt p fdg -> h p = p  };
      assert { h fdg = fdg };
      let fdh = first_diff h ni nj  (mkp 0 0) in
      assert { pair_lt fdg fdh  } ;
      umkp_dec fdh fdg ni nj;
      assert { umkp fdh ni nj < umkp fdg ni nj } ;
      sum_permut_aux f h ni nj;
      assert {
      let fg = (f @g) in
      let fh = (f @ h) in
      fh = fg @ (transpose fdg fdg') };
      assert { sum2d ( f @ g ) ni nj = sum2d ( f @ h ) ni nj };

    end
  end
   )

  let  lemma sum_permut (f : pair -> int) (g : pair -> pair) (ni nj : int)
  requires { 1 <= ni /\ 1 <= nj }
  requires { is_involution g ni nj }
  ensures { sum2d f ni nj = sum2d ( f @ g ) ni nj }
  =
  (
    sum_permut_aux f g ni nj;
    assert { sum2d f ni nj = sum2d ( f @ g ) ni nj }

  )

end

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