提交 #4

import Mathlib.Data.Int.Bitwise

def prefixes {A : Type} : List A → List (List A)
  | [] => [[]]
  | a :: l0 => [] :: (List.map (fun x => a :: x) (prefixes l0))

lemma nil_in_prefixes {A : Type} (l : List A) : [] ∈ prefixes l := by
  induction l with
  | nil => simp [prefixes]
  | cons a l ih =>
      simp [prefixes]

theorem in_prefixes {A : Type} (l1 l2 : List A) : l1 ∈ prefixes (l1 ++ l2) := by
  induction l1 generalizing l2 with
  | nil =>
      simp [nil_in_prefixes]
  | cons a l1 ih =>
      simp [prefixes, List.cons_append]
      apply ih

theorem in_prefixes_inv {A : Type} (l1 l : List A) :
    l1 ∈ prefixes l → ∃ l2, l1 ++ l2 = l := by
  induction l generalizing l1 with
  | nil =>
      intro h
      simp [prefixes] at h
      rw [h]
      exists []
  | cons a l ih =>
      intro h
      simp [prefixes] at h
      rcases h with (rfl | h)
      · exact ⟨a :: l, rfl⟩
      · rcases h with ⟨l1', h1, rfl⟩
        rcases ih l1' h1 with ⟨l2, h2⟩
        exact ⟨l2, by simp [h2]⟩


def sublists {A : Type} : List A → List (List A)
  | [] => [[]]
  | a :: l0 => List.map (fun x => a :: x) (prefixes l0) ++ sublists l0

lemma nil_in_sublists {A : Type} (l : List A) : [] ∈ sublists l := by
  induction l with
  | nil => simp [sublists]
  | cons a l ih =>
      simp [sublists]
      exact ih


lemma prefixes_in_sublists {A : Type} (l1 l2 : List A) : l1 ∈ sublists (l1 ++ l2) := by
  induction l1 with
  | nil =>
      simp [nil_in_sublists]
  | cons a l1 ih =>
      simp [sublists, List.cons_append]
      left
      have h : l1 ∈ prefixes (l1 ++ l2) := in_prefixes l1 l2
      apply h

theorem in_sublists {A : Type} (l1 l2 l3 : List A) :
    l2 ∈ sublists (l1 ++ l2 ++ l3) := by
  induction l1 with
  | nil =>
      simp
      exact prefixes_in_sublists l2 l3
  | cons a l1 ih =>
      simp [sublists]
      right
      rw [<- List.append_assoc]
      apply ih

theorem in_sublists_inv {A : Type} (l2 l : List A) :
    l2 ∈ sublists l → ∃ l1 l3, l1 ++ l2 ++ l3 = l := by
  induction l generalizing l2 with
  | nil =>
      intro h
      simp [sublists] at h
      rcases h with (rfl | ⟨⟩)
      exact ⟨[], [], rfl⟩
  | cons a l ih =>
      intro h
      simp [sublists] at h
      rcases h with (h | h)
      · rcases h with ⟨l2', h1, rfl⟩
        rcases in_prefixes_inv l2' l h1 with ⟨l3, h2⟩
        exact ⟨[], l3, by simp [h2]⟩
      · rcases ih l2 h with ⟨l1, l3, h3⟩
        exact ⟨a :: l1, l3, by simp [h3]⟩