UNDER CONSTRUCTION
Code for this chapter

Strings

open List

Note that List already have an ordering on them, but it is not the prefix ordering. This creates issues because List.le and [LT (List A)] are already defined. We avoid this here by just not using the ≤ notation.

#check List.le
variable {A : Type u} (x : List A) [LT A]
#check [] ≤ x
#eval [1,2,3] ≤ [1,2,5]
example {A : Type u} [LT A] (x : List A) : [] ≤ x := by
  simp[List.instLE]

End Note

instance list_poset {A : Type u} : Poset (List A) :=
  ⟨
    IsPrefix,
    List.prefix_refl,
    by
      intro s t ⟨ x, h1 ⟩ ⟨ y, h2 ⟩
      aesop,
    by
      intro s t u
      exact List.IsPrefix.trans
  ⟩

example {A : Type u} (x : List A) : [] <+: x := by
  simp[list_poset]

def meet {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A) : List A :=
  match x,y with
  | [], [] => []
  | _, [] => []
  | [], _ => []
  | a::L, b::M => if a = b then a :: meet L M else []

theorem bot_le {A : Type u} [Poset (List A)] (x: List A) : [] <+: x := by
  exact nil_prefix

theorem meet_le {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A)
  : (meet x y) <+: x := by
  match x,y with
  | a::L, b::M =>
    simp[meet]
    split_ifs
    . have : IsPrefix (meet L M) L := by apply meet_le -- structural recursion!
      simp[this]
    . apply bot_le
  | [], [] => simp[meet]
  | a::L, [] => simp[meet]
  | [], b::M => simp[meet]

theorem meet_le' {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A)
  : (meet x y) <+: y := by
  match x,y with
  | a::L, b::M =>
    simp[meet]
    split_ifs
    . have : IsPrefix (meet L M) M := by apply meet_le' -- structural recursion!
      simp[this]
      assumption
    . apply bot_le
  | [], [] => simp[meet]
  | a::L, [] => simp[meet]
  | [], b::M => simp[meet]

theorem meet_great {A : Type u} [Poset (List A)] [DecidableEq A] (x y : List A)
  : ∀ w, w <+: x → w <+: y → w <+: (meet x y) := by
  intro w hwx hwy
  match x, y with
  | a::L, b::M =>
    simp[meet]
    split_ifs
    . rename_i hab
      simp_all[hab]
      by_cases hw : w = []
      . simp[hw]
      . obtain ⟨ c, ⟨ N, hcN ⟩ ⟩ := ne_nil_iff_exists_cons.mp hw
        simp_all[hcN]
        apply meet_great -- structural recursion!
        . exact hwx.right
        . exact hwy
    . rename_i hab
      have : w = [] := by
        by_cases h : w = []
        . exact h
        . have ⟨ c, ⟨ N, hN ⟩ ⟩ : ∃ c, ∃ N, w = c :: N := ne_nil_iff_exists_cons.mp h
          have h1 : c = a := by simp_all[hN]
          have h2 : c = b := by simp_all[hN]
          simp_all
      simp[this]
  | [], [] => simp[meet,hwx]
  | a::L, [] => simp[meet,hwy]
  | [], b::M => simp[meet,hwx]

instance info_semilattice {A : Type u} [DecidableEq A] : Semilattice (List A) :=
  ⟨
    meet,
    λ L M => by
      constructor
      . constructor
        . apply meet_le
        . apply meet_le'
      . apply meet_great
  ⟩