提交 #6

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Tactic

def neighbor_nonequal (xs : List Nat) : Bool :=
  ∀ i, 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)

lemma ge_exists (right left : ℕ) (g : right > left) (n : left + 1 ≠ right) :
    ∃ n0 : ℕ, right = n0 + left ∧ n0 > 1 := by
  induction right generalizing left with
  | zero =>
    exfalso; linarith [g]
  | succ k IH =>
    rcases left with (_ | m)
    · refine ⟨k + 1, ?_, by omega⟩
      omega
    · have g' : k > m := by omega
      have n' : m + 1 ≠ k := by
        intro h
        apply n
        omega
      rcases IH m g' n' with ⟨k', hk1, hk2⟩
      refine ⟨k', ?_, hk2⟩
      omega

lemma div2_plus_2 : ∀ k, (k + 2) / 2 = k / 2 + 1 := by
  intros k
  simp

lemma div2_plus_2n : ∀ n k,  (k + (n + n)) / 2 =  k / 2 + n := by
  intro n
  omega

lemma div2_le : ∀ n k, n ≤ k → n / 2 ≤ k /2 := by
  intro n k h
  omega

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) (h1 : r = l + 1)
      (h2 : 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) (h1 : r = l + 1)
      (h2 : 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) (h1 : l + 1 ≠ r) (h2 : mid = (l + r) / 2)
      (h3 : xs.getD (mid - 1) 0 < xs.getD mid 0)
      (h4 : 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) (h1 : l + 1 ≠ r) (h2 : mid = (l + r) / 2)
      (h3 : xs.getD mid 0 ≤ xs.getD (mid - 1) 0)
      (h4 : 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 ∨ (i < ls.length ∧ (i - 1) < ls.length ∧ ls.getD i 0 < ls.getD (i - 1) 0)) ∧
  (i = ls.length - 1 ∨ (i < ls.length ∧ (i + 1) < ls.length ∧ 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 ∨ (a < xs.length ∧ (a - 1) < xs.length ∧ xs.getD a 0 < xs.getD (a - 1) 0))
    (H_b_cond : b = xs.length - 1 ∨
            (b < xs.length ∧ (b + 1) < xs.length ∧ 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 : l = r := by omega
    subst l
    omega

  | case_left_plus_1_eq_right_l l r h h1 h2 =>
    subst r
    constructor <;> try omega
  | case_left_plus_1_eq_right_r l r H H1 H2 =>
    subst r
    constructor <;> try omega
    constructor <;> try omega
    constructor
    · rcases H_a_cond with (hb | hb)
      · subst hb
        right
        constructor <;> try omega
        constructor <;> try omega
        unfold neighbor_nonequal at H_neighbor
        simp at *
        have hc: 0 < xs.length - 1 := by omega
        specialize (H_neighbor 0 hc)
        apply Nat.eq_or_lt_of_le at H2
        rcases H2 with (H2 | H2)
        · exfalso
          apply H_neighbor
          simp
          omega
        · omega
      · rcases hb with ⟨hb, hc, hd⟩
        right
        constructor <;> try omega
        constructor <;> try omega
        unfold neighbor_nonequal at H_neighbor
        simp at *
        have hh: l < xs.length - 1 := by omega
        specialize (H_neighbor l hh)
        apply Nat.eq_or_lt_of_le at H2
        rcases H2 with (H2 | H2)
        · exfalso
          apply H_neighbor
          omega
        · omega
    · omega
  | case_mid_1 l r mid i H H1 H2 H3 H4 H4_ih =>
    subst mid
    specialize (H4_ih H_a_lower)
    have Heq: l ≤ (l + r) / 2 - 1 := by omega
    specialize (H4_ih Heq); clear Heq
    have Heq: (l + r) / 2 - 1 < xs.length := by omega
    specialize (H4_ih Heq); clear Heq
    have Heq:  l = 0 ∨ l < xs.length ∧
      l - 1 < xs.length ∧ xs.getD l 0 < xs.getD (l - 1) 0  := by omega
    specialize (H4_ih Heq); clear Heq
    have Heq: (l + r) / 2 - 1 = xs.length - 1 ∨
      (l + r) / 2 - 1 < xs.length ∧ (l + r) / 2 - 1 + 1 < xs.length ∧
      xs.getD ((l + r) / 2 - 1) 0 < xs.getD ((l + r) / 2 - 1 + 1) 0 := by
      rcases H_b_cond with (Hb | Hb)
      · rcases ge_exists r l H H1 with ⟨k, hk1, hk2⟩
        have Heq: (l + r) / 2 - 1 = xs.length - 1 ∨ ¬ (l + r) / 2 - 1 = xs.length - 1 := by omega
        subst hk1
        rw [show l + (k + l) = k + (l + l) by omega] at *
        rw [div2_plus_2n] at *
        rcases Heq with (Heq | Heq)
        · omega
        · right
          constructor ; try omega
          constructor ; try omega
          have He: k / 2 + l - 1 + 1 = k / 2 + l := by omega
          rw [He]
          omega
      · rcases ge_exists r l H H1 with ⟨k, hk1, hk2⟩
        have Heq: (l + r) / 2 - 1 = xs.length - 1 ∨ ¬ (l + r) / 2 - 1 = xs.length - 1 := by omega
        subst hk1
        rw [show l + (k + l) = k + (l + l) by omega] at *
        rw [div2_plus_2n] at *
        rcases Heq with (Heq | Heq)
        · omega
        · right
          constructor ; try omega
          constructor ; try omega
          have He: k / 2 + l - 1 + 1 = k / 2 + l := by omega
          rw [He]
          omega
    specialize (H4_ih Heq); clear Heq
    rcases H4_ih with ⟨H5, H6, H7⟩
    constructor ; try omega
    omega

  | case_mid_r l r mid res H H1 H2 H3 H4 H4_ih =>
    subst mid
    have Heq:  0 ≤ (l + r) / 2 := by omega
    specialize (H4_ih Heq); clear Heq
    have Heq: (l + r) / 2 ≤ r := by omega
    specialize (H4_ih Heq); clear Heq
    have Heq: r < xs.length := by omega
    specialize (H4_ih Heq); clear Heq
    have Heq: (l + r) / 2 = 0 ∨
      (l + r) / 2 < xs.length ∧ (l + r) / 2 - 1 < xs.length ∧
        xs.getD ((l + r) / 2) 0 < xs.getD ((l + r) / 2 - 1) 0 := by
      clear H4_ih H4
      rcases H_a_cond with (Ha | Ha)
      · rcases ge_exists r l H H1 with ⟨k, hk1, hk2⟩
        have Hn : (l + r) / 2 = 0 ∨ ∃ t, (l + r) / 2 = (t+1) := by
          rcases (l + r) / 2 with (_ | t)
          · omega
          · right
            exists t

        rcases Hn with (Hn | ⟨t, Hn⟩)
        · omega
        · right
          subst hk1
          rw [show l + (k + l) = k + (l + l) by omega] at *
          rw [div2_plus_2n] at *
          constructor ; try omega
          constructor ; try omega

          unfold neighbor_nonequal at H_neighbor
          simp at *
          have hh: k / 2 + l - 1 < xs.length - 1 := by omega
          specialize (H_neighbor _ hh)
          apply Nat.eq_or_lt_of_le at H3
          rcases H3 with (H3 | H3)
          · exfalso
            apply H_neighbor
            have He: k / 2 + l - 1 + 1 = k / 2 + l := by omega
            rw [He]
            omega
          · omega
      · rcases ge_exists r l H H1 with ⟨k, hk1, hk2⟩
        have Hn : (l + r) / 2 = 0 ∨ ∃ t, (l + r) / 2 = (t+1) := by
          rcases (l + r) / 2 with (_ | t)
          · omega
          · right
            exists t

        rcases Hn with (Hn | ⟨t, Hn⟩)
        · omega
        · right
          subst hk1
          rw [show l + (k + l) = k + (l + l) by omega] at *
          rw [div2_plus_2n] at *
          constructor ; try omega
          constructor ; try omega

          unfold neighbor_nonequal at H_neighbor
          simp at *
          have hh: k / 2 + l - 1 < xs.length - 1 := by omega
          specialize (H_neighbor _ hh)
          apply Nat.eq_or_lt_of_le at H3
          rcases H3 with (H3 | H3)
          · exfalso
            apply H_neighbor
            have He: k / 2 + l - 1 + 1 = k / 2 + l := by omega
            rw [He]
            omega
          · omega
    specialize (H4_ih Heq H_b_cond); clear Heq
    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 Heq: is_local_min_part xs 0 (xs.length - 1) i := by
    apply local_min_correct_induct at Hmin
    · omega
    · omega
    · omega
    · omega
    · omega
    · omega
    · omega
  unfold is_local_min_part at Heq
  unfold is_local_min
  rcases Heq with ⟨h1, h2, h3, h4⟩
  constructor <;> try omega