feat: add support for Fin to omega

[dupuisf]

With this PR, omega can handle equalities and inequalities about variables in Fin n. For i : Fin n it will add both (i : Int) + 1 ≤ n and 0 ≤ i to the facts that are processed.

[dupuisf]

awaiting-review

[kim-em]

Thinking about this some more, I'm unconvinced we're ready to add support for Fin.

The current PR doesn't support having goals in Fin, e.g. even

example (i j : Fin n) (w : i < j) : i < j := by omega

would fail. That itself is easy to fix; I have it locally.

However if a user sees that working I think they would expect also to be able to use arithmetic operations in Fin, e.g.

example (i j : Fin n) (w : i.succ < j.succ) : i < j := by omega
example (i j : Fin n) (w : i + i < j) : i < j := by omega

However it would be a fair bit more work to support this. (e.g. addition in Fin is saturating, so involves a case split).

I'd prefer to not scope keep until we can provide a good experience with Fin!

Can you show me where you wanted to use omega that prompted this PR?

Second thoughts!

[dupuisf]

I considered also making it work for arithmetic operations on Fin, but as you say it would be a fair bit of work, and I don't get the sense that it's used all that much. (Also, addition in Fin is not saturating, #eval (2 : Fin 3) + (1 : Fin 3) gives me 0.) The fact that it doesn't work for literals at the moment is a bigger issue I think.

I'm currently working on a project that involves vectors of type Fin k → R and goals where omega doesn't work directly show up fairly often; even a quick fix that doesn't solve everything would be great.

Regarding the "proper" way to handle this eventually, I think it would be worth thinking about a way to make it extensible to be able to support types that are not in Std, like e.g. ZMod.

[kim-em]

I think the right strategy might just be some preprocessing tactics that are not part of omega, e.g. unfold_fin_arith which transforms the context by replacing all facts / goals about Fin with the corresponding statements in Nat.

[kim-em]

I pushed some changes, but I'm not happy yet. :-)

[dupuisf]

Fair enough. I've been experimenting some more with the aesop approach for preprocessing, and that seems to work well enough. In any case, feel free to either adopt this PR or close it entirely.

[kim-em]

@dupuisf, I've moved this to Lean: leanprover/lean4#3427

It seems to work quite well now.

[dupuisf]

@dupuisf, I've moved this to Lean: leanprover/lean4#3427

It seems to work quite well now.

I just noticed this with the announcement today, somehow I had missed this message -- very nice! :-)