Struggling to prove this very basic `Fin` lemma

Stream: new members

[Malcolm Langfield]

Is there a tactic that can resolve something like this right away? (It is true, right?)

import Mathlib

lemma thing {n : Fin 20} (h : n ≥ 4) : n - 1 ≥ 3 := by
  rw [ge_iff_le] at *
  rw [le_iff_exists_add] at h
  sorry

[Andrea Bourque]

using 1 I think?

[Andrea Bourque]

Sorry, use 1, or at least that's how it was in Lean 3

[Malcolm Langfield]

That doesn't quite work. I thought use was for proving existentials?

[Andrea Bourque]

a >= b means (or is equivalent to) there exists a non-negative c such that a = b+c.
And I was mistaken. It should be something like this:

cases h with c hc
use c

the first line gives you hc: n = 4 + c, and then the second line makes your goal n-1 = 3 + c. From there you can rw hc and then simp.
Let me know if that works

[Andrea Bourque]

Ugh, looks like I might be mistaken on how cases works in Lean 4. Maybe.

[Malcolm Langfield]

Looks like it gives a dependent elimination error.

[Newell Jensen]

Andrea Bourque said:

Ugh, looks like I might be mistaken on how cases works in Lean 4. Maybe.

cases' h with c hc

[Riccardo Brasca]

Are you doing the NNG or working in mathlib? The definition of ≤ is not the same (but of course the two are equivalent).

[Malcolm Langfield]

Working in mathlib!

[Malcolm Langfield]

cases' h with c hc - This similarly gives a dependent elimination error.

[Riccardo Brasca]

Then you can first of all do rw [le_iff_exists_add] at h to get the version with ∃

[Riccardo Brasca]

a ≤ b ↔ ∃ (c : α), b = a + c is true by definition in the NNG, but it is a theorem in mathlib, so cases doesn't work.

[Malcolm Langfield]

n : Fin 20
h : 4 ≤ n
⊢ 3 ≤ n - 1

▶ 331:7-331:24: error:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?m.74853 ≤ ?m.74854

The le_iff_exists_add lemma also does not work. So I guess the answer is no, there is not anything that can resolve this automatically? I was surprised aesop couldn't do it out of the box either.

[Riccardo Brasca]

Can you write a #mwe?

[Newell Jensen]

Malcolm Langfield said:

cases' h with c hc - This similarly gives a dependent elimination error.

That comment was just for the syntax.

[Riccardo Brasca]

Wait, sorry, n has type Fin 20!

[Riccardo Brasca]

Is this

lemma thing {n : Fin 20} (h : n ≥ 4) : n - 1 ≥ 3 := by
  sorry

really what you want?

[Malcolm Langfield]

Yes, I mean it doesn't have to be exactly 20, but some Fin.

[Malcolm Langfield]

It does say Fin in the title. I edited the OP to give a MWE!

[Riccardo Brasca]

Sorry, my fault.

[Malcolm Langfield]

All good all good! :smile:

[Riccardo Brasca]

Then first of all you can use docs#Fin.le_iff_val_le_val

[Riccardo Brasca]

to get rid of Fin

[Malcolm Langfield]

Thanks! That gets me to here, and then it looks like I need some sort of val_sub lemma that doesn't exist.

n : Fin 20
c : ℕ
h : ↑n = ↑4 + c
⊢ ↑(n - 1) = ↑3 + c

[Malcolm Langfield]

And it shouldn't exist, right? I don't think such a lemma would be true when n is 0.

[Riccardo Brasca]

Well, it's a little tricky

[Riccardo Brasca]

let me see

[Riccardo Brasca]

You can do something like this

import Mathlib

lemma thing {n : Fin 20} (h : n ≥ 4) : n - 1 ≥ 3 := by
  rw [ge_iff_le, Fin.le_iff_val_le_val, le_iff_exists_add] at h ⊢
  obtain ⟨k, hk⟩ := h
  use k
  by_cases h0 : n = 0
  · exfalso
    rw [h0] at hk
    change 0 = 4 + k at hk
    linarith
  · rw [Fin.coe_sub_one, if_neg h0, hk, add_comm, add_comm _ k, Nat.add_sub_assoc]
    · rfl
    · show 1 ≤ 4
      norm_num

[Riccardo Brasca]

It's tricky because you play with subtraction on Fin, that is not very well behaved (what is 0 - 1?)

[Riccardo Brasca]

How did you end up with such a goal?

[Andy Jiang]

Riccardo Brasca said:

It's tricky because you play with subtraction on Fin, that is not very well behaved (what is 0 - 1?)

(I'm a newbie) shouldn't this just be 0 :Fin _ ? Also is it possible to modify the omega tactic to also solve things involving Fin _ ? Like if the type was N, omega would have finished immediately right?

[Malcolm Langfield]

I have gotten here:

⊢ k + ↑4 - 1 = ↑3 + k

▶ 342:9-342:25: error:
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ?a + ?b - ?c

But add_sub_assoc' is not working when I believe it should.

[Riccardo Brasca]

I've posted a full proof above.

[Malcolm Langfield]

@Andy Jiang 0 - 1 is 19 in this case, because we are working in Fin 20.

[Malcolm Langfield]

Oh thanks! I've never seen the change tactic before!

[Riccardo Brasca]

It's possible that a smart use of fin_cases can close the goal immediately, but I think the real point is why you want to prove this.

[Malcolm Langfield]

I work with Lean in industry, this came up in a program verification problem.

[Andy Jiang]

Malcolm Langfield said:

Andy Jiang 0 - 1 is 19 in this case, because we are working in Fin 20.

Ah so the goal is actually false when 20 is changed to 4?

[Riccardo Brasca]

Yes, it is false.

import Mathlib

lemma thing' : ¬(∀ (n : Fin 4), n ≥ 4 → n - 1 ≥ 3) := by
  by_contra h
  have : (4 : Fin 4) = 0 := rfl
  specialize h 1
  rw [this] at h
  simp at h
  have : (3 : Fin 4) ≠ 0 := by decide
  contradiction

[Riccardo Brasca]

Indeed slim_check works here.

import Mathlib

lemma thing {n : Fin 4} (h : n ≥ 4) : n - 1 ≥ 3 := by
  slim_check


===================
Found problems!
n := 1
guard: 0 ≤ 1
issue: 3 ≤ 0 does not hold
(0 shrinks)
-------------------

[Yakov Pechersky]

I have the Fin version of the exists add in #9033 https://github.com/leanprover-community/mathlib4/pull/9033/files#diff-6ae63812d312aba302a17e36f91f095aee62f00d3cb2f4966f176ea040474db6R1338

[Malcolm Langfield]

Thanks very much for all your help guys!!

[ZHAO Jiecheng]

A little more straight proof.

theorem thing {n : Fin 20} (h : n ≥ 4) : n - 1 ≥ 3 := by
  apply Fin.le_iff_val_le_val.mpr
  rw [Fin.coe_sub_iff_le.mpr]
  have : n.val - 1 ≥ 3 := by
    rw [show 3 = 4 - 1 by simp]
    exact Nat.sub_le_sub_right h 1
  exact this
  apply le_trans _ h
  decide

[ZHAO Jiecheng]

Riccardo Brasca said:

Indeed slim_check works here.

import Mathlib

lemma thing {n : Fin 4} (h : n ≥ 4) : n - 1 ≥ 3 := by
  slim_check


===================
Found problems!
n := 1
guard: 0 ≤ 1
issue: 3 ≤ 0 does not hold
(0 shrinks)
-------------------

lemma things {n : Nat} (h : n ≥ 4) : n - 1 ≥ 3 := by
  slim_check

The slim_check close the goal and say no goals to be solved with a red line. Is the proof finished? Or it is some kind of another sorry.

[Kevin Buzzard]

slim_check won't solve any goals (as far as I know), it only finds a counterexample or fails to find one and gives up with a kind of sorry.