reify_or

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Fmla.reify_or

Lean4

/-- Negation turns AND into OR, so `¬⟦f₁ ∧ f₂⟧_v ≡ ¬⟦f₁⟧_v ∨ ¬⟦f₂⟧_v`. -/
theorem reify_or {f₁ : Fmla} {a : Prop} {f₂ : Fmla} {b : Prop} (h₁ : Fmla.reify v f₁ a) (h₂ : Fmla.reify v f₂ b) :
    Fmla.reify v (f₁.and f₂) (a ∨ b) :=
  by
  refine ⟨fun H ↦ by_contra fun hn ↦ H ⟨fun c h ↦ by_contra fun hn' ↦ ?_⟩⟩
  rcases List.mem_append.1 h with h | h
  · exact hn <| Or.inl <| h₁.1 fun Hc ↦ hn' <| Hc.1 _ h
  · exact hn <| Or.inr <| h₂.1 fun Hc ↦ hn' <| Hc.1 _ h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru