Fin < automation

Stream: mathlib4

[James Gallicchio]

is linarith expected to work on simple goals involving Fin terms? MWE:

example (a b c : Fin n) (h1 : a < b) (h2 : b < c) : a < c := by
  linarith -- no contradiction found

I don't know how linarith works, it's just my default tactic for goals that feel linear.

Aside: aesop also does not work here without marking lt_trans as an aesop lemma. Is this a bad idea to do locally (or in mathlib)?

attribute [aesop unsafe apply] lt_trans
example (a b c : Fin n) (h1 : a < b) (h2 : b < c) : a < c := by
  aesop

[Kevin Buzzard]

The < on Fin n is pathological in the sense that it does not play well with $+$ or $\times$ (arithmetic), so I would very much doubt that linarith would work on Fin n. It seems to me that you want some kind of "partial order" or "total order" tactic, but I should think that you could knock one off yourself with apply_rules -- in fact there was a discussion about this recently (I'll try and find it) (it was here )

[Kim Morrison]

This really should be in scope for omega...

[Kyle Miller]

Here's a trick:

import Mathlib.Tactic

example {n : Nat} (a b c : Fin n) (h1 : a < b) (h2 : b < c) : a < c := by
  revert n
  simp [Fin.forall_iff]
  intros
  linarith

(A link to related discussion)

[Johan Commelin]

Should there be a version of zify for subtypes?

[Johan Commelin]

In fact, maybe there should be a general ambient_typify tactic, takes a type Y, realizes the goal is about terms in type X, finds a coercion X -> Y, and looks up suitable norm_cast lemmas to transform the goal into something about terms in type Y.

[Johan Commelin]

That would generalize zify and friends...

[Johan Commelin]

And then one could hope that a goal like in OP would be ambient_typify Nat ; omega

[Johan Commelin]

(Which isn't to say that in this specific case omega shouldn't be able to close it on its own...)

[James Gallicchio]

Johan Commelin said:

Should there be a version of zify for subtypes?

I think that would be quite useful for CS proofing

[Johan Commelin]

Maybe coerce would be a better name than ambient_typify. Then zify would be spelled coerce \Z.

[Terence Tao]

coerce_to, perhaps? I don't know how feasible this would be to implement, but it would be a natural tool to have.

[Yaël Dillies]

Now that we have zify, qify, rify, it might be worth thinking about unifying those tactics.

[Eric Wieser]

The approach in general is to apply infectivity of the coercion then use push_cast

[Yaël Dillies]

And I've been asking for a similar tactic for the coercion Finset α → Set α for a while now.

[Jannis Limperg]

James Gallicchio said:

Aside: aesop also does not work here without marking lt_trans as an aesop lemma. Is this a bad idea to do locally (or in mathlib)?

attribute [aesop unsafe apply] lt_trans
example (a b c : Fin n) (h1 : a < b) (h2 : b < c) : a < c := by
  aesop

Transitivity lemmas are no good as global Aesop rules because they always apply but are rarely useful. In other words, all your unsuccessful Aesop calls will time out after ~200 lt_trans applications.

However, adding transitivity lemmas locally, when you know a specific theorem needs them, is fine:

example (a b c : Fin n) (h1 : a < b) (h2 : b < c) : a < c := by
  aesop (add 1% lt_trans)

[Anne Baanen]

Eric Wieser said:

The approach in general is to apply infectivity of the coercion then use push_cast

If we want to do this, definitely look at the transfer tactics in other provers. I think a few are simply called transfer and also trocq is interesting.

[Kevin Buzzard]

Another potential example not mentioned yet is natify to move from PNat to Nat, which I needed recently.

[Johan Commelin]

I guess that falls under the Subtype class?