How to determine if the conditions are contradictory?

Stream: new members

[tsuki hao]

Dose there exist a simple tactic that can lead to a contradiction of the conditions?

import Mathlib
import LeanCopilot


theorem lean_workbook_plus_79999 (a b c d e : ℝ) (hab : a = 13) (hbc : b = 14) (hca : c = 15) (hpc : d = 10) (hABCD : a + b = c + d) (hABCE : a + b = c + e) (hDEF : d + e = 2 * b) : e - d = 12 * Real.sqrt 2    := by

[Johan Commelin]

linarith works

[Johan Commelin]

In general, the tactic you need of course depends on the shape of your conditions

[Edward van de Meent]

contradiction is another good one to know about

[tsuki hao]

Johan Commelin said:

linarith works

Actually, when I use linarith, the formal statement is proved? But the hypothesis contradict with each other :smiling_face_with_tear:

[Josha Dekker]

tsuki hao said:

Johan Commelin said:

linarith works

Actually, when I use linarith, the formal statement is proved? But the hypothesis contradict with each other :smiling_face_with_tear:

If the hypotheses contradict each-other, you can prove False, which then proves anything.

[tsuki hao]

Edward van de Meent said:

contradiction is another good one to know about

contradiction is to negate the conclusion?But what I need is to verify if the hypothesis is contradictory?

[Ruben Van de Velde]

No, contradiction solves any goal if there's P and not P in the context; you may be thinking of by_contra

[tsuki hao]

Josha Dekker said:

tsuki hao said:

Johan Commelin said:

linarith works

Actually, when I use linarith, the formal statement is proved? But the hypothesis contradict with each other :smiling_face_with_tear:

If the hypotheses contradict each-other, you can prove False, which then proves anything.

Yeah! Then how can I prove False using some simple tactic? I want to get the state False in Lean Infoview.

[Edward van de Meent]

you want the goal to be False? or you want to have a hypothesis False? for the first, you can probably use apply False.elim, while for the second, you can do have hfalse: False := by ...

[tsuki hao]

Maybe my explanation was unclear. I want to automatically verify whether the hypotheses contradict with each other, and if they are, to derive a new condition: False.

[Ralf Stephan]

I would set the goal manually to False and write contradiction in the proof. If it succeeds, your conditions are contradictory.

[Edward van de Meent]

how about this:

import Mathlib

macro "have_contra" n:ident : tactic => `(tactic|
  try have $n :False := by (
    try contradiction;
    try linarith;
    try omega;))

theorem lean_workbook_plus_79999 (a b c d e : ℝ) (hab : a = 13) (hbc : b = 14) (hca : c = 15)
    (hpc : d = 10) (hABCD : a + b = c + d) (hABCE : a + b = c + e) (hDEF : d + e = 2 * b) :
    e - d = 12 * Real.sqrt 2 := by
  have_contra hfalse
  sorry

example : 1 = 1 := by
  have_contra hfalse
  sorry

[Ruben Van de Velde]

As it happens, "automatically verify whether the hypotheses contradict with each other" is just as strong as "prove the theorem", so you can't expect a procedure that works in general

[Edward van de Meent]

indeed. to elaborate on why that is: if you'd like to prove that $h_1,h_2,h_3,\ldots,h_n \rightarrow P$ with $h_i$ your hypotheses and $P$ your goal, it suffices to show that $h_1,h_2,h_3,\ldots,h_n,\neg P$ is a set of contradictory hypotheses.