提交 #7

import Mathlib.Data.Real.Basic

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

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

def val_in_knapsack (s : ℕ → Option Bool) (n : ℕ) (c_rem : ℕ) : Option ℕ :=
  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 : ℕ → Option Bool) (n : ℕ) : Prop :=
  ∀ i, (s i ≠ none ↔ 1 ≤ i ∧ i ≤ n)

def opt_s (s : ℕ → Option Bool) (n c_rem : ℕ) : Prop :=
  wf s n ∧
  ∀ (s' : ℕ → Option Bool) (v1 v2 : ℕ),
    wf s' n →
    val_in_knapsack caps vals  s' n c_rem = some v1 →
    val_in_knapsack caps vals  s n c_rem = some v2 →
      v1 ≤ v2

lemma wf_clr (s : ℕ → Option Bool) (n : ℕ)
    (Hlt : 1 ≤ n ∧ n ≤ N) (Hwf : wf s n) : wf (clear s n) (n - 1) :=
by
  unfold wf clear at *
  intro i
  constructor
  · intro H
    simp at H
    by_cases h : i = n
    · simp [h] at H
    · simp [h] at H ⊢
      have := (Hwf i).mp H
      omega
  · intro ⟨hi1, hi2⟩ H
    by_cases h: i= n
    · omega
    · simp at H
      have hi : s i = none := (H h)
      have hwf_i : 1 ≤ i ∧ i ≤ n → s i ≠ none := (Hwf i).mpr
      apply hwf_i
      · omega
      · 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
  unfold wf at Hwf ⊢
  intro i
  have Hwf_i := Hwf i
  constructor
  · intro Hs
    unfold set_s at Hs
    by_cases h : i = n
    · omega
    · simp [h] at Hs
      have ⟨left_implication, _⟩ := Hwf_i
      have H := left_implication Hs
      constructor <;> omega
  · intro ⟨hi1, hi2⟩
    unfold set_s
    by_cases h : i = n
    · simp [h]
    · simp [h]
      have ⟨_, right_implication⟩ := Hwf_i
      have : i ≤ n - 1 := by
        have : i < n := by omega
        omega
      exact right_implication ⟨hi1, 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
  unfold clear
  apply funext
  intro x
  by_cases h : x = n
  · subst x
    simp [Hn]
  · simp [h]

-- #check opt_s
-- #check opt_s
-- #check wf_clr
-- #check Nat.exists_eq_succ_of_ne_zero
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
  unfold opt_s at Hopt ⊢
  rcases Hopt with ⟨Hwf, Ha⟩
  constructor
  · exact wf_clr N s n Hrgn Hwf
  · intro s' v1 v2 Hwf' Hval1 Hval2
    have h : v1 ≤ v2 ∨ v1 > v2 := by omega
    rcases h with (h | h)
    · exact h
    · exfalso
      have Hnone : s' n = none := by
        by_cases h' : s' n ≠ none
        · have ⟨hn1, hn2⟩ := (Hwf' n).mp h'
          omega
        · push_neg at h'
          exact h'

      unfold wf at Hwf
      rcases Nat.exists_eq_succ_of_ne_zero (by omega : n ≠ 0) with ⟨n', rfl⟩
      have h1_eq: n'.succ = n'+1 := by omega
      have h2_eq: n'.succ - 1 = n' := by omega
      rw [h2_eq] at Hwf' Hval1
      have Hv1 : val_in_knapsack caps vals (set_s s' (n'+1) true) (n'+1) c_rem =
        some (v1 + vals (n'+1)) := by
        simp [val_in_knapsack, set_s]
        have Hle: caps (n' + 1) ≤ c_rem := by omega
        unfold set_s
        rw [clr_set]
        · rw [h1_eq] at Hval1
          rw [Hval1]
          simp
          assumption
        · omega

      have Hv2 : val_in_knapsack caps vals s (n'+1) c_rem = some (v2 + vals (n'+1)) := by
        simp [val_in_knapsack]
        rw [← h1_eq, Htt]
        simp
        rw [← h1_eq]
        rw [h2_eq] at Hval2
        rw [Hval2]
        simp
        omega

      have Heq : wf (set_s s' (n' + 1) true) (n' + 1) :=
      by
        apply wf_set_s
        · omega
        · rw [← h1_eq, h2_eq]
          assumption

      have K := Ha (set_s s' (n' + 1) true) (v1 + vals (n' + 1)) (v2 + vals (n' + 1)) Heq Hv1 Hv2
      -- K and h are conflict
      omega
end ProblemB