propagateValueInconsistency

Mathlib.Tactic.CC.Addition

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCM.propagateValueInconsistency

Lean4

/-- Derive contradiction if we can get equality between different values. -/
def propagateValueInconsistency (e₁ e₂ : Expr) : CCM Unit := do
  guard (← isInterpretedValue e₁)
  guard (← isInterpretedValue e₂)
  let some eqProof ← getEqProof e₁ e₂ |
    failure
  let trueEqFalse ← mkEq (.const ``True []) (.const ``False [])
  let neProof :=
    Expr.app (.proj ``Iff 0 (← mkAppOptM ``bne_iff_ne #[none, none, none, e₁, e₂])) (← mkEqRefl (.const ``true []))
  let H ← mkAbsurd trueEqFalse eqProof neProof
  pushEq (.const ``True []) (.const ``False []) H

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

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

Разделы

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

Аффилиация

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