how to derive false from trivial inequalities

Stream: new members

[Tobias Grosser]

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]

Does linarith work?

[Tobias Grosser]

linarith gives me:

failed to synthesize
  LinearOrder (Option Bool)

[Tobias Grosser]

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]

I am not yet sure how to do that.

[Niels Voss]

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]

They both work in Lean 4.

[Kyle Miller]

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

[Tobias Grosser]

It does, indeed!

[Tobias Grosser]

Thank you!

[Niels Voss]

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

[Tobias Grosser]

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

[Tobias Grosser]

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]

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]

Cool. That is super helpful. Thank you.

[Tobias Grosser]

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

[Alex J. Best]

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