not — Mathlib

English

A technical lemma asserting that the specific pattern L2 ++ (x,b) :: (x,¬b) :: L3 cannot occur as a reduction of L1; otherwise any proposition would hold (a form of a contradiction-elimination).

Русский

Техническая лемма, утверждающая, что образец L2 ++ (x,b) :: (x,¬b) :: L3 не может быть результатом редукции L1; иначе можно было бы доказать что угодно.

LaTeX

$$$$\forall L_1,L_2,L_3,x,b\; (\operatorname{reduce}(L_1) = L_2 \cup (x,b) :: (x, b^{\neg}) :: L_3) \Rightarrow \text{False}.$$$$

Lean4

@[to_additive]
theorem not {p : Prop} : ∀ {L₁ L₂ L₃ : List (α × Bool)} {x b}, reduce L₁ = L₂ ++ (x, b) :: (x, !b) :: L₃ → p
  | [], L2, L3, _, _ => fun h => by cases L2 <;> injections
  | (x, b) :: L1, L2, L3, x', b' => by
    dsimp
    cases r : reduce L1 with
    | nil =>
      dsimp; intro h
      exfalso
      have := congr_arg List.length h
      grind
    | cons hd tail =>
      obtain ⟨y, c⟩ := hd
      dsimp only
      split_ifs with h <;> intro H
      · rw [H] at r
        exact @reduce.not _ L1 ((y, c) :: L2) L3 x' b' r
      rcases L2 with (_ | ⟨a, L2⟩)
      · injections; subst_vars
        simp at h
      · refine @reduce.not _ L1 L2 L3 x' b' ?_
        rw [List.cons_append] at H
        injection H with _ H
        rw [r, H]

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