mergesort.lean

namespace X  -- to avoid clashes with the stdlib List

-- Define our own List type
inductive List (α : Type u)
| nil : List α
| cons : α → List α → List α

infixr:70 " :: " => List.cons

open List

def append : List α → List α → List α
| nil, ys => ys
| x :: xs, ys => x :: append xs ys

-- TODO: idk what the precedence should be but ok
infix:60 " ++ " => append

-- Let's prove that xs ++ nil = xs
@[simp]
theorem append_nil (xs : List α) : xs ++ nil = xs :=
  match xs with
  | nil => by
      simp [append]
  | x :: xs => by
      simp [append]
      rw [append_nil xs]
      -- Q: huh, why can append_nil refer to itself?
      -- ok, Lean shows termination somehow, because this doesn't work:
      --
      --   theorem append_nil_bad (xs : List α) : xs ++ nil = xs :=
      --     append_nil_bad xs

theorem nil_not_append_cons {x : α} {xs : List α} :
  nil ≠ x :: xs := by
  intro h
  cases h

theorem nil_append_iff {xs ys : List α} :
  xs ++ ys = nil ↔ xs = nil ∧ ys = nil := by

  apply Iff.intro
  . intro
    cases xs with  -- TODO: how to apply `trivial` to both cases? 
                   -- (later update: I know about `all_goals` now but maybe there's a better way)
    | nil => trivial
    | cons x xs => trivial
  . intro
    cases xs with
    | nil =>
        cases ys with
        | nil => trivial
        | cons y ys => simp [append] at *
    | cons x xs => simp [append] at *

-- Now let's define `reverse`
def reverse : List α → List α
| nil => nil
| x :: xs => reverse xs ++ (x :: nil)

@[simp]
theorem reverse_nil : reverse (nil : List α) = nil := by
  simp [reverse]

-- Prove that reverse (xs ++ [x]) = x :: reverse xs
theorem reverse_snoc (xs : List α) (x : α) :
  reverse (xs ++ x :: nil) = x :: reverse xs :=

  match xs with
  | nil => by
      simp [append, reverse]
  | y :: ys => by
      simp [reverse]
      rw [reverse_snoc ys x]
      simp [append]

-- Prove that reverse (reverse xs) = xs
@[simp]
theorem reverse_reverse (xs : List α) :
  reverse (reverse xs) = xs :=

  match xs with
  | nil => by simp
  | x :: xs => by
      simp [reverse]
      rw [reverse_snoc, reverse_reverse xs]

-- Define list length
def length : List α → Nat
| nil => 0
| _ :: xs => 1 + length xs

@[simp]
theorem length_nil : length (nil : List α) = 0 := by
  simp [length]

theorem length_nil_mpr {xs : List α} : length xs = 0 → xs = nil := by
  intro h
  cases xs with
  | nil => rfl
  | cons x xs => simp [length] at h  -- TODO: how does this work?

@[simp]
theorem length_cons (x : α) (xs : List α) :
  length (x :: xs) = 1 + length xs := by
  simp [length]

-- TODO: can I just add @[simp] to `length` directly? or is it a bad idea

-- Prove that length (xs ++ ys) = length xs + length ys
theorem length_append (xs ys : List α) :
  length (xs ++ ys) = length xs + length ys :=

  match xs with
  | nil => by
      simp [append]
  | x :: xs => by
      simp!       -- simp + applying definitions
      rw [length_append xs ys]
      simp_arith  -- TODO: why doesn't normal `simp` include this?

-- Prove that length (reverse xs) = length xs
@[simp]
theorem length_reverse (xs : List α) :
  length (reverse xs) = length xs :=

  match xs with
  | nil => by
      simp [length_nil]
  | x :: xs => by
      simp!
      rw [length_append, length_reverse xs]
      simp!; simp_arith

-- Define "is permutation of"
def is_permutation : List α → List α → Prop
| nil, nil => True
| nil, _ => False
| x :: xs, ys =>
    -- Exists yl,yr such that: ys = yl++[x]++yr
    ∃ yl yr,
      ys = yl ++ x :: yr   -- TODO: how come everything is eq-able in Lean? ok maybe it's something about definitional equality idk
      ∧
      is_permutation xs (yl ++ yr)

-- Prove that xs is a permutation of itself
theorem is_permutation_refl (xs : List α) :
  is_permutation xs xs :=

  match xs with
  | nil => by
      simp!
  | x :: xs => by
      simp!
      exists nil, xs
      simp!
      exact is_permutation_refl xs

-- Prove that reversing a list doesn't change its elements
theorem is_permutation_reverse (xs : List α) :
  is_permutation xs (reverse xs) :=

  match xs with
  | nil => by
      simp!
  | x :: xs => by
      rw [is_permutation]
      exists reverse xs, nil
      simp! [append_nil]
      exact is_permutation_reverse xs

theorem permutation_pair {a b ap bp : List α} :
  is_permutation a ap → is_permutation b bp →
  is_permutation (a ++ b) (ap ++ bp) :=

  sorry

@[simp]
theorem nil_append (xs : List α) : nil ++ xs = xs := by
  simp [append]

-- Define list membership
-- (also see https://github.com/leanprover/lean4/blob/ffac974dba799956a97d63ffcb13a774f700149c/src/Init/Data/List/Basic.lean#L709-L710)
def mem (a : α) : List α → Prop
| nil => False
| x :: xs => x = a ∨ mem a xs

instance : Membership α (List α) where
  mem l a := mem a l

-- Prove that no element is in the empty list
theorem not_in_nil (x : α) : x ∉ nil := by
  intro h
  cases h  -- TODO: why did this work??

-- An element is surely in a list if it's literally the head
theorem in_cons {x : α} {xs : List α} :
  x ∈ x :: xs := by
  simp [Membership.mem, mem]

-- Prove that an element is *either* in a cons or in the tail
theorem mem_elim_cons {x head : α} {tail : List α} :
  x ∈ head :: tail ↔ x = head ∨ x ∈ tail := by

  apply Iff.intro
  . intro h
    cases h
    . left; symm; assumption
    . right; assumption
  . intro h
    simp [Membership.mem, mem]
    rw [Eq.comm]
    assumption

-- Prove that if an element is in a list, it's still there no matter what you prepend
theorem mem_after_prepend {x : α} {init xs : List α} :
  x ∈ xs → x ∈ init ++ xs := by

  intro in_xs
  cases init
  case nil => simp!; exact in_xs
  case cons x' xs' =>
    simp [append]
    by_cases h : x' = x  -- Assume they're equal; then assume they aren't
    -- I'm told that simp! doesn't work because expanding stuff is not
    -- necessarily simpler, ok then
    . rw [h]; simp [Membership.mem, mem]
    . simp [Membership.mem, mem]; right
      have := mem_after_prepend (init := xs') in_xs  -- := gives a named arg here
      simp [Membership.mem, mem] at this
      assumption
      -- TODO: I don't like that I have to manually shift between mem <-> ∈

theorem mem_after_append {x : α} {xs tail : List α} :
  x ∈ xs → x ∈ xs ++ tail := by

  intro in_xs
  induction xs with
    | nil =>
        exfalso; exact not_in_nil x in_xs
    | cons x' xs' ih =>
        cases in_xs
        . left; assumption
        . right; apply ih; assumption

theorem in_append_elim_mp {x : α} {as bs : List α} :
  x ∈ as ++ bs →
  x ∈ as ∨ x ∈ bs := by

  intro in_asbs
  by_cases h : x ∈ as
  . left; assumption
  . right
    induction as with
      | nil => simp! at in_asbs; assumption
      | cons a as ih =>
          have neq : x ≠ a := by
            intro h'
            rw [h'] at h
            exact h in_cons
          apply ih
          . rw [append] at in_asbs
            rw [mem_elim_cons] at in_asbs
            cases in_asbs with  -- TODO: there has to be a shorter way
              | inl h' => contradiction
              | inr h' => assumption
          . false_or_by_contra
            rename_i x_in_as
            apply h
            rw [mem_elim_cons]
            right; assumption

theorem in_append_elim_mpr {x : α} {as bs : List α} :
  x ∈ as ∨ x ∈ bs →
  x ∈ as ++ bs := by

  intro in_as_or_bs
  cases in_as_or_bs with
    | inl in_as => apply mem_after_append; assumption
    | inr in_bs => apply mem_after_prepend; assumption

-- If an element is in (as ++ bs), it's either in as or in bs
theorem in_append_elim {x : α} {as bs : List α} :
  x ∈ as ++ bs ↔
  x ∈ as ∨ x ∈ bs :=
  Iff.intro in_append_elim_mp in_append_elim_mpr

theorem in_append_cons {x : α} {as bs : List α} :
  x ∈ as ++ x :: bs := by

  apply mem_after_prepend
  apply in_cons

-- Prove that if an element is in a list, it's also in its permutation
theorem in_permutation {x : α} {xs ys : List α} :  -- TODO: why { } ?
  x ∈ xs → is_permutation xs ys → x ∈ ys := by

  intro in_xs is_perm

  -- TODO: what's the proper way to match by cases of is_perm?
  rw [is_permutation.eq_def] at is_perm
  cases xs
  case nil =>
    false_or_by_contra
    exact not_in_nil x in_xs
  -- TODO: is there a more idiomatic way to eliminate the boring case and keep going?
  case cons x' xs' =>
    simp! at is_perm
    by_cases h : x' = x
    . rw [h] at in_xs is_perm; clear h x'
      obtain ⟨yl, yr, is_perm⟩ := is_perm  -- deconstructing the exists
      rw [is_perm.left]; clear is_perm
      apply mem_after_prepend; exact in_cons
    . -- TODO: how can I convert `mem x xs'` to `x ∈ xs'`?  I never want to see `mem` really
      obtain ⟨yl, yr, is_perm⟩ := is_perm
      have in_ys := in_permutation (x := x) (xs := xs') (ys := yl ++ yr)
      have in_xs' : x ∈ xs' := by
        -- ^ this introduced a new sub-goal that I will be proving now
        -- (TODO: how to split `in_ys` in one go and prove the -> requirement?)
        cases mem_elim_cons.mp in_xs
        case inl eq => symm at eq; contradiction
        case inr => assumption
      specialize in_ys in_xs' is_perm.right -- ! This applies an implication (`in_ys`) to some known facts
      rw [is_perm.left]; clear is_perm in_xs' in_xs xs' ys

      rw [in_append_elim]
      cases in_append_elim_mp in_ys
      . left; assumption
      . right; rw [mem_elim_cons]; right; assumption

-- I didn't install mathlib so I'll define my own orders
structure Order (α : Type u) (leq : α → α → Bool) where
  trans : ∀ x y z, leq x y → leq y z → leq x z
  -- TODO: idk how to work with `¬`
  not : ∀ x y, leq x y = false → leq y x = true

-- A merging function on sorted lists
def merge (ord : Order α leq) (xs : List α) (ys : List α) : List α :=
  match _hxs : xs, _hys : ys with
  | nil, _ => ys
  | _, nil => xs
  | x :: xs', y :: ys' =>
      if leq x y then x :: merge ord xs' ys else y :: merge ord xs ys'

  -- I claim this decreases
  termination_by length xs + length ys

  -- And here I will prove it
  decreasing_by
  . rw [_hys]; simp
  . rw [_hxs]; simp

-- #eval merge (· ≤ ·) (1 :: 3 :: 5 :: nil) (2 :: 4 :: 6 :: nil)

-- A function to split a list in halves
def split : List α → List α × List α
  | nil => (nil, nil)
  | x :: nil => (x :: nil, nil)
  | x :: y :: s =>
      let (s1, s2) := split s
      (x :: s1, y :: s2)

theorem split_not_longer (s : List α) :
  let (s1, s2) := split s
  length s1 ≤ length s ∧ length s2 ≤ length s := by

  match s with
  | nil =>
      simp [split]
  | x :: nil =>
      simp [split]
  | x :: y :: s =>
      simp [split]
      have := split_not_longer s
      simp [split] at this
      apply And.intro
      . apply Nat.le_trans
        apply this.left
        simp
      . apply Nat.le_trans
        apply this.right
        simp

theorem split_permutes (s : List α) :
  is_permutation s (let (s1, s2) := split s; s1 ++ s2) := by

  match s with
  | nil =>
      simp [split]
      exact is_permutation_refl nil
  | x :: nil =>
      simp [split]
      exact is_permutation_refl (x :: nil)
  | x :: y :: s =>
      simp [split]
      rw [is_permutation]
      exists nil, (split s).fst ++ y :: (split s).snd
      simp
      apply And.intro rfl
      rw [is_permutation]
      exists (split s).fst, (split s).snd
      exact And.intro rfl (split_permutes s)

-- Merge sort!
def merge_sort (ord : Order α leq) (as : List α) : List α :=
  match _h : as with
  | nil => nil
  | x :: nil => x :: nil
  | x :: y :: s =>
      -- TODO: how to create a hypothesis for the split?
      match _hsplit : split s with
      | (s1, s2) =>
        merge ord (merge_sort ord (x :: s1)) (merge_sort ord (y :: s2))

  termination_by length as
  decreasing_by
    all_goals {
      simp; simp_arith
      have := split_not_longer s
      rw [_hsplit] at this
      simp at this
      try exact this.left
      try exact this.right
    }

def is_sorted (ord : Order α leq) : List α → Prop
  | nil => true
  | _ :: nil => true
  | x :: y :: s => leq x y ∧ is_sorted ord (y :: s)

theorem sorted_cons {x : α} {xs : List α} :
  is_sorted leq (x :: xs) → is_sorted leq xs := by

  intro h
  match xs with
  | nil => simp [is_sorted]
  | y :: ys =>
      simp [is_sorted] at h
      exact h.right

-- There is something called "minimum"
-- (TODO: but I don't promise it is actually in the list)
-- (update from the future: I gave up on `Minimum` entirely)
structure Minimum (ord : Order α leq) (xs : List α) (value : α) where
  is_min : ∀ x, x ∈ xs → leq value x

-- Theorem: minimum(xs ++ ys) = min(minimum(xs), minimum(ys))
theorem minimum_append {ord : Order α leq} {xs ys : List α} :
  (mx : Minimum ord xs x) →
  (my : Minimum ord ys y) →
  Minimum ord (xs ++ ys) (if leq x y then x else y) := by

  intro mx my
  by_cases h : leq x y

  . rw [h]; simp
    have : ∀ a, a ∈ xs ++ ys → leq x a := by
      intro a in_xs_ys
      rw [in_append_elim] at in_xs_ys
      cases in_xs_ys
      . apply mx.is_min; assumption
      . rename_i a_in_ys; have := my.is_min a a_in_ys
        exact ord.trans _ _ _ h this
    exact ⟨this⟩  -- TODO: what are the angle brackets for?

  . simp at h; rw [h]; simp
    have : ∀ a, a ∈ xs ++ ys → leq y a := by
      intro a in_xs_ys
      rw [in_append_elim] at in_xs_ys
      cases in_xs_ys
      . rename_i a_in_xs; have := mx.is_min a a_in_xs
        exact ord.trans _ _ _ (ord.not _ _ h) this
      . apply my.is_min; assumption
    exact ⟨this⟩

-- In a sorted list, the first element is ≤ than everything else
theorem minimum_head {ord : Order α leq} {x : α} {xs : List α}:
  is_sorted ord (x :: xs) → ∀ a ∈ x :: xs, leq x a := by

  sorry

-- If something applies to all elements, it also applies to all elements in a permutation
theorem forall_permutation {P : α → Prop} {xs ys : List α} :
  (∀ x, x ∈ xs → P x) → is_permutation xs ys → ∀ y, y ∈ ys → P y := by

  sorry

-- Permutation transitivity
theorem permutation_trans {a b c : List α} :
  is_permutation a b → is_permutation b c → is_permutation a c := by

  intro hab hbc
  match a, b, c with
  | nil, nil, nil => exact is_permutation_refl nil
  | nil, nil, _ => exact hbc
  | nil, bx::bs, _ => simp! at hab
  | ax::as, nil, _ =>
      simp! at hab
      obtain ⟨_, _, h, _⟩ := hab
      have h := congrArg length h
      simp [length_append] at h
      simp_arith at h
  | ax::as, bx::bs, nil =>
      simp! at hbc
      obtain ⟨_, _, h, _⟩ := hbc
      have h := congrArg length h
      simp [length_append] at h
      simp_arith at h

  -- The only interesting case
  | ax::as, bx::bs, cx::cs =>
      rw [is_permutation] at *
      obtain ⟨al, ar, ⟨h1a, h2a⟩⟩ := hab
      obtain ⟨bl, br, ⟨h1b, h2b⟩⟩ := hbc



  -- rw [is_permutation.eq_def]
  -- split
  -- case _ => trivial
  -- case _ =>
  --   rw [is_permutation.eq_def] at hab; simp at hab



-- Ok, this is a big struggle, let's use the `Perm` definition from mathlib instead
--
-- https://github.com/leanprover/lean4/blob/ffac974dba799956a97d63ffcb13a774f700149c/src/Init/Data/List/Basic.lean#L1307-L1319
--
-- Also a good link: https://github.com/leanprover/lean4/blob/ffac974dba799956a97d63ffcb13a774f700149c/src/Init/Data/List/Perm.lean
inductive Perm : List α → List α → Prop
  -- Empty list is a permutation of itself
  | nil : Perm nil nil
  -- Consing is ok
  | cons (x : α) {a b : List α} : Perm a b → Perm (x :: a) (x :: b)
  -- Swapping is ok (this is crucial I suppose? idk)
  | swap (x y : α) {a b : List α} : Perm a b → Perm (x :: y :: a) (y :: x :: b)
  -- Transitivity
  | trans {a b c : List α} : Perm a b → Perm b c → Perm a c

theorem Perm_nil :
  Perm a b → a = nil →
  b = nil := by

  intro p
  induction p with
  | nil => simp
  | cons p' IH => intro; trivial
  | swap p' IH => intro; trivial
  | trans p1 p2 IH1 IH2 => intro h; exact IH2 (IH1 h)

-- Split a list given a `Perm`
theorem Perm_find {a b : List α} {x : α} (elem : x ∈ a) :
  Perm a b →
  ∃ (b_left b_right : List α), b = b_left ++ x :: b_right := by

  intro p
  induction p with
  | nil => trivial
  | cons x' p_ IH =>
      rename_i a' b'
      cases elem with
      | inl eq => subst x'; exists nil, b'
      | inr elem =>
          obtain ⟨bl, br, h⟩ := IH elem
          subst b'
          exists (x' :: bl), br
  | swap x' y' p_ IH =>
      rename_i a' b'
      cases elem with
      | inl eq => subst x'; exists (y' :: nil), b'
      | inr elem' =>
          cases elem' with
          | inl eq => subst y'; exists nil, x' :: b'
          | inr elem'' =>
              obtain ⟨bl, br, h⟩ := IH elem''
              subst b'
              exists (y' :: x' :: bl), br
  | trans p1 p2 IH1 IH2 =>
      rename_i a' b' c'
      obtain ⟨bl, br, h1⟩ := IH1 elem; clear IH1
      have elem'' : x ∈ b' := by
        subst b'
        simp [in_append_elim]
        right; apply in_cons
      obtain ⟨bl', br', h2⟩ := IH2 elem''; clear IH2
      exists bl', br'

theorem Perm_middle {x : α} :
  Perm (a_left ++ x :: a_right) (b_left ++ x :: b_right) →
  Perm (a_left ++ a_right) (b_left ++ b_right) := by

  -- This is like.. an alternative type? idk
  suffices ∀ a b,
    a = a_left ++ x :: a_right →
    b = b_left ++ x :: b_right →
    Perm a b →
    Perm (a_left ++ a_right) (b_left ++ b_right)
    from this _ _ rfl rfl

  intro a b a_def b_def p
  -- TODO: why doesn't this set nil = ... :(
  -- cases p with
  -- | nil => exact Perm.nil

  cases p with
  | nil =>
      exfalso
      have := nil_append_iff.mp a_def.symm
      exact nil_not_append_cons (this.right.symm)

  | cons => sorry

  | swap => sorry

  | trans p_am p_mb =>
      rename_i mid
      subst a b
      obtain ⟨mid_l, mid_r, ⟨h1, h2⟩⟩ := Perm_find in_append_cons p_am
      exact Perm.trans (Perm_middle p_am) (Perm_middle p_mb)




  -- intro a b a_def b_def p
  -- induction p with
  -- | nil =>
  --     exfalso
  --     exact nil_not_append_cons (nil_append_iff.mp a_def.symm).right.symm
  -- | cons p' IH =>

  --     rename_i x' a' b'





-- Split a list given a `Perm`
-- theorem Perm_cons_split {x : α} {a b : List α} :
--   Perm (x :: a) b →
--   ∃ (bl br : List α), b = bl ++ x :: br ∧ Perm a (bl ++ br) := by

--   intro p
--   cases p with
--   | cons p' =>
--       rename_i br'
--       exists nil, br'
--   | swap p' =>
--       rename_i a' b' br'
--       exists (a' :: nil), br'
--       simp [append]
--       exact Perm.cons p'
--   | trans p1 p2 =>
--       rename_i mid
--       obtain ⟨mid_l, mid_r, ⟨h1, h2⟩⟩ := Perm_cons_split p1
--       -- I know `p2 : Perm mid b` and therefore `x` *has* to be in `b` somewhere;
--       -- and I also know `p2` is smaller than `p`, so I should be able to use induction
--       have := Perm_cons_split p2


-- Prove that `is_permutation` (a reasonable definition) is equivalent to `Perm`
theorem Perm_equiv_is_permutation {a b : List α} :
  Perm a b → is_permutation a b := by

  intro p

  cases p with
  | nil => exact is_permutation_refl nil

  | cons x p' =>
      rename_i a' b'
      rw [is_permutation.eq_def]; simp
      exists nil, b'
      simp
      exact Perm_equiv_is_permutation p'

  | swap x y p' =>
      rename_i a' b'
      rw [is_permutation.eq_def]; simp
      exists (y :: nil), b'
      simp [append]
      rw [is_permutation.eq_def]; simp
      exists nil, b'
      simp
      exact Perm_equiv_is_permutation p'

  | trans p_ab p_bc =>
      rename_i mid
      cases a with
      | nil =>
          have := Perm_nil p_ab rfl; subst mid
          have := Perm_nil p_bc rfl; subst b
          exact is_permutation_refl nil
      | cons x xs =>
          rw [is_permutation.eq_def]; simp
          obtain ⟨bl, br, _⟩ := Perm_find in_cons p_ab; subst mid
          obtain ⟨cl, cr, _⟩ := Perm_find in_append_cons p_bc; subst b
          exists cl, cr
          simp
          have blonk : Perm xs (bl ++ br) := sorry
          have plonk : Perm (bl ++ br) (cl ++ cr) := sorry
          have bodonk : Perm xs (cl ++ cr) := Perm.trans blonk plonk
          exact Perm_equiv_is_permutation bodonk

  -- termination_by length a
  -- decreasing_by



  /-

  induction p with
  | nil => exact is_permutation_refl nil

  | cons x hp hi =>
      rename_i a' b'
      rw [is_permutation.eq_def]; simp
      exists nil, b'

  | swap x y hp hi =>
      rename_i a' b'
      rw [is_permutation.eq_def]; simp
      exists (y :: nil), b'
      simp [append]
      rw [is_permutation.eq_def]; simp
      exists nil, b'

  | trans p_ab p_bc hi_ab hi_bc =>
      rename_i a' b' c'
      cases h_a' : a' with
      | nil =>
          have := Perm_nil p_ab h_a'; subst b'; trivial
      | cons x xs =>
          rw [is_permutation.eq_def]; simp
          subst h_a'
          obtain ⟨bl, br, h⟩ := Perm_find in_cons p_ab
          subst b'
          obtain ⟨cl, cr, h⟩ := Perm_find in_append_cons p_bc
          subst c'
          exists cl, cr
          simp
          have blonk : Perm xs (bl ++ br) := sorry
          have plonk : Perm (bl ++ br) (cl ++ cr) := sorry
          have bodonk : Perm xs (cl ++ cr) := Perm.trans blonk plonk
          exact Perm_equiv_is_permutation bodonk

  termination_by length a
  decreasing_by

-/



theorem permutation_cons_mp {a b : List α} {x : α} :
  is_permutation a b → is_permutation (x :: a) (x :: b) := by

  intro h
  rw [is_permutation]
  exists nil, b

theorem permutation_cons_mpr_len (n : Nat) :
  ∀ (a b : List α) (x : α),
  length a = length b → length a ≤ n →
  is_permutation (x :: a) (x :: b) → is_permutation a b := by

  induction n with
  | zero =>
      intro a b x hab hl h
      rw [Nat.le_zero_eq] at hl
      have := length_nil_mpr hl
      have := length_nil_mpr (hab ▸ hl)
      subst_vars
      exact is_permutation_refl nil
  | succ k ih =>
      intro a b x ha hb h
      sorry




-- TODO: can this one get @[simp]?
theorem permutation_cons_mpr {a b : List α} {x : α} :
  is_permutation (x :: a) (x :: b) → is_permutation a b := by

  intro h

  -- have eq_len : length a = length b := sorry

  -- match hlen : length a with
  -- | 0 =>
  --     have := length_nil_mpr hlen
  --     have := length_nil_mpr (eq_len ▸ hlen)
  --     subst_vars
  --     exact is_permutation_refl nil

  -- | Nat.succ n =>
  --     -- it's proven for


  -- intro h
  -- rw [is_permutation] at h
  -- obtain ⟨yl, yr, ⟨h1, h2⟩⟩ := h




  -- have h_yl : yl = nil := by
  --   rw [← nil_append (x::b)] at h1
  --   have h1 := congrArg length h1  -- TODO: how to replace?
  --   repeat rw [length_append, length_cons] at h1

  --   simp_arith at h1

  -- have h_yr : yr = b := sorry
  -- rw [h_yl, h_yr] at h2; simp at h2; assumption

-- if smth is sorted, and another element is ≤, then cons is also sorted
theorem sorted_after_cons {ord : Order α leq} {x : α} {xs : List α} :
  is_sorted ord xs → (∀ a, a ∈ xs → leq x a) → is_sorted ord (x :: xs) := by

  intro xs_sorted x_leq_xs
  match xs with
  | nil => simp [is_sorted]
  | y :: ys =>
      simp [is_sorted, x_leq_xs y in_cons]
      assumption


-- `merge` creates a permutation
theorem merge_permutation {ord : Order α leq} {xs ys : List α} :
  is_permutation (merge ord xs ys) (xs ++ ys) := by

  sorry

-- theorem merge_sorted_is_sorted_induction_by_length (ord : Order α leq) (xs ys : List α) :
--   is_sorted ord xs → is_sorted ord ys → is_sorted ord (merge ord xs ys) := by

--   intro sorted_xs sorted_ys

--   let size : Nat := length xs + length ys
--   have : length xs + length ys = size -> is_sorted ord (merge ord xs ys) := by
--     induction size with
--     | zero => -- TODO: there has to be a nicer way to get size=0 in hypotheses
--     intro hsize ...
--     | succ n ih =>
--   apply this
--   simp [size]

-- `merge` preserves sortedness
theorem merge_sorted_is_sorted (ord : Order α leq) (xs ys : List α) :
  is_sorted ord xs → is_sorted ord ys → is_sorted ord (merge ord xs ys) := by

  intro sorted_xs sorted_ys

  match _hxs : xs, _hys : ys with
  | nil, _ => simp [merge]; assumption
  | x :: xs', nil => simp [merge]; assumption
  | x :: xs', y :: ys' =>
      simp [merge]
      cases leq_x_y : leq x y with
      | true =>
          simp
          apply sorted_after_cons
          . refine merge_sorted_is_sorted ord xs' (y :: ys') ?_ ?_
            . exact sorted_cons sorted_xs
            . assumption
          . intro a a_elem
            have : a ∈ xs' ++ y :: ys' := in_permutation a_elem merge_permutation
            cases in_append_elim_mp this with
            | inl a_in_xs' =>
                refine minimum_head sorted_xs a (? a_in_xs')
                rw [mem_elim_cons]; right; assumption
            | inr a_in_ys =>
                have leq_y_a : leq y a := minimum_head sorted_ys a a_in_ys
                exact ord.trans x y a leq_x_y leq_y_a

      | false =>
          simp
          apply sorted_after_cons
          . refine merge_sorted_is_sorted ord (x :: xs') ys' ?_ ?_
            . assumption
            . exact sorted_cons sorted_ys
          . intro a a_elem
            have : a ∈ x :: xs' ++ ys' := in_permutation a_elem merge_permutation
            cases in_append_elim_mp this with
            | inl a_in_xs =>
                have leq_x_a : leq x a := minimum_head sorted_xs a a_in_xs
                exact ord.trans y x a (ord.not _ _ leq_x_y) leq_x_a
            | inr a_in_ys' =>
                refine minimum_head sorted_ys a (? a_in_ys')
                rw [mem_elim_cons]; right; assumption


-- Prove that `merge_sort` produces a sorted list
theorem merge_sort_sorts (ord : Order α leq) (s : List α) :
  is_sorted ord (merge_sort ord s) := by

  match h : s with
  | nil =>
      simp [merge_sort, is_sorted]
  | x :: nil =>
      simp [merge_sort, is_sorted]
  | x :: y :: s' =>
      simp [merge_sort]
      apply merge_sorted_is_sorted
      . apply merge_sort_sorts
      . apply merge_sort_sorts

  termination_by length s
  decreasing_by
    all_goals {
      simp; simp_arith
      have := split_not_longer s'
      simp at this
      try exact this.left
      try exact this.right
    }

-- Prove that `merge_sort` produces a permutation
theorem merge_sort_permutes (ord : Order α leq) (s : List α) :
  is_permutation (merge_sort ord s) s := by

  match s_def : s with
  | nil => simp [merge_sort, is_permutation]
  | x :: nil => simp [merge_sort]; exists nil, nil
  | x :: y :: s' =>
      simp [merge_sort]
      -- TODO: do a rewrite like this? rw [(split s').fst = s1]
      let s1 := (split s').fst; have es1 : (split s').fst = s1 := rfl
      let s2 := (split s').snd; have es2 : (split s').snd = s2 := rfl
      rewrite [es1, es2]
      have hx := merge_sort_permutes ord (x :: s1)
      have hy := merge_sort_permutes ord (y :: s2)
      have h
        : is_permutation
            (merge ord (merge_sort ord (x :: s1)) (merge_sort ord (y :: s2)))
            (merge_sort ord (x :: s1) ++ merge_sort ord (y :: s2))
        := merge_permutation
      have h
        : is_permutation
            (merge ord (x :: s1) (y :: s2))
            (x :: s1 ++ y :: s2)
        := merge_permutation

      apply permutation_trans (b := x :: s1 ++ y :: s2)
      . apply permutation_trans (b := merge_sort ord (x :: s1) ++ merge_sort ord (y :: s2))
        . exact merge_permutation
        . apply permutation_pair
          . sorry
          . sorry
      . have := split_permutes s'; simp at this
        rw [← s_def, ← es1]










-- https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#tactic-ref