Omega + Decide

Stream: lean4

[Siddharth Bhat]

I've started to get goal states that contain boolean combinations of decide of arithmetic statements:

example {i w : Nat} (h : (i < w + 1) ∧ (w ≤ w - i)) : (i = 0) := by
  omega

example (i w : Nat) : decide (i < w + 1) && (w ≤ w - i) = (i = 0) := by
  omega -- omega did not find a contradiction: trivial

I'm wondering what the correct approach to this is. am I using omega incorrectly, and it should be able to solve this?

Implementation-wise, I guess we would want to teach omega to try and convert decide(P) when P is arithmetic into a case split over P plus a call to omega?

[Geoffrey Irving]

What does simp? produce for the second example?

[Siddharth Bhat]

that is indeed correct, I can just run a simp. I ought to have tried that, duh!

[Siddharth Bhat]

Thanks!

[Siddharth Bhat]

Hmm, this does not seem to help with the larger goal state that I have from which I MWE'd this:

theorem intMin_getMsb (w : Nat) : (intMin (w+1)).getMsb i = decide (i = 0) := by
  simp [intMin, getMsb, getLsb, Nat.testBit_one_eq]
  -- ▶ 1 goal
  -- i w : Nat
  -- ⊢ (decide (i < w + 1) && (decide (w - i < w + 1) && (decide (w ≤ w - i) && decide (w - i - w = 0)))) = decide (i = 0)

[Siddharth Bhat]

@Geoffrey Irving any idea what's going on in this case?

[Geoffrey Irving]

In that case I (perhaps ignorantly) usually use simp lemmas in reverse, in particular Bool.decide_and and friends. Then you'll end up with decide ... = decide ..., which will simplify to a non-decide thing. But using simp lemmas in reverse is a bit ugly, so I'm not sure this approach is optimal.

[Kim Morrison]

Yes, currently omega doesn't like decide.

[Kim Morrison]

It does limited propositional reasoning, but the goals have to be expressed in Prop, not Bool.

[Kim Morrison]

I'm not intending to change this until (hopefully soon) we have sat available, after which we will make it work properly.

[Kim Morrison]

I would like to have good simp sets for "working in the opposite direction". E.g simp only [bool_to_prop] and simp only [prop_to_bool].

[Kim Morrison]

We've made a small start on the direction with the bv_toNat simp set in core for "converting BitVec goals to Nat goals, and pushing BitVec.toNat inwards", which is essentially the preprocessor for bv_omega.