fin_cases on variables

Stream: Is there code for X?

[Yaël Dillies]

Imagine I have i j : fin 3 and I want to case on whether j = i, j = i + 1, j = i + 2. Could fin_cases handle that?

[Adam Topaz]

import tactic.fin_cases
import data.fin.basic

example (i j : fin 3) : true :=
begin
  have : i = j ∨ i = j+1 ∨ i = j+2, by { fin_cases i; fin_cases j; finish },
  sorry
end

Do you want anything beyond this?

[Yaël Dillies]

Oooh, very nice.

[Adam Topaz]

I don't know if this would scale to i j : fin 37.

[Eric Wieser]

Can't you case on j - i?

[Yaël Dillies]

This sounds like fin_cases could go faster on those things.

[Yaël Dillies]

In my case, casing on j = i isn't enough, no.

[Adam Topaz]

import tactic.fin_cases
import data.fin.basic

example (i j : fin 3) : true :=
begin
  have : i = j ∨ i = j+1 ∨ i = j+2,
  let k := j - i,
  fin_cases k,
  -- Is there a quick way to finish?
  sorry
end

[Yaël Dillies]

Exactly what I'm doing is having one i : fin 3, and then I need the other two elements j k : fin 3 to build a function fin 3 → ℕwhich then is equal to some other function by extensionality and by exhaustion of fin 3.

[Eric Wieser]

example (i j : fin 3) : j = i ∨ j+1 = i ∨ j+2 = i :=
begin
  -- there's probably a nicer way to do this
  let k := j - i,
  have : j = i + k := (add_sub_cancel'_right i j).symm,
  clear_value k,
  subst this,
  simp only [add_assoc, add_right_eq_self],
  fin_cases k; norm_num,
  -- :(
  sorry
end

norm_num doesn't know 1 + 2 = 0

[Eric Wieser]

In fact, it seems to be totally stuck on fin in general

[Rob Lewis]

import tactic.norm_fin?

[Rob Lewis]

import tactic.norm_fin tactic.fin_cases

example (i j : fin 3) : j = i ∨ j+1 = i ∨ j+2 = i :=
begin
  -- there's probably a nicer way to do this
  let k := j - i,
  have : j = i + k := (add_sub_cancel'_right i j).symm,
  clear_value k,
  subst this,
  simp only [add_assoc, add_right_eq_self],
  fin_cases k; norm_num,
end

is done.

[Eric Wieser]

Here's one possible nicer spelling:

lemma forall_add {G : Type*} [add_comm_group G] {P : G → Prop} (x : G) :
  (∀ y, P y) ↔ ∀ dx, P (x + dx):=
(equiv.add_left x).surjective.forall

example (i j : fin 3) : j = i ∨ j+1 = i ∨ j+2 = i :=
begin
  revert j,
  rw forall_add i,
  intros k,
  simp only [add_assoc, add_right_eq_self],
  fin_cases k; norm_num,
end

[Yaël Dillies]

I didn't know about tactic.norm_fin!

[Yaël Dillies]

It's pretty unreliable, however:

import tactic.norm_fin

example {i : fin 3} : i + 1 ≠ i := by norm_fin -- works
example {i : fin 3} : i + 2 ≠ i := by norm_fin -- fails
example {i : fin 3} : i + 3 = i := by norm_fin -- works
example {i : fin 3} : i + 4 ≠ i := by norm_fin -- works
example {i : fin 3} : i + 5 ≠ i := by norm_fin -- fails

[Yakov Pechersky]

Yes, that makes sense because 1, 4 are all normalized to 1, and we know that + 1 is not id. 3 is normalized to 0, and we know + 0 is id. But not the case for things that don't normalize to 1.

[Yakov Pechersky]

It'd be nice if norm_fin discharged something like ¬3 = 0 when both numerals are fin 37.

[Yakov Pechersky]

Otherwise, you can rely on fin_cases i; norm_fin