## Stream: new members

### Topic: how to derive false from trivial inequalities

#### Tobias Grosser (Jun 19 2023 at 03:29):

I am trying to derive false from two trivial hypothesis. Would anybody be able to point me to the right tactic?

h₁: Bitvec.toNat C + i < w
h₂: ¬Bitvec.toNat C + i ≤ w
⊢ False


#### Niels Voss (Jun 19 2023 at 03:44):

Does linarith work?

#### Tobias Grosser (Jun 19 2023 at 03:46):

linarith gives me:

failed to synthesize
LinearOrder (Option Bool)


#### Tobias Grosser (Jun 19 2023 at 03:48):

I am trying to use exact absurd h₁ h₂, but for this to work, I would like to turn h₁ into h₁: Bitvec.toNat C + i <= w

#### Tobias Grosser (Jun 19 2023 at 03:48):

I am not yet sure how to do that.

#### Niels Voss (Jun 19 2023 at 03:49):

Either Nat.le_of_lt h₁ or h₁.le should work (though I'm not sure about the second one in Lean 4)

#### Yaël Dillies (Jun 19 2023 at 03:50):

They both work in Lean 4.

#### Kyle Miller (Jun 19 2023 at 03:50):

I'd guess exact absurd h₁.le h₂ might work. If it doesn't, an #mwe might help.

It does, indeed!

Thank you!

#### Niels Voss (Jun 19 2023 at 03:54):

Note that h₁.le works because it is shorthand for LT.lt.le h₁

#### Tobias Grosser (Jun 19 2023 at 03:56):

I guess as a step to understand this better, I am trying too simplify h₁ first and then trivially apply absurd.

#### Tobias Grosser (Jun 19 2023 at 03:57):

To get something in the form of
rw [LT.lt.le] h₁; exact absurd h₁ h₂, but this does not seem to work.

#### Niels Voss (Jun 19 2023 at 04:00):

rw doesn't work here because LT.lt.le is a one way implication, and rw only works with = and ↔ statements. You could instead directly write exact absurd (LT.lt.le h₁) h₂ (this is equivalent to what Kyle Miller suggested). You could also define a new hypothesis with
have h3 : Bitvec.toNat C + i ≤ w := LT.lt.le h₁; exact absurd h3 h2.

#### Tobias Grosser (Jun 19 2023 at 04:02):

Cool. That is super helpful. Thank you.

#### Tobias Grosser (Jun 19 2023 at 04:03):

I guess I now learned a little piece of lean code.

#### Alex J. Best (Jun 19 2023 at 14:25):

Tobias Grosser said:

linarith gives me:

failed to synthesize
LinearOrder (Option Bool)


Can you provide a MWE for this?

import Mathlib.Data.Bitvec.Defs
import Mathlib.Tactic.Linarith

lemma a (h₁: Bitvec.toNat C + i < w) (h₂: ¬Bitvec.toNat C + i ≤ w) :
False :=
by
linarith


works fine and I'd like to understand why linarith isn't working for you

Last updated: Dec 20 2023 at 11:08 UTC