coe trouble, i guess

Stream: new members

[jachym simon]

Hi, how can i prove the following?

import tactic

instance {n : ℕ} : has_coe (fin n) (fin n.succ) :=
by split; intro i; exact ⟨i.val, nat.lt.step i.property⟩

lemma lem1 (n : ℕ)(i : fin n)(h : (i : fin n.succ) = (n : fin n.succ)) : i.val = n :=
begin
sorry
end

[Eric Wieser]

I assume you're aware that both h and the goal are false?

[jachym simon]

Yes. I would like to show, that h implies false. Probably should have written it this way right away

import tactic

instance {n : ℕ} : has_coe (fin n) (fin n.succ) :=
by split; intro i; exact ⟨i.val, nat.lt.step i.property⟩

lemma lem1 (n : ℕ)(i : fin n)(h : (i : fin n.succ) = (n : fin n.succ)) : false :=
begin
sorry
end

[jachym simon]

I managed to get this far, but can't prove the sorry.

import tactic

instance {n : ℕ}: has_coe (fin n) (fin n.succ) :=
by split; intro i; exact ⟨i.val, nat.lt.step i.property⟩

lemma lem1 (n : ℕ)(i : fin n)(h : (i : fin n.succ) = (n : fin n.succ)) : false :=
begin
  have : i.val = n,
    simp * at *,
    have : (n : fin n.succ) = (⟨n, by omega⟩ : fin n.succ),
      sorry,
    unfold_coes at *,
    rw this at h,
    finish,
  linarith[(i.property), this]
end

[Chris B]

Not a big lean 3 user, but here's one way.

lemma lem1 (n : ℕ) (i : fin n) (h : (i : fin n.succ) = (n : fin n.succ)) : i.val = n :=
begin
  have h0 : (i : fin n.succ).val = (n : fin n.succ).val, from congr_arg subtype.val h,
  simp [nat.mod_eq_of_lt (nat.lt.base n)] at h0,
  unfold_coes at h0,
  rw [h0]
end

[jachym simon]

Cool, thank you :)

[jachym simon]

One more connected question. If i have open tactic in the same file, the unfold_coes goes red with an error. Why is that?

import tactic
open tactic

instance {n : ℕ}: has_coe (fin n) (fin n.succ) :=
by split; intro i; exact ⟨i.val, nat.lt.step i.property⟩

lemma lem1 (n : ℕ)(i : fin n)(h : (i : fin n.succ) = (n : fin n.succ)) : false :=
begin
  have : i.val = n,
    have h0 : (i : fin n.succ).val = (n : fin n.succ).val, from congr_arg subtype.val h,
    simp [nat.mod_eq_of_lt (nat.lt.base n)] at h0,
    unfold_coes at h0, -- error: unfold tactic failed, lift does not have equational lemmas nor is a projection
    rw [h0],
  linarith[(i.property), this]
end

[Alex J. Best]

Looks like a bug in https://github.com/leanprover-community/mathlib/blob/3ba1c0230e76b8dbd19cd2d2179cd102df533dfa/src/tactic/interactive.lean#L45-L48 (or unfold itself perhaps) I can try and take a look later if nobody else does first. In the meantime you can do something like open tactic (hiding lift) (I don't remember the exact sequence right now but hopefully you can find examples in mathlib)

[jachym simon]

ok, i will try that, thanks :) i dealt with it by putting the part of my code that needs open tactic in a separate section, which is not ideal but works for now