提交 #19

import Mathlib.Tactic.Lemma

def neighbor_nonequal (xs : List Nat) : Prop :=
  ∀ i < xs.length - 1, xs.getD i 0 ≠ xs.getD (i + 1) 0

def is_local_min (xs : List Nat) (i : Nat) : Prop :=
  i < xs.length ∧
  (i = 0 ∨ xs.getD i 0 < xs.getD (i - 1) 0) ∧
  (i = xs.length - 1 ∨ xs.getD i 0 < xs.getD (i + 1) 0)

inductive local_min : List Nat → Nat → Nat → Nat → Prop
  | case_le_right_left (xs : List Nat) (l r : Nat) (h : r ≤ l) : local_min xs l r l
  | case_left_plus_1_eq_right_l (xs : List Nat) (l r : Nat) (h : l < r) (h₁ : r = l + 1)
      (h₂ : xs.getD l 0 < xs.getD r 0) : local_min xs l r l
  | case_left_plus_1_eq_right_r (xs : List Nat) (l r : Nat) (h : l < r) (h₁ : r = l + 1)
      (h₂ : xs.getD r 0 ≤ xs.getD l 0) : local_min xs l r r
  | case_mid_1 (xs : List Nat) (l r mid i : Nat) (h : l < r) (h₁ : l + 1 ≠ r)
      (h₂ : mid = (l + r) / 2)
      (h₃ : xs.getD (mid - 1) 0 < xs.getD mid 0)
      (h₄ : local_min xs l (mid - 1) i) : local_min xs l r i
  | case_mid_r (xs : List Nat) (l r mid i : Nat) (h : l < r) (h₁ : l + 1 ≠ r)
      (h₂ : mid = (l + r) / 2)
      (h₃ : xs.getD mid 0 ≤ xs.getD (mid - 1) 0)
      (h₄ : local_min xs mid r i) : local_min xs l r i

def is_local_min_part (ls : List Nat) (l r i : Nat) : Prop :=
  i ≥ l ∧ i ≤ r ∧
  (i = 0 ∨ ls.getD i 0 < ls.getD (i - 1) 0) ∧
  (i = ls.length - 1 ∨ ls.getD i 0 < ls.getD (i + 1) 0)

lemma local_min_correct_induct (xs : List Nat) (a b i : Nat)
    (H_neighbor : neighbor_nonequal xs) (H_a_lower : 0 ≤ a)
    (H_ab : a ≤ b) (H_b_upper : b < xs.length)
    (H_a_cond : a = 0 ∨ xs.getD a 0 < xs.getD (a - 1) 0)
    (H_b_cond : b = xs.length - 1 ∨ xs.getD b 0 < xs.getD (b + 1) 0)
    (Hi : local_min xs a b i) : is_local_min_part xs a b i := by
  unfold is_local_min_part
  induction Hi with
  | case_le_right_left l r h =>
    have heq := Nat.le_antisymm H_ab h
    subst l
    exact ⟨H_ab, H_ab, H_a_cond, H_b_cond⟩
  | case_left_plus_1_eq_right_l l r h h₁ h₂ =>
    refine ⟨Nat.le_refl l, H_ab, H_a_cond, Or.inr ?_⟩
    rw [← h₁]
    exact h₂
  | case_left_plus_1_eq_right_r l r h h₁ h₂ =>
    refine ⟨H_ab, Nat.le_refl r, Or.inr ?_, H_b_cond⟩
    conv => rhs; rw [h₁, Nat.add_sub_cancel]
    exact Nat.lt_of_le_of_ne h₂ <| h₁ ▸ (H_neighbor l (by omega)).symm
  | case_mid_1 l r mid i h h₁ h₂ h₃ h₄ ih =>
    have ⟨il, ir, il', ir'⟩ := ih H_a_lower (by omega) (by omega) H_a_cond (Or.inr ?_)
    refine ⟨il, ?_, il', ir'⟩
    · omega
    · rw [Nat.sub_add_cancel]
      exact h₃
      omega
  | case_mid_r l r mid i h h₁ h₂ h₃ h₄ ih =>
    have ⟨il, ir, il', ir'⟩ := ih (Nat.zero_le mid) (by omega) H_b_upper (Or.inr ?_) H_b_cond
    refine ⟨?_, ir, il', ir'⟩
    · omega
    · refine Nat.lt_of_le_of_ne h₃ ?_
      have hn := (H_neighbor (mid - 1) (by omega)).symm
      rw [Nat.sub_add_cancel] at hn
      exact hn
      omega

theorem local_min_correct (xs : List Nat) (i : Nat)
  (Hn : neighbor_nonequal xs) (Hlen : xs.length > 0)
  (Hmin : local_min xs 0 (xs.length - 1) i) : is_local_min xs i := by
  have ⟨_, ib, il, ir⟩ := local_min_correct_induct xs 0 (xs.length - 1) i Hn
    (Nat.le_refl 0) (Nat.zero_le _) (Nat.pred_lt <| Nat.ne_zero_of_lt Hlen)
    (Or.inl rfl) (Or.inl rfl) Hmin
  exact ⟨Nat.lt_of_le_pred Hlen ib, il, ir⟩

#print axioms local_min_correct