diamond_aux — Mathlib

English

Let L1, L2, L3, L4 be lists of pairs and x1,b1,x2,b2 be elements with L1 ++ (x1,b1) :: (x1, not b1) :: L2 = L3 ++ (x2,b2) :: (x2, not b2) :: L4. Then either L1 ++ L2 = L3 ++ L4, or there exists L5 such that Red.Step (L1 ++ L2) L5 and Red.Step (L3 ++ L4) L5.

Русский

Пусть L1,L2,L3,L4 — списки пар, а x1,b1, x2,b2 — элементы. Если L1 ++ (x1,b1) :: (x1, not b1) :: L2 = L3 ++ (x2,b2) :: (x2, not b2) :: L4, то либо L1 ++ L2 = L3 ++ L4, либо существует L5 such that Red.Step (L1 ++ L2) L5 и Red.Step (L3 ++ L4) L5.

LaTeX

$$$\forall {L_1,L_2,L_3,L_4:\text{List}(\alpha\times\text{Bool})}\; x_1,b_1,x_2,b_2,\; L_1 ++ (x_1,b_1) :: (x_1, b_1^{\neg}) :: L_2 = L_3 ++ (x_2,b_2) :: (x_2, b_2^{\neg}) :: L_4 \Rightarrow L_1 ++ L_2 = L_3 ++ L_4 \lor \exists L_5, Red.Step (L_1 ++ L_2) L_5 \land Red.Step (L_3 ++ L_4) L_5$$$

Lean4

@[to_additive]
theorem diamond_aux :
    ∀ {L₁ L₂ L₃ L₄ : List (α × Bool)} {x1 b1 x2 b2},
      L₁ ++ (x1, b1) :: (x1, !b1) :: L₂ = L₃ ++ (x2, b2) :: (x2, !b2) :: L₄ →
        L₁ ++ L₂ = L₃ ++ L₄ ∨ ∃ L₅, Red.Step (L₁ ++ L₂) L₅ ∧ Red.Step (L₃ ++ L₄) L₅
  | [], _, [], _, _, _, _, _, H => by injections; subst_vars; simp
  | [], _, [(x3, b3)], _, _, _, _, _, H => by injections; subst_vars; simp
  | [(x3, b3)], _, [], _, _, _, _, _, H => by injections; subst_vars; simp
  | [], _, (x3, b3) :: (x4, b4) :: tl, _, _, _, _, _, H => by injections; subst_vars; right;
    exact ⟨_, Red.Step.not, Red.Step.cons_not⟩
  | (x3, b3) :: (x4, b4) :: tl, _, [], _, _, _, _, _, H => by injections; subst_vars; right;
    simpa using ⟨_, Red.Step.cons_not, Red.Step.not⟩
  | (x3, b3) :: tl, _, (x4, b4) :: tl2, _, _, _, _, _, H =>
    let ⟨H1, H2⟩ := List.cons.inj H
    match Step.diamond_aux H2 with
    | Or.inl H3 => Or.inl <| by simp [H1, H3]
    | Or.inr ⟨L₅, H3, H4⟩ => Or.inr ⟨_, Step.cons H3, by simpa [H1] using Step.cons H4⟩

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