:: Dynamic Programming for the Subset Sum Problem
:: by Hiroshi Fujiwara , Hokuto Watari and Hiroaki Yamamoto
::
:: 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;
correctness
coherence
for b1 being FinSequence-like Function st b1 = x | i holds
b1 is D -valued
;
;
end;

registration
let x be real-valued FinSequence;
let i be Nat;
correctness
coherence
for b1 being FinSequence-like Function st b1 = x | i holds
b1 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 b1 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 b1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b1 . (i,s) = FALSE ) )
by LM010;
uniqueness
for b1, b2 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 b1 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b1 . (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 b2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b2 . (i,s) = FALSE ) ) ) holds
b1 = b2
by LM020;
end;

:: deftheorem defQ defines Q_ex PRSUBSET:def 3 :
for x being REAL -valued FinSequence
for b2 being Function of [:(Seg (len x)),REAL:],BOOLEAN holds
( b2 = 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 b2 . (i,s) = TRUE ) & ( not x | i exist_subset_sum_eq s implies b2 . (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' ()
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;