提交 #17

variable {A : Type}

def prefixes : List A → List (List A)
  | [] => [[]]
  | a :: l₀ => [] :: (List.map (fun x => a :: x) (prefixes l₀))

def sublists : List A → List (List A)
  | [] => [[]]
  | a :: l₀ => List.map (fun x => a :: x) (prefixes l₀) ++ sublists l₀

theorem in_prefixes (l₁ l₂ : List A) : l₁ ∈ prefixes (l₁ ++ l₂) := by
  induction l₁ with
  | nil => unfold prefixes; grind
  | cons head tail h => simp [prefixes, h]

theorem in_prefixes_inv (l₁ l : List A) : l₁ ∈ prefixes l → ∃ l₂, l₁ ++ l₂ = l := by
  induction l generalizing l₁ with
  | nil =>
    intro h
    simp [prefixes] at h
    simp [h]
  | cons head tail h =>
    intro h'
    simp [prefixes] at h'
    cases h' with
    | inl e => simp [e]
    | inr l₂i =>
      have ⟨l₂, l₂p, hl₂⟩ := l₂i
      have ⟨l₃, l₂₃⟩ := h l₂ l₂p
      refine ⟨l₃, ?_⟩
      rw [← hl₂, ← l₂₃, List.cons_append]

theorem empty_sublists (l : List A) : [] ∈ sublists l := by
  induction l with
  | nil => simp [sublists]
  | cons head tail h => simp [sublists, h]

theorem in_sublists (l₁ l₂ l₃ : List A) : l₂ ∈ sublists (l₁ ++ l₂ ++ l₃) := by
  induction l₁ with
  | nil =>
    unfold sublists
    simp
    split
    · next h => simp at h; simp [h]
    next head tail l₂₃ =>
      simp
      cases l₂ with
      | nil => exact Or.inr (empty_sublists tail)
      | cons head' tail' =>
        simp at l₂₃
        left
        refine ⟨tail', ?_, ?_⟩
        · rw [← l₂₃.2]
          exact in_prefixes tail' l₃
        · rw [l₂₃.1]
  | cons head tail h =>
    simp at h
    simp [sublists, h]

theorem in_sublists_inv (l₂ l : List A) : l₂ ∈ sublists l → ∃ l₁ l₃, l₁ ++ l₂ ++ l₃ = l := by
  induction l with
  | nil => simp [sublists]
  | cons head tail h =>
    intro h'
    simp [sublists] at h'
    cases h' with
    | inl l₂p =>
      have ⟨l₃, l₃p, hl₂⟩ := l₂p
      have ⟨l₄, l₃₄⟩ := in_prefixes_inv l₃ tail l₃p
      refine ⟨[], l₄, ?_⟩
      rw [← hl₂]
      simp [l₃₄]
    | inr l₂t =>
      have ⟨l₁, l₃, l₁₂₃⟩ := h l₂t
      refine ⟨head :: l₁, l₃, ?_⟩
      rw [← l₁₂₃]
      simp