Check consistency between two statements

Stream: new members

[Harith]

Hello!
I'm pretty new to Lean and I've gone through some of the basics.
I was wondering if there is a way to check consistency between 2 given mathematical statements. In the sense, if we have 2 hypotheses h1, h2, is there a way to check if h1 does not negate any part of h2?

Example:
h1 : x = 25
h2 : x != 25

Is there a way to sort of say h1 \and h2 is false? The above example has only 1 variable in both the hypotheses, but I am looking to generalize it to any number of variables. A simple example would be: if h2 : y != 25 then I want h1 ^ h2 is true since they are consistent.

[Aaron Liu]

Harith said:

Hello!
I'm pretty new to Lean and I've gone through some of the basics.
I was wondering if there is a way to check consistency between 2 given mathematical statements. In the sense, if we have 2 hypotheses h1, h2, is there a way to check if h1 does not negate any part of h2?

Example:
h1 : x = 25
h2 : x != 25

Is there a way to sort of say h1 \and h2 is false? The above example has only 1 variable in both the hypotheses, but I am looking to generalize it to any number of variables. A simple example would be: if h2 : y != 25 then I want h1 ^ h2 is true since they are consistent.

Sorry, I don't quite follow. What statement do you want to make? Remember that if h1 : x = 25, then x = 25 is the statement and h1 is a proof of the statement.

[Martin Dvořák]

Is there a way to sort of say h1 \and h2 is false?

example {x} (h1 : x = 25) (h2 : x ≠ 25) : False := h2 h1

[Notification Bot]

3 messages were moved here from #new members > defining variables by Kenny Lau.

[Kenny Lau]

@Harith are the x in the two statements referring to the same value? can you state your question mathematically? what is your maths background and what Lean basics have you gone through?

[Harith]

Yeah, let me phrase the question mathematically (I'll try to ;-;). So far I've gone through a couple of modules in https://lean-lang.org/theorem_proving_in_lean4/
https://lean-lang.org/doc/reference/latest/
https://hrmacbeth.github.io/math2001/

I have a pretty decent math background - but pretty new to formal theorem proving

My intention is as follows:
Given a set of variables, and some equations involving these variables, I wanna know if the equations are consistent with each other.

If we have 2 variables x, y and equations as follows:

1. x = 10
2. y = 15
3. x + y = 25
4. x - y = 2

We can say 4 is not consistent with 1 and 2 right. Is there a way I can generalize something like this in Lean?
not sure I did a better job at explaining this time, hope its a lil bit more clear.

[Aaron Liu]

What do you mean by "generalize"?

[Luigi Massacci]

At the very least you would need to specify the domain of those variables. x + x = 1 is impossible over the integers, but not the rationals, while x ^ 2 = -1 is impossible over the rationals, but not over complex numbers, etc. If you are working over the rationals, linarith can do that for you.

[Kenny Lau]

@Harith see, "consistent" is a math term that nobody tends to think about the definition of. What consistent means is that they have a solution (so a big exists statement), and what inconsistent means is that you can prove false from those statements. This is how I would formalise it.

You also need to pay attention to types. The x and y in your equations are untyped, which is very dangerous when you're doing Lean. For all I know, they could all be in Fin 1.

import Mathlib

example (x y : ℝ) (h1 : x = 10) (h2 : y = 15) (h3 : x + y = 25) (h4 : x - y = 2) : False := by
  rw [h1, h2] at h4
  norm_num at h4

[Kenny Lau]

I can believe that you have a decent math background, but then what you would need to pay attention to is that sometimes mathematicians throw terms around that everyone knows what they mean, but it's a different thing when you need to formalise them, because then you suddenly need to make everything absolutely specific.

[Harith]

@Kenny Lau Got it! that helps and I shall be mindful of keeping things specific.
@Aaron Liu by generalize I meant something like, given a bunch of variables and equations like the ones above, I wanna prove

example  (x1 x2 ... xn : \R) (h1 : eq1) (h2 : eq2) ... (hn : eqn) : True

[Kenny Lau]

@Harith you can always prove true (the proof is trivial), so this is not what you want.

[Kenny Lau]

as I mentioned above, you need a big exists statement

[Kenny Lau]

can you be more specific? I see that you've now specified them as real numbers, but what do the equations look like?

[Kenny Lau]

(are they linear equations? quadratic equations? are they even one equation each? can I have inequalities?)

[Kenny Lau]

Could you clarify what you mean by a "decent math background"?

[Harith]

In my use case, the equations are linear equations and there aren't any inequalities.
By decent math background I mean undergraduate level math. Although I did not major in math.
Also what do you mean by "are they even one equation each?"?

Also yes, I am aware that one can just prove it with trivial. But I just wanted to illustrate what my end goal looks like.

[Kenny Lau]

@Harith if you have linear equations, then you can represent them with one matrix

[Kenny Lau]

Ax=v either has no solutions, one solution, or infinitely many solutions

[Kenny Lau]

Ax=0 either has one solution or infinitely many solutions

[Kenny Lau]

Harith said:

what do you mean by "are they even one equation each?"

In Lean, a proposition can pretty much be anything. A proposition is formally a term of type Prop. Term + type means whatever you put on the left vs. right of the colon. For example, "3 is a natural number" is represented as "3 : Nat", which means "3 is a term of type Nat".

A Prop can have one equal sign, two equal signs, anything in between, and many more. You can fit "sin(x)=0 and forall y, x+y=0 and exists z, z*z=0" all in one single proposition

[Kenny Lau]

These are the things you need to think about when you use Lean's type theory

[Kenny Lau]

what you're asking here... sounds like something like polyrith? basically you want a program to automatically determine (i.e. "calculate") if a set of linear equations is consistent?

[Harith]

Yeah, thats the ultimate goal

[Kenny Lau]

it's certainly within the realm of possibility, but idk who mainly deals with that part of the library, maybe other people can give you a more useful answer

[Kenny Lau]

I tried to demonstrate polyrith but it often has connection errors, lol

[Harith]

Yeah, I'll check out polyrith
thanks a ton

[Kenny Lau]

actually, linarith already exists for the negative case.

[Kenny Lau]

import Mathlib

example (x y : ℝ) (h1 : x = 10) (h2 : y = 15)
    (h3 : x + y = 25) (h4 : x - y = 2) : False := by
  linarith

[Aaron Liu]

linarith I think is complete for the theory of linear equations with rational coefficients in a linearly ordered ring

[Kenny Lau]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Tactic/Linarith/Frontend.html#Mathlib.Tactic.linarith

linarith attempts to find a contradiction between hypotheses that are linear (in)equalities.
Equivalently, it can prove a linear inequality by assuming its negation and proving False.

In theory, linarith should prove any goal that is true in the theory of linear arithmetic over
the rationals. While there is some special handling for non-dense orders like Nat and Int,
this tactic is not complete for these theories and will not prove every true goal. It will solve
goals over arbitrary types that instantiate LinearOrderedCommRing.

An example:

example (x y z : ℚ) (h1 : 2*x < 3*y) (h2 : -4*x + 2*z < 0)
        (h3 : 12*y - 4* z < 0) : False := by
  linarith

[Kenny Lau]

but linarith doesn't cover the positive case:

import Mathlib

example : ∃ (x y : ℝ), (x + y = 10) ∧ (x - 3 * y = 15) := by
  linarith -- fails

[Aaron Liu]

That docstring needs updating, since LinearOrderedCommRing is no longer a thing since #20676

[Kenny Lau]

presumably because you can just use wolframalpha/parigp to generate a solution and then plug it in

[Kenny Lau]

@Harith

[Harith]

Got it !
I'll check that out

[Harith]

Thanks !