How to quickly show Fin sub ne itself

Stream: new members

[Mathias Sven]

I have been struggling with this for a bit. I am not sure how one it supposed to quickly show or observe the fact that $a - x \ne a$ where $x$ is sum OfNat of the same Fin n as $a$ where $x \lt n$ and $x \ne 0$.

As an example, I have this in my environment:

h1 : 2 ≤ n ∧ n ≤ 5000
h2 : m = 2 * n
atLeastFour : 4 ≤ m
instAtLeastTwo : m.AtLeastTwo
instNeZero : NeZero m

The atLeastFour and instAtLeastTwo I only derived in hopes that it would make this process easier.
I just need a proof that $i - 1 \ne i$ and $i - 2 \ne i$ where i : Fin m, in a way that is mostly automatic or at most one line.

[Aaron Liu]

can you provide a #mwe

[Mathias Sven]

Yes one second

[Mathias Sven]

Aaron Liu said:

can you provide a #mwe

I am not sure what properties I need to double check, so my MWE is in context to what I was trying do. Here the Lean 4 Web Link. Ideally, all those haves would be trivially true.

[Aaron Liu]

why are you using Fin.ofNat

[Mathias Sven]

Do you mean just using i - 1 in general?

[Aaron Liu]

no, I mean specifically the let i := Fin.ofNat nums.size i

[Mathias Sven]

Ah, because in the original code I wanted to imitate wrap around indexing of arrays like you might have in some other languages

[Aaron Liu]

but it never wraps around?

[Mathias Sven]

It wraps when i = 0

[Aaron Liu]

i ∈ [:nums.size]

[Aaron Liu]

so Fin.ofNat never wraps

[Mathias Sven]

I am not sure if I understand. Does the loop not start with i = 0? Then (0 : Fin nums.size) - 1 should be the last index

[Mathias Sven]

I suppose it never wraps around in the MWE you are right, I still had the original code in mind...

[Mathias Sven]

In the original code it wraps on line 56.

[Aaron Liu]

no I mean

[Aaron Liu]

if i ∈ [:nums.size]

[Aaron Liu]

then i < nums.size

[Aaron Liu]

so Fin.ofNat nums.size i doesn't wrap the value of i

[Aaron Liu]

because i was already less than nums.size

[Aaron Liu]

does that make sense?

[Mathias Sven]

Yes, but I wanted nums[i - x] to wrap, if I drop that line than any natural offset requires a proof of it being part of the interval and no longer wraps automatically

[Mathias Sven]

I did it as a coercion

[Aaron Liu]

so what you want to do here is use Fin.mk instead of Fin.ofNat

[Aaron Liu]

because Fin.ofNat is for when you don't know the number is below the bound so you want to wrap it if it's too big

[Mathias Sven]

I might be using this wrong, but before I did indeed have Fin.mk, like this:
let i := Fin.mk i (Membership.get_elem_helper h rfl)
But it seemed more cumbersome and I didn't seem to lose any information. Now i : Fin [:nums.size].stop which should be the same as Fin nums.size

[Mathias Sven]

It doesn't seem to change how one might get $i - 1 \ne i$

[Aaron Liu]

well it makes it a lot easier to show i.val = i✝

[Aaron Liu]

I guess yeah you're right it doesn't change how to show i - 1 ≠ i

[Mathias Sven]

Is this perhaps simply a case of Mathlib not having these lemmas? Or no easy chain to leads to it? Perhaps there really isn't a "quick" way to show this yet

[Mathias Sven]

I used LeanSearch and Moogle for quite a bit but couldn't find anything

[Aaron Liu]

while I wouldn't call this "quick" it's not really long either:

import Mathlib

def foo
  (nums : Array Int32)
  {n : ℕ}
  {h1 : 2 ≤ n ∧ n ≤ 5000}
  {h2 : nums.size = 2 * n}
  : ℕ := Id.run do
  -- have atLeastFour : 4 ≤ nums.size := by omega
  -- have instAtLeastTwo : nums.size.AtLeastTwo := ⟨by omega⟩
  have instNeZero : NeZero nums.size := ⟨by omega⟩

  for h : i in [:nums.size] do
    let i : Fin nums.size := ⟨i, Membership.get_elem_helper h rfl⟩

    have : i - 1 ≠ i := by
      rw [ne_eq, sub_eq_self, ← Fin.val_inj]
      simp
      lia
    have : i - 2 ≠ i := by
      rw [ne_eq, sub_eq_self, ← Fin.val_inj]
      -- simp?
      simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod]
      rw [Nat.mod_eq_of_lt (by grind)]
      simp
    have : i - 3 ≠ i := by
      rw [ne_eq, sub_eq_self, ← Fin.val_inj]
      -- simp?
      simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod]
      rw [Nat.mod_eq_of_lt (by grind)]
      simp
  0

[Ruben Van de Velde]

By the way, to make your question a minimal working example, you'd at least trim the monad stuff:

import Mathlib

example
    (nums : Array Int32)
    {n : ℕ}
    {h1 : 2 ≤ n ∧ n ≤ 5000}
    {h2 : nums.size = 2 * n}
    (i) (hi : i ∈ [:nums.size]) :
    True := by
  -- have atLeastFour : 4 ≤ nums.size := by omega
  -- have instAtLeastTwo : nums.size.AtLeastTwo := ⟨by omega⟩
  have instNeZero : NeZero nums.size := ⟨by omega⟩

  let i : Fin nums.size := ⟨i, Membership.get_elem_helper hi rfl⟩
  have : i - 1 ≠ i := by
    simp
    grind
  have : i - 2 ≠ i := by
    sorry
  have : i - 3 ≠ i := by
    sorry
  trivial

[Mathias Sven]

I see, before I did get to the ⊢ ¬2 % nums.size = 0 stage, but stopped because I didn't see a quick way of closing the goal. I suppose I just needed 2 more lines. Thanks for the help!

[Mathias Sven]

Yes apologies, I only did the monad to get the constraints imposed by the for loop. I wasn't super sure if that would be relevant or not

[Mathias Sven]

I ended up making this lemma:

lemma Fin.sub_ne_self
  {n : ℕ} [NeZero n] (a : Fin n)
  (b : ℕ) (h : b < n := by omega) [NeZero b] :
  a - OfNat.ofNat b ≠ a := by
  rw [ne_eq, sub_eq_self, ← Fin.val_inj]
  simp only [Fin.coe_ofNat_eq_mod, Nat.zero_mod]
  rw [Nat.mod_eq_of_lt (by grind)]
  have hb := (Nat.pos_of_neZero b).ne.symm
  simp [ne_eq]; exact hb

For more ergonomics