:: Algorithm NextFit for the Bin Packing Problem
::  by Hiroshi Fujiwara , Ryota Adachi and Hiroaki Yamamoto
:: 
:: Received June 30, 2021
:: Copyright (c) 2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies BINPACK1, NUMBERS, NAT_1, FINSEQ_1, CARD_1, RELAT_1, SUBSET_1,
      XBOOLE_0, FUNCT_1, TARSKI, ORDINAL4, ARYTM_1, ARYTM_3, REAL_1, ZFMISC_1,
      XXREAL_0, CARD_3, INT_1, FINSEQ_2, VALUED_0, PARTFUN1, ABIAN, FINSET_1,
      CLASSES1, RFUNCT_3, AFINSQ_1, AFINSQ_2, PRGCOR_2;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, ORDINAL1, CARD_1, ABIAN, BINOP_1, NUMBERS, XCMPLX_0,
      XXREAL_0, XREAL_0, FINSEQ_1, FINSEQ_2, FINSEQOP, RVSUM_1, INT_1,
      FINSET_1, VALUED_0, CLASSES1, RFUNCT_3, GLIB_003, RVSUM_3, AFINSQ_1,
      AFINSQ_2;
 constructors CARD_1, RELSET_1, RVSUM_1, NAT_D, CLASSES1, RFUNCT_3, DBLSEQ_1,
      GLIB_003, PROB_1, PARTFUN3, AFINSQ_2, RECDEF_1, WELLORD2;
 registrations ORDINAL1, XBOOLE_0, FUNCT_1, NUMBERS, XREAL_0, NAT_1, FINSEQ_1,
      FINSEQ_2, VALUED_0, RELAT_1, RVSUM_1, ABIAN, RELSET_1, INT_1, FINSET_1,
      CARD_1, XXREAL_0, MEMBERED, AFINSQ_1, AFINSQ_2, NAT_6;
 requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;


begin :: Preliminaries

definition
  let a be non empty FinSequence of REAL;
  let i be Element of dom a;
  redefine func a . i -> Element of REAL;
end;

definition
  let h be non empty FinSequence of NAT*;
  let i be Element of dom h;
  redefine func h . i -> FinSequence of NAT;
end;

theorem :: BINPACK1:1
  for n being Nat st n is odd holds 1 <= n & (n + 1) div 2 = (n + 1) / 2;

theorem :: BINPACK1:2
  for D be set, p being FinSequence st
  (for i being Nat st i in dom p holds p . i in D) holds
  p is FinSequence of D;

theorem :: BINPACK1:3
  for x, y being object holds {[x, y]} " {y} = {x};

theorem :: BINPACK1:4
  for a, b being Nat, s being set holds
  Seg a \/ {s} = Seg b implies a = b or a + 1 = b;

definition
  let D be non empty set;
  let f be D-valued FinSequence;
  let I be set;
:::  assume I c= dom f; :: not needed to prove the correctness of definition
  func Seq (f, I) -> D-valued FinSequence equals
:: BINPACK1:def 1
  Seq (f | I);
end;

definition
  let a be non empty FinSequence of REAL;
  let f be Function;
  let s be set;
  func SumBin (a, f, s) -> Real equals
:: BINPACK1:def 2
  Sum (Seq (a, (f " s)));
end;

registration
  cluster positive for non empty FinSequence of REAL;
end;

definition
  let a be FinSequence of REAL;
  attr a is at_most_one means
:: BINPACK1:def 3
  for i being Nat st 1 <= i & i <= len a holds a . i <= 1;
end;

registration
  cluster at_most_one for non empty positive FinSequence of REAL;
end;

theorem :: BINPACK1:5
  for f being FinSequence of NAT, j, b being Nat holds
  b = j implies (f ^ <* b *>) " {j} = f " {j} \/ {len f + 1};

theorem :: BINPACK1:6
  for f being FinSequence of NAT, j, b being Nat holds
  b <> j implies (f ^ <* b *>) " {j} = f " {j};

theorem :: BINPACK1:7
  for a being non empty FinSequence of REAL,
      p being set, i being Nat st
  (p \/ {i}) c= dom a &
  (for m being Nat st m in p holds m < i) holds
  Seq (a | (p \/ {i})) = Seq (a | p) ^ <* a . i *>;

theorem :: BINPACK1:8
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT, j, b being Nat st
  len f + 1 <= len a holds
  b = j implies
  SumBin (a, f ^ <* b *>, {j}) = SumBin (a, f, {j}) + a . (len f + 1);

theorem :: BINPACK1:9
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT, j, b being Nat st
  len f + 1 <= len a holds
  b <> j implies
  SumBin (a, f ^ <* b *>, {j}) = SumBin (a, f, {j});

theorem :: BINPACK1:10
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT st
  dom f = dom a holds
  SumBin (a, f, rng f) = Sum a;

theorem :: BINPACK1:11
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT, s, t being set st s misses t holds
  SumBin (a, f, s \/ t) = SumBin (a, f, s) + SumBin (a, f, t);

theorem :: BINPACK1:12
  for a being non empty positive FinSequence of REAL,
  f being FinSequence of NAT, s being set holds
  0 <= SumBin (a, f, s);

theorem :: BINPACK1:13
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT, s be set st
  s misses rng f holds
  SumBin (a, f, s) = 0;

begin :: Optimal Packing

theorem :: BINPACK1:14
  for a being non empty at_most_one FinSequence of REAL holds
  ex k being Nat st
  ex f being non empty FinSequence of NAT st
  dom f = dom a &
  (for j being Nat st j in rng f holds SumBin (a, f, {j}) <= 1) &
  k = card rng f;

theorem :: BINPACK1:15
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT st
  dom f = dom a &
  (for j being Nat st j in rng f holds SumBin (a, f, {j}) <= 1) holds
  ex fr being FinSequence of NAT st
  dom fr = dom a &
  (for j being Nat st j in rng fr holds SumBin (a, fr, {j}) <= 1) &
  (ex k being Nat st rng fr = Seg k) &
  card rng f = card rng fr;

definition
  let a be non empty at_most_one FinSequence of REAL;
  func Opt(a) -> Element of NAT means
:: BINPACK1:def 4

  ex g being non empty FinSequence of NAT st
  dom g = dom a &
  (for j being Nat st j in rng g holds SumBin (a, g, {j}) <= 1) &
  it = card rng g &
  (for f being non empty FinSequence of NAT st
  dom f = dom a &
  (for j being Nat st j in rng f holds SumBin (a, f, {j}) <= 1) holds
  it <= card rng f);
end;

theorem :: BINPACK1:16
  for a being non empty FinSequence of REAL, f being FinSequence of NAT,
  k being Nat, R1 being real-valued FinSequence st
  dom f = dom a & (rng f = Seg k) & len R1 = k &
  (for j being Nat st j in dom R1 holds R1 . j = SumBin (a, f, {j})) holds
  Sum R1 = SumBin (a, f, rng f);

theorem :: BINPACK1:17
  for a being non empty FinSequence of REAL,
  f being FinSequence of NAT st
  dom f = dom a &
  (for j being Nat st j in rng f holds SumBin (a, f, {j}) <= 1) holds
  [/ (Sum a) \] <= card rng f;

theorem :: BINPACK1:18
  for a being non empty at_most_one FinSequence of REAL holds
  [/ Sum a \] <= Opt a;

begin

definition
  let a be non empty FinSequence of REAL,
  Alg be Function of [:REAL,NAT*:],NAT;
  func OnlinePackingHistory(a, Alg) -> non empty FinSequence of NAT*
  means
:: BINPACK1:def 5

  len it = len a &
  it . 1 = <* 1 *> &
  for i being Nat st 1 <= i & i < len a holds
  ex d1 being Element of REAL, d2 being FinSequence of NAT
  st d1 = a . (i + 1) & d2 = it . i &
  it . (i + 1) = d2 ^ <* Alg . (d1, d2) *>;
end;

theorem :: BINPACK1:19
  for a be non empty FinSequence of REAL,
  Alg being Function of [:REAL,NAT*:],NAT holds
  (OnlinePackingHistory(a, Alg)) . 1 = {[1, 1]};

theorem :: BINPACK1:20
  for a being non empty FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, Alg) holds
  SumBin (a, h . 1, {(h . 1) . 1}) = a . 1;

theorem :: BINPACK1:21
  for a being non empty FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, Alg) holds
  (for i being Nat st 1 <= i & i <= len a holds
  h . i is FinSequence of NAT);

theorem :: BINPACK1:22
  for a being non empty FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, Alg) holds
  (for i being Nat st 1 <= i & i <= len a holds len (h . i) = i);

theorem :: BINPACK1:23
  for a being non empty FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, Alg) holds
  (for i being Nat st 1 <= i & i < len a holds
  h . (i + 1) = (h . i) ^ <* Alg . (a . (i + 1), h . i) *> &
  (h . (i + 1)) . (i + 1) =  Alg . (a . (i + 1), h . i));

theorem :: BINPACK1:24
  for a being non empty FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, Alg) holds
  (for i being Nat st 1 <= i & i < len a holds
  rng (h . (i + 1)) = rng (h . i) \/ {(h . (i + 1)) . (i + 1)});

theorem :: BINPACK1:25
  for a being non empty positive FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, Alg) holds
  (for i, l being Nat st
  1 <= i & i < len a holds
  SumBin (a, h . i, {l}) <= SumBin (a, h . (i + 1), {l}));

definition
  let a be non empty FinSequence of REAL, Alg be Function of [:REAL,NAT*:],NAT;
  func OnlinePacking(a, Alg) -> non empty FinSequence of NAT
  equals
:: BINPACK1:def 6
  OnlinePackingHistory(a, Alg) . (len OnlinePackingHistory(a, Alg));
end;

theorem :: BINPACK1:26
  for a being non empty FinSequence of REAL,
  Alg being Function of [:REAL, NAT*:],NAT,
  h being non empty FinSequence of NAT*,
  f being non empty FinSequence of NAT holds
  dom OnlinePacking(a, Alg) = dom a;

begin

definition
  let a be non empty FinSequence of REAL;
  func NextFit(a) -> Function of [:REAL, NAT*:],NAT
  means
:: BINPACK1:def 7

  for s be Real, f be FinSequence of NAT holds
  (s + SumBin (a, f, {f . (len f)}) <= 1 implies it . (s, f) = f . (len f)) &
  (s + SumBin (a, f, {f . (len f)}) > 1 implies it . (s, f) = f . (len f) + 1);
end;

theorem :: BINPACK1:27
  for a being non empty FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  (for i being Nat st 1 <= i & i <= len a holds
  ex k being Nat st rng (h . i) = Seg k & (h . i) . i = k);

theorem :: BINPACK1:28
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  for i being Nat st 1 <= i & i <= len a holds
  SumBin (a, h . i, {(h . i) . i}) <= 1;

theorem :: BINPACK1:29
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  for i, j being Nat st 1 <= i & i <= len a & j in rng (h . i) holds
  SumBin (a, h . i, {j}) <= 1;

theorem :: BINPACK1:30
  for a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT st
  f = OnlinePacking(a, NextFit(a)) holds
  for j being Nat st j in rng f holds SumBin (a, f, {j}) <= 1;

begin :: Approximation Guarantee of Algorithm NextFit

theorem :: BINPACK1:31
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  (for i, k being Nat st
  1 <= i & i <= len a & rng (h . i) = Seg k holds (h . i) . i = k);

theorem :: BINPACK1:32
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  (for i, k being Nat st 1 <= i & i < len a &
  rng (h . i) = Seg k & rng (h . (i + 1)) = Seg (k + 1) holds
  SumBin (a, (h . (i + 1)), {k}) + SumBin (a, (h . (i + 1)), {k + 1}) > 1);

theorem :: BINPACK1:33
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  (for i, l, k being Nat st 1 <= i & i <= len a &
  rng (h . i) = Seg k & 2 <= k & 1 <= l & l < k holds
  SumBin (a, (h . i), {l}) + SumBin (a, (h . i), {l + 1}) > 1);

theorem :: BINPACK1:34
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT* st
  h = OnlinePackingHistory(a, NextFit(a)) holds
  (for i, j, k be Nat st 1 <= i & i <= len a &
  rng (h . i) = Seg k & 2 <= k & 1 <= j & j <= k div 2 holds
  SumBin (a, (h . i), {2 * j - 1}) + SumBin (a, (h . i), {2 * j}) > 1);

theorem :: BINPACK1:35
  for a being non empty positive at_most_one FinSequence of REAL,
  h being non empty FinSequence of NAT*,
  f being FinSequence of NAT st
  f = OnlinePacking(a, NextFit(a)) holds
  ex k being Nat st rng f = Seg k;

theorem :: BINPACK1:36
  for a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT, k being Nat st
  f = OnlinePacking(a, NextFit(a)) & rng f = Seg k holds
  (for j being Nat st 1 <= j & j <= k div 2 holds
  SumBin (a, f, {2 * j - 1}) + SumBin (a, f, {2 * j}) > 1);

theorem :: BINPACK1:37
  for a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT, k being Nat st
  f = OnlinePacking(a, NextFit(a)) & k = card rng f holds
  k div 2 < Sum a;

theorem :: BINPACK1:38
  for a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT, k being Nat st
  f = OnlinePacking(a, NextFit(a)) & k = card rng f holds
  k <= 2 * [/ Sum a \] - 1;

theorem :: BINPACK1:39
  for a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT, k being Nat st
  f = OnlinePacking(a, NextFit(a)) & k = card rng f holds
  k <= 2 * Opt a - 1;

begin :: Tightness of Approximation Guarantee of Algorithm NextFit

theorem :: BINPACK1:40
  for n being Nat, epsilon being Real,
  a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT st
  n is odd & len a = n & epsilon = 1 / (n + 1) &
  (for i being Nat st i in Seg n holds
  (i is odd  implies a . i = 2 * epsilon) &
  (i is even implies a . i = 1 - epsilon)) &
  f = OnlinePacking(a, NextFit(a)) holds
  n = card rng f;

theorem :: BINPACK1:41
  for n being Nat, epsilon being Real,
  a being non empty positive at_most_one FinSequence of REAL st
  n is odd & len a = n & epsilon = 1 / (n + 1) &
  (for i being Nat st i in Seg n holds
  (i is odd  implies a . i = 2 * epsilon) &
  (i is even implies a . i = 1 - epsilon)) holds
  Sum a = (n + 1) / 2 + 1 / (n + 1) - 1 / 2;

theorem :: BINPACK1:42
  for n being Nat, epsilon being Real,
  a being non empty positive at_most_one FinSequence of REAL,
  f being non empty FinSequence of NAT st
  n is odd & len a = n & epsilon = 1 / (n + 1) &
  (for i being Nat st i in Seg n holds
  (i is odd  implies a . i = 2 * epsilon) &
  (i is even implies a . i = 1 - epsilon)) &
  dom f = dom a &
  (for i being Nat st i in Seg n holds
  (i is odd  implies f . i = 1) &
  (i is even implies f . i = i div 2 + 1)) holds
  for j being Nat st j in rng f holds SumBin (a, f, {j}) <= 1;

theorem :: BINPACK1:43
  for n being Nat, epsilon being Real,
  a being non empty positive at_most_one FinSequence of REAL st
  n is odd & len a = n & epsilon = 1 / (n + 1) &
  (for i being Nat st i in Seg n holds
  (i is odd  implies a . i = 2 * epsilon) &
  (i is even implies a . i = 1 - epsilon)) holds n = 2 * Opt a - 1;

theorem :: BINPACK1:44
  for n being Nat st n is odd holds
  ex a being non empty positive at_most_one FinSequence of REAL st
  len a = n &
  for f being non empty FinSequence of NAT st
  f = OnlinePacking(a, NextFit(a)) holds
  n = card rng f & n = 2 * Opt a - 1;