:: Dynamic Programming for the Subset Sum Problem
:: by Hiroshi Fujiwara , Hokuto Watari and Hiroaki Yamamoto
::
:: Received January 13, 2020
:: Copyright (c) 2020-2021 Association of Mizar Users

definition

let x be FinSequence;
let I be set ;

func Seq (x,I) -> FinSequence equals :: PRSUBSET:def 1
Seq (x | I);

coherence
Seq (x | I) is FinSequence ;

end;

:: deftheorem defines Seq PRSUBSET:def 1 :
for x being FinSequence
for I being set holds Seq (x,I) = Seq (x | I);

registration

let D be set ;
let x be D -valued FinSequence;
let I be set ;

cluster Seq (x,I) -> D -valued ;

coherence
Seq (x,I) is D -valued ;

end;

registration

let x be real-valued FinSequence;
let I be set ;

cluster Seq (x,I) -> real-valued ;

coherence
Seq (x,I) is real-valued ;

end;

registration

let D be set ;
let x be D -valued FinSequence;
let i be Nat;

cluster x | i -> D -valued FinSequence-like for FinSequence-like Function;

correctness
coherence
for b₁ being FinSequence-like Function st b₁ = x | i holds
b₁ is D -valued ;
;

end;

registration

let x be real-valued FinSequence;
let i be Nat;

cluster x | i -> FinSequence-like real-valued for FinSequence-like Function;

correctness
coherence
for b₁ being FinSequence-like Function st b₁ = x | i holds
b₁ is real-valued ;
;

end;

definition

let x be REAL -valued FinSequence;
let a be Real;

pred x exist_subset_sum_eq a means :: PRSUBSET:def 2
ex I being set st
( I c= dom x & Sum (Seq (x,I)) = a );

end;

:: deftheorem defines exist_subset_sum_eq PRSUBSET:def 2 :
for x being REAL -valued FinSequence
for a being Real holds
( x exist_subset_sum_eq a iff ex I being set st
( I c= dom x & Sum (Seq (x,I)) = a ) );

LM010: for x being REAL -valued FinSequence ex Q being Function of [:(Seg (len x)),REAL:],BOOLEAN st
for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q . (i,s) = FALSE ) )

proof end;

LM020: for x being REAL -valued FinSequence
for Q1, Q2 being Function of [:(Seg (len x)),REAL:],BOOLEAN st ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q1 . (i,s) = FALSE ) ) ) & ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies Q2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies Q2 . (i,s) = FALSE ) ) ) holds
Q1 = Q2

proof end;

definition

let x be REAL -valued FinSequence;

func Q_ex x -> Function of [:(Seg (len x)),REAL:],BOOLEAN means :defQ: :: PRSUBSET:def 3
for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies it . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies it . (i,s) = FALSE ) );

existence
ex b₁ being Function of [:(Seg (len x)),REAL:],BOOLEAN st
for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies b₁ . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b₁ . (i,s) = FALSE ) ) by LM010;
uniqueness
for b₁, b₂ being Function of [:(Seg (len x)),REAL:],BOOLEAN st ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies b₁ . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b₁ . (i,s) = FALSE ) ) ) & ( for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies b₂ . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b₂ . (i,s) = FALSE ) ) ) holds
b₁ = b₂ by LM020;

end;

:: deftheorem defQ defines Q_ex PRSUBSET:def 3 :
for x being REAL -valued FinSequence
for b₂ being Function of [:(Seg (len x)),REAL:],BOOLEAN holds
( b₂ = Q_ex x iff for i being Nat
for s being Real st 1 <= i & i <= len x holds
( ( x | i exist_subset_sum_eq s implies b₂ . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b₂ . (i,s) = FALSE ) ) );

registration

let A be Subset of NAT;
let i be Nat;
let s be Real;
let f be Function of [:A,REAL:],BOOLEAN;

cluster f . (i,s) -> boolean ;

correctness
coherence
f . (i,s) is boolean ;
;

end;

definition

let a, b be object ;

func a _eq_ b -> object equals :: PRSUBSET:def 4
IFEQ (a,b,TRUE,FALSE);

correctness
coherence
IFEQ (a,b,TRUE,FALSE) is object ;
;

end;

:: deftheorem defines _eq_ PRSUBSET:def 4 :
for a, b being object holds a _eq_ b = IFEQ (a,b,TRUE,FALSE);

registration

let a, b be object ;

cluster a _eq_ b -> boolean ;

correctness
coherence
a _eq_ b is boolean ;
;

end;

definition

let a, b be ExtReal;

func a _le_ b -> object equals :: PRSUBSET:def 5
IFGT (a,b,FALSE,TRUE);

correctness
coherence
IFGT (a,b,FALSE,TRUE) is object ;
;

end;

:: deftheorem defines _le_ PRSUBSET:def 5 :
for a, b being ExtReal holds a _le_ b = IFGT (a,b,FALSE,TRUE);

registration

let a, b be ExtReal;

cluster a _le_ b -> boolean ;

correctness
coherence
a _le_ b is boolean ;
by XXREAL_0:def 11;

end;

Lemacik1: for x being REAL -valued FinSequence st 1 <= len x holds
dom (x | 1) = {1}

proof end;

theorem :: PRSUBSET:1

for s being Real
for x being REAL -valued FinSequence st 1 <= len x holds
(Q_ex x) . (1,s) = ((x . 1) _eq_ s) 'or' (s _eq_ 0)

proof end;

LM040: for i, k, x being Nat
for I being set st I c= Seg k & k < x & x in Seg i holds
Sgm (I \/ {x}) = (Sgm I) ^ <*x*>

proof end;

theorem LM050: :: PRSUBSET:2

for f, g being Function
for X, Y being set st rng g c= X holds
(f | (X \/ Y)) * g = (f | X) * g

proof end;

theorem LM060: :: PRSUBSET:3

for x being REAL -valued FinSequence
for i being Nat
for I0 being set st I0 c= Seg i & Seg (i + 1) c= dom x holds
Seq ((x | (i + 1)),(I0 \/ {(i + 1)})) = (Seq ((x | i),I0)) ^ <*(x . (i + 1))*>

proof end;

theorem LM080: :: PRSUBSET:4

for x being real-valued FinSequence st x <> {} & x is positive holds
0 < Sum x

proof end;

theorem LM090: :: PRSUBSET:5

for x being real-valued FinSequence
for i being Nat st x is positive & 1 <= i & i <= len x holds
( x | i is positive & x | i <> {} )

proof end;

theorem LM100: :: PRSUBSET:6

for x being real-valued FinSequence
for I being set st x is positive & I c= dom x & I <> {} holds
( Seq (x,I) is positive & Seq (x,I) <> {} )

proof end;

:: Recurrence Relation: Induction Case

theorem :: PRSUBSET:7

for x being REAL -valued FinSequence st x is positive holds
for i being Nat
for s being Real st 1 <= i & i < len x holds
(Q_ex x) . ((i + 1),s) = ((Q_ex x) . (i,s)) 'or' (((x . (i + 1)) _le_ s) '&' ((Q_ex x) . (i,(s - (x . (i + 1))))))

proof end;