Cut elimination for classical linear logic

DefinitionList representative of a submultiset by scanning a list#✓fully proved

Compute a list representative of a submultiset by scanning a supplied list. The resulting list preserves the order of the selected occurrences in the supplied list.

Multiset.scanToList · 24 lines

def scanToList [DecidableEq α] (l : List α) (s : Multiset α)
    (h : s ≤ (l : Multiset α)) : {l' : List α // (l' : Multiset α) = s} :=
  match l with
  | [] =>
    ⟨[], by
      have hs : s = 0 := Multiset.le_zero.mp (by simpa using h)
      simpa using hs.symm⟩
  | a :: l =>
    if ha : a ∈ s then
      have h' : s.erase a ≤ (l : Multiset α) := by
        apply Multiset.erase_le_iff_le_cons.mpr
        simpa using h
      let l' := scanToList l (s.erase a) h'
      ⟨a :: l'.1, by
        change a ::ₘ (l'.1 : Multiset α) = s
        rw [l'.2]
        exact Multiset.cons_erase ha⟩
    else
      have h' : s ≤ (l : Multiset α) := by
        have he : s.erase a ≤ (l : Multiset α) := by
          apply Multiset.erase_le_iff_le_cons.mpr
          simpa using h
        simpa [Multiset.erase_of_notMem ha] using he
      scanToList l s h'

Used by 3

Used byList presentations of two summands from a supplied list · List presentation of a tail without choosing a representative · Splitting replicated question marks across two summands

• Prerequisite APIs for the frozen cut-elimination source port
• Cut-free proofs, cut admissibility, and cut elimination for classical linear logic
• Source exponential multicut for the locked CLL calculus
• Source cut elimination for the locked CLL calculus
• Canonical pinned API for the upstream CLL cut-elimination port

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.