Tactic for solving simple inequalities?

Stream: new members

[Philogy]

What tactics are there that would solve the goal to yield the:

Nat.lt_trans
        (Nat.mod_lt (a * b) ne_zero)
        m.isLt

automatically? It's relatively simple now but it took me quite some time to figure out what lemmas and structures to use to get it to work. The typical tactics like linarith or aesop don't seem to fair well at this. Any I'm missing? It seems like fairly trivial proof that it should be automatable.

abbrev UInt256 := BitVec UInt256.width
abbrev UInt256.width := 256
abbrev UInt256.size := 2^UInt256.width

def evm_mulmod (x y m: UInt256): UInt256 :=
  if ne_zero: m > 0
  then
    let a := x.toNat
    let b := y.toNat
    ⟨
      (a * b) % m.toNat,
      Nat.lt_trans
        (Nat.mod_lt (a * b) ne_zero)
        m.isLt
    ⟩
  else 0

[Henrik Böving]

Your file isn't a #mwe, UInt256 doesn't exist in ordinary Lean

[Kyle Miller]

(We ask that people give a working example so that we can copy/paste it and try to give a precise answer.)

[Philogy]

Henrik Böving said:

Your file isn't a #mwe, UInt256 doesn't exist in ordinary Lean

The definition of UInt256 is in my example?

[Henrik Böving]

Oh i oversaw that sorry

[Henrik Böving]

The only simplification I could think of would be

      by
        have := Nat.mod_lt (a * b) ne_zero
        have := m.isLt
        omega

If you were to stay in the bitvec fragment you could also use bv_decide though that might be a bit of a sledgehammer for such a simple problem

[Philogy]

Henrik Böving said:

The only simplification I could think of would be

      by
        have := Nat.mod_lt (a * b) ne_zero
        have := m.isLt
        omega

If you were to stay in the bitvec fragment you could also use bv_decide though that might be a bit of a sledgehammer for such a simple problem

Ah thanks, didn't know about the omega, is there a page of tactics like omega, linarith, aesop that help with automating the theorem-proving process?

Also FYI I found that the following also works:

      by
        have := Nat.mod_lt (a * b) ne_zero
        omega

[Henrik Böving]

Ah I guess omega also knows about the size of BitVecs mhm

[Henrik Böving]

there is an ever growing page of built in tactics in the reference manual https://lean-lang.org/doc/reference/latest/ but linarith and aesop aren't built in

[Alex Mobius]

How is that document not linked on the main site?.. I've been going off Lean 3's reference manual this whole time!

[Kyle Miller]

(It's in a public preview @Alex Mobius: https://leanprover.zulipchat.com/#narrow/channel/113486-announce/topic/Introducing.20the.20Lean.20Language.20Reference/near/478091276)