Drop from the Last Separator

This file contains the list-level operation used by separator-erasing block machines.

Key results

• dropFromLastSep: drops everything through the final occurrence of sep.
• dropFromLastSep_not_mem: if sep is absent, the operation is the identity.
• dropFromLastSep_ne_default: non-default cells stay non-default.

def dropFromLastSep {Γ : Type} [DecidableEq Γ] (sep : Γ) : List Γ → List Γ

Drop everything up to and including the LAST occurrence of sep. If sep ∉ l, return l unchanged.

Equations

• dropFromLastSep sep [] = []
• dropFromLastSep sep (c :: rest) = if sep ∈ rest then dropFromLastSep sep rest else if c = sep then rest else c :: rest

theorem dropFromLastSep_nil {Γ : Type} [DecidableEq Γ] (sep : Γ) : dropFromLastSep sep [] = []

theorem dropFromLastSep_cons_mem {Γ : Type} [DecidableEq Γ] (sep c : Γ) (rest : List Γ) (h : sep ∈ rest) : dropFromLastSep sep (c :: rest) = dropFromLastSep sep rest

theorem dropFromLastSep_cons_sep_not_mem {Γ : Type} [DecidableEq Γ] (sep : Γ) (rest : List Γ) (h : sep ∉ rest) : dropFromLastSep sep (sep :: rest) = rest

theorem dropFromLastSep_cons_ne_not_mem {Γ : Type} [DecidableEq Γ] (sep c : Γ) (rest : List Γ) (hc : c ≠ sep) (h : sep ∉ rest) : dropFromLastSep sep (c :: rest) = c :: rest

theorem dropFromLastSep_not_mem {Γ : Type} [DecidableEq Γ] (sep : Γ) (l : List Γ) (h : sep ∉ l) : dropFromLastSep sep l = l

When sep ∉ l, dropFromLastSep is the identity.

theorem dropFromLastSep_ne_default {Γ : Type} [Inhabited Γ] [DecidableEq Γ] (sep : Γ) (l : List Γ) (hl : ∀ g ∈ l, g ≠ default) (g : Γ) : g ∈ dropFromLastSep sep l → g ≠ default

dropFromLastSep preserves non-defaultness.