listDecode — Mathlib

English

Decodes a list of encoded symbols into a list of bounded formulas by a recursive specification handling various constructor cases (terms, relations, 2-sums, etc.).

Русский

Декодирует список закодированных символов в список ограниченных формул согласно рекурсивному определению, учитывая различные случаи конструкторов.

LaTeX

$$$\\text{listDecode}: \\text{List}((\\Sigma k, L.Term(α\\oplus\\mathrm{Fin}k)) \\oplus ((\\Sigma n, L.Relations n) \\oplus \\Bbb N)) \\to \\text{List}(\\Sigma n, L.BoundedFormula α n)$$$

Lean4

/-- Decodes a list of symbols as a list of formulas. -/
def listDecode : List ((Σ k, L.Term (α ⊕ Fin k)) ⊕ ((Σ n, L.Relations n) ⊕ ℕ)) → List (Σ n, L.BoundedFormula α n)
  | Sum.inr (Sum.inr (n + 2)) :: l => ⟨n, falsum⟩ :: (listDecode l)
  | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l =>
    (if h : n₁ = n₂ then ⟨n₁, equal t₁ (Eq.mp (by rw [h]) t₂)⟩ else default) :: (listDecode l)
  | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l =>
    (if h : ∀ i : Fin n, (l.map Sum.getLeft?)[i]?.join.isSome then
        if h' : ∀ i, (Option.get _ (h i)).1 = k then
          ⟨k, BoundedFormula.rel R fun i => Eq.mp (by rw [h' i]) (Option.get _ (h i)).2⟩
        else default
      else default) ::
      (listDecode (l.drop n))
  | Sum.inr (Sum.inr 0) :: l =>
    if h : 2 ≤ (listDecode l).length then (sigmaImp (listDecode l)[0] (listDecode l)[1]) :: (drop 2 (listDecode l))
    else []
  | Sum.inr (Sum.inr 1) :: l =>
    if h : 1 ≤ (listDecode l).length then (sigmaAll (listDecode l)[0]) :: (drop 1 (listDecode l)) else []
  | _ => []
termination_by l => l.length

Похожие утверждения