提交 #20

import Mathlib.Data.Nat.Notation
import Mathlib.Tactic.Lemma

variable (C N : ℕ) (posN : N > 0) (caps vals : ℕ → ℕ)

def clear (s : Nat → Option Bool) (i : Nat) : Nat → Option Bool :=
  fun j => if j = i then none else s j

def val_in_knapsack (s : Nat → Option Bool) (n : Nat) (c_rem : Nat) : Option Nat :=
  match n with
  | 0 => some 0
  | n' + 1 =>
    let s' := clear s n
    match s n with
    | some true =>
      if caps n ≤ c_rem then
        match val_in_knapsack s' n' (c_rem - caps n) with
        | some v => some (v + vals n)
        | _ => none
      else
        none
    | some false =>
        val_in_knapsack s' n' c_rem
    | none => none

def wf (s : Nat → Option Bool) (n : Nat) : Prop :=
  ∀ i, (s i ≠ none ↔ 1 ≤ i ∧ i ≤ n)

def opt_s (s : Nat → Option Bool) (n c_rem : Nat) : Prop :=
  wf s n ∧
  ∀ (s' : Nat → Option Bool) (v₁ v₂ : Nat),
    wf s' n →
    val_in_knapsack caps vals s' n c_rem = some v₁ →
    val_in_knapsack caps vals s  n c_rem = some v₂ →
      v₁ ≤ v₂

lemma wf_clr (s : ℕ → Option Bool) (n : ℕ) (Hlt : 1 ≤ n ∧ n ≤ N) (Hwf : wf s n) : wf (clear s n) (n - 1) := by
  intro i
  unfold clear
  simp
  refine ⟨λ h ↦ ?_, λ h ↦ ?_⟩
  · have e := (Hwf i).1 h.2
    omega
  · refine ⟨?_, (Hwf i).2 ?_⟩ <;> omega

def set_s (s : ℕ → Option Bool) (i : ℕ) (b : Bool) : ℕ → Option Bool :=
  fun j => if j = i then some b else s j

lemma wf_set_s (s : ℕ → Option Bool) (n : ℕ) (b : Bool) (Hge : 1 ≤ n) (Hwf : wf s (n - 1)) : wf (set_s s n b) n := by
  intro oi
  unfold set_s
  refine ⟨λ h ↦ ?_, λ h ↦ ?_⟩
  · split at h
    · next hn => simp [hn, Hge]
    · next hn =>
      have e := (Hwf oi).1 h
      omega
  · split
    · simp
    · next hn => exact (Hwf oi).2 (by omega)

lemma clr_set (s : ℕ → Option Bool) (n : ℕ) (Hn : s n = none) : clear (fun j => if j = n then some true else s j) n = s := by
  ext1 i
  unfold clear
  simp
  split
  · next h => exact h ▸ Hn.symm
  · rfl

theorem optimal_substructure (s : ℕ → Option Bool) (n c_rem : ℕ)
  (Hrgn : 1 ≤ n ∧ n ≤ N) (Htt : s n = some true) (Hrem : caps n ≤ c_rem)
  (Hopt : opt_s caps vals s n c_rem) : opt_s caps vals (clear s n) (n - 1) (c_rem - caps n) := by
  refine ⟨wf_clr N s n Hrgn Hopt.1, λ s' v₁ v₂ wf' hs' hs ↦ ?_⟩
  let s₁ j := if j = n then some true else s' j
  have s₁clear : clear s₁ n = s' := clr_set s' n (Decidable.byContradiction <| mt (wf' n).1 (by omega))
  have wf₁ : wf s₁ n := wf_set_s s' n true Hrgn.1 wf'
  refine Nat.le_of_add_le_add_right (b := vals n) <| Hopt.2 s₁ (v₁ + vals n) (v₂ + vals n) wf₁ ?_ ?_
  · rw [← n.succ_pred (by omega)]
    unfold val_in_knapsack
    simp only
    have k₁ : s₁ n = some true := by simp [s₁]
    rw [n.succ_pred (by omega)]
    simp only [k₁, Hrem, reduceIte, s₁clear, Nat.pred_eq_sub_one, hs']
  · rw [← n.succ_pred (by omega)]
    unfold val_in_knapsack
    simp only
    rw [n.succ_pred (by omega)]
    simp only [Htt, Hrem, reduceIte, Nat.pred_eq_sub_one, hs]

#print axioms optimal_substructure