pair_encode_injective

theoremverified

The pair encoding is injective: if pairEncode w₁ c₁ = pairEncode w₂ c₂ then w₁ = w₂ and c₁ = c₂.

Statement

theorem pair_encode_injective {Γ : Type} {w₁ c₁ w₂ c₂ : List Γ}
    (h : pairEncode w₁ c₁ = pairEncode w₂ c₂) : w₁ = w₂ ∧ c₁ = c₂

Source

folklore; needed for the verifier characterisation of NP (Arora & Barak, Def. 2.2)

Verified

10 Sep 2026

Axioms

propext

Built on 1

pairEncodeFor words w and c over an alphabet Γ, pairEncode w c is the word over Γ ⊕ Unit obtained by writing w, then the single separator symbol…

Read back from the Lean

For every type Γ and every four lists w₁, c₁, w₂, c₂ with elements in Γ: if the encoding pairEncode w₁ c₁ equals the encoding pairEncode w₂ c₂, then w₁ = w₂ and c₁ = c₂. Explicitly, with all binders in order and all hypotheses named: ∀ (Γ : Type) (w₁ c₁ w₂ c₂ : List Γ), pairEncode w₁ c₁ = pairEncode w₂ c₂ → (w₁ = w₂ ∧ c₁ = c₂). There are no typeclass/instance hypotheses (in particular no [DecidableEq Γ]) and no other hypotheses besides the equality of the two encodings. The single hypothesis is the equality of the encoded lists; the conclusion is the conjunction of the two component equalities, i.e. the map (w, c) ↦ pairEncode w c is injective on List Γ × List Γ for every Γ.

Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.

Lean source view module on GitHub

theorem pair_encode_injective_aux {Γ : Type} :
    ∀ (w₁ w₂ : List Γ) (x y : List (Γ ⊕ Unit)),
      List.map Sum.inl w₁ ++ Sum.inr () :: x = List.map Sum.inl w₂ ++ Sum.inr () :: y →
      w₁ = w₂ ∧ x = y := by
  intro w₁
  induction w₁ with
  | nil =>
    intro w₂ x y h
    cases w₂ with
    | nil => exact ⟨rfl, (List.cons.inj h).2⟩
    | cons b w₂ =>
      simp only [List.map_cons, List.map_nil, List.nil_append] at h
      exact absurd (List.cons.inj h).1 Sum.inr_ne_inl
  | cons a w₁ ih =>
    intro w₂ x y h
    cases w₂ with
    | nil =>
      simp only [List.map_cons, List.map_nil, List.nil_append] at h
      exact absurd (List.cons.inj h).1 Sum.inl_ne_inr
    | cons b w₂ =>
      simp only [List.map_cons] at h
      obtain ⟨hab, htail⟩ := List.cons.inj h
      have hab' : a = b := Sum.inl_injective hab
      obtain ⟨hw, hxy⟩ := ih w₂ x y htail
      exact ⟨by rw [hab', hw], hxy⟩

/-- The pair encoding (w, c) ↦ w ++ [sep] ++ c is injective. -/
theorem pair_encode_injective {Γ : Type} {w₁ c₁ w₂ c₂ : List Γ}
    (h : pairEncode w₁ c₁ = pairEncode w₂ c₂) : w₁ = w₂ ∧ c₁ = c₂ := by
  simp only [pairEncode, List.singleton_append, List.append_assoc] at h
  obtain ⟨hw, hc⟩ :=
    pair_encode_injective_aux w₁ w₂ (List.map Sum.inl c₁) (List.map Sum.inl c₂) h
  exact ⟨hw, (Function.Injective.list_map Sum.inl_injective) hc⟩

Discuss this result Challenge it