has_duplicate.lean

open list
open nat

def duplicate {α:Type} (l:list α) (i:ℕ)(il:i<l.length) (j:ℕ)(jl:j<l.length) : Prop := i ≠ j ∧ (nth_le l i il = nth_le l j jl)
def has_duplicate {α:Type} (l:list α) : Prop := ∃(i:ℕ)(il:i<l.length) (j:ℕ)(jl:j<l.length), duplicate l i il j jl

lemma mem_nth {α:Type} (a:α) (l:list α) : a ∈ l ↔ ∃(i:ℕ)(il:i<l.length), (a = nth_le l i il) :=
begin
  induction l with hd tl ih,
  simp, intro e,
  cases e with i e,
  cases e with il e,
  simp at il,
  exact (not_lt_zero i il),

  split,
  intro aht,
  cases aht with ahd atl,

  -- ahd case
  existsi 0,
  have il : 0 < length (hd :: tl),
  rw length_cons,
  exact zero_lt_succ (length tl),
  existsi il,
  simp,
  exact ahd,

  -- atl case
  cases ih,
  have te := ih_mp atl,
  cases te with ti te,
  cases te with til te,
  existsi ti.succ,
  have il : succ ti < length (hd :: tl),
  rw length_cons,
  exact succ_le_succ til,
  existsi il,
  simp,
  exact te,

  -- other direction
  intro e,
  cases e with i e,
  cases e with il e,
  cases i,
  simp,
  simp at e,
  exact or.inl e,

  simp at e,
  simp,
  cases ih,
  suffices k : ∃ (i : ℕ) (il : i < length tl), a = nth_le tl i il, from or.inr (ih_mpr k),
  existsi i,
  existsi (le_of_succ_le_succ il),
  exact e,
end


instance dec_duplicate {α:Type} [decidable_eq α] (l:list α) : decidable (has_duplicate l) :=
begin
  induction l with hd tl ih,

  -- Empty list case: there is no duplicate because i cannot even exist.
  suffices f : ¬ has_duplicate nil, from is_false f,
  intro p,
  cases p with i p,
  cases p with il p,
  cases p with j p,
  cases p with jl p,
  simp at il,
  exact not_lt_zero i il,

  -- TODO: recursive case:
  --   1. If head ∈ tail, there's a duplicate.
  --   2. Otherwise, decide if there's a duplicate in the tail.
  --     a. If not, show that head ∉ tail means the full list has no duplicate either.
  --     b. If there is, show it is also in this list.

  by_cases m : hd ∈ tl,

  -- Case 1
  suffices f : has_duplicate (hd :: tl), from is_true f,
  have m := iff.mp (mem_nth hd tl) m,
  cases m with mi m,
  cases m with mil m,
  existsi 0,
  have il : 0 < length (hd :: tl),
  simp, exact zero_lt_succ (length tl),
  existsi il,
  existsi mi.succ,
  have jl : succ mi < length (hd :: tl),
  simp,
  apply succ_le_succ,
  exact mil,
  existsi jl,

  -- Show there's a duplicate:
  split,
  intro equ,
  have uqe := eq.symm equ,
  exact (succ_ne_zero mi uqe),
  simp,
  exact m,

  -- Case 2
  cases ih,

  -- Case 2a
  suffices f : ¬ has_duplicate (hd :: tl), from is_false f,
  intro d,
  cases d with i d,
  cases d with il d,
  cases d with j d,
  cases d with jl d,
  cases d with i_neq_j nth_eq,


  cases i,
  cases j,
  -- (i,j) = (0,0) is impossible because i_neq_j.
  exact (i_neq_j nat_zero_eq_zero),

  -- (i,j) = (0,+) is impossible because then hd ∈ tl, in contradiction with m : hd ∉ tl.
  simp at nth_eq,
  have nth_ex : ∃(z:ℕ)(zl:z<tl.length), (hd = nth_le tl z zl),
  existsi j,
  existsi (le_of_succ_le_succ jl),
  exact nth_eq,
  have me := iff.mpr (mem_nth hd tl) nth_ex,
  exact m me,

  cases j,
  -- (i,j) = (+,0) is impossible for the same reason.
  simp at nth_eq,
  have nth_ex : ∃(z:ℕ)(zl:z<tl.length), (hd = nth_le tl z zl),
  existsi i,
  existsi (le_of_succ_le_succ il),
  apply eq.symm,
  exact nth_eq,
  have me := iff.mpr (mem_nth hd tl) nth_ex,
  exact m me,

  -- (i,j) = (+,+) is impossible because this means a duplicate in the tail, in contradiction with ih.
  simp at nth_eq,
  have d : has_duplicate tl,
  existsi i,
  existsi (le_of_succ_le_succ il),
  existsi j,
  existsi (le_of_succ_le_succ jl),
  split,
  intro iej,
  rw iej at i_neq_j,
  exact i_neq_j rfl,
  exact nth_eq,
  exact absurd d ih,

  -- Case 2b
  suffices f : has_duplicate (hd :: tl), from is_true f,
  cases ih with i ih,
  cases ih with il ih,
  cases ih with j ih,
  cases ih with jl ih,

  -- Claim there's a duplicate at (i+1,j+1) in hd::tl.
  existsi succ i,
  have eil : succ i < length (hd :: tl),
    rw length_cons,
    apply succ_le_succ,
    exact il,
  existsi eil,
  existsi succ j,
  have ejl : succ j < length (hd :: tl),
    rw length_cons,
    apply succ_le_succ,
    exact jl,
  existsi ejl,

  -- Show it's a duplicate:
  cases ih with i_neq_j nth_eq,
  split,
  simp,
  exact i_neq_j,
  simp,
  exact nth_eq,
end