Zulip Chat Archive

Stream: new members

Topic: Coercion question


view this post on Zulip Dan Stanescu (Aug 04 2020 at 16:20):

I have the following in my context:

context.png

with the corresponding types:

xtxtype.png

I didn't find a way to obtain the goal, everything seems to fail (norm_cast, fin.coe_eq_val, fin.coe_fin_lt.mp). Does anyone see something that might work here?

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 16:20):

does exact h3 work?

view this post on Zulip Dan Stanescu (Aug 04 2020 at 16:20):

Nope

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:21):

apply h3?

view this post on Zulip Dan Stanescu (Aug 04 2020 at 16:21):

Funny I didn't try this last one. I'll give it a try in a sec.

view this post on Zulip Dan Stanescu (Aug 04 2020 at 16:22):

No, it doesn't.

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 16:22):

just bite the bullet and do cases on i and j

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:22):

finish would probably work :)

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 16:22):

I think h3 might say something like j % (n + 2) < (i + 1) % (n + 2) or something

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 16:23):

and you can prove j % (n + 2) = j by mod_lt or something

view this post on Zulip Dan Stanescu (Aug 04 2020 at 16:24):

Adam Topaz said:

finish would probably work :)

It doesn't. I wish it did.

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:24):

Oh, I see the coercion is going into fin (n+2). Missed that.

view this post on Zulip Dan Stanescu (Aug 04 2020 at 16:26):

Kevin Buzzard said:

I think h3 might say something like j % (n + 2) < (i + 1) % (n + 2) or something

Thanks, I'll have to try cases I guess. Maybe I get to see if there's a hidden problem somewhere in the process.

view this post on Zulip Shing Tak Lam (Aug 04 2020 at 16:56):

import data.fin tactic

example (n : ) (i j : fin n) (h : (j.val : fin (n+2)) < (i.val.succ : fin (n+2))) : j.val < i.val.succ :=
begin
  have h1 : (j.val : fin (n+2)).val = j.val,
  { rw fin.coe_val_of_lt (show j.1 < n + 2, by linarith [j.2]) },
  have h2 : (i.val.succ : fin (n+2)).val = i.val.succ,
  { rw fin.coe_val_of_lt (show i.1 + 1 < n + 2, by linarith [i.2]) },
  change (j.val : fin (n+2)).val < (i.val.succ : fin (n+2)).val at h,
  rwa [h1, h2] at h,
end

view this post on Zulip Reid Barton (Aug 04 2020 at 17:00):

This looks like a situation it would be better not to get into in the first place

view this post on Zulip Reid Barton (Aug 04 2020 at 17:03):

e.g. if h3 was stated in terms of things like cast_succ

view this post on Zulip Dan Stanescu (Aug 04 2020 at 18:26):

Reid Barton said:

e.g. if h3 was stated in terms of things like cast_succ

That h3 comes from something like this:

    rcases lt_trichotomy ((i+1) : fin (n+2) ) (j : fin (n+2)) with h1|h2|h3,

and is the one case that leads to false. I did expect to have trouble with it, the other two worked like a charm. How could I have done a better job with cast_succ?

view this post on Zulip Reid Barton (Aug 04 2020 at 18:36):

Don't write things like ((i+1) : fin (n+2)) (you implicitly used a coercion here) but instead use methods of fin designed for this purpose

view this post on Zulip Reid Barton (Aug 04 2020 at 18:37):

see the top of data.fin

view this post on Zulip Dan Stanescu (Aug 06 2020 at 14:23):

Reid Barton said:

Don't write things like ((i+1) : fin (n+2)) (you implicitly used a coercion here) but instead use methods of fin designed for this purpose

This is very good advice, unfortunately I just got it too late and am not sure what to do now. I have a rather dense 200-lines proof that hinges on this one sorry:

import data.fin
import tactic

lemma fin_lt_succ (n : ) (i : fin (n + 1)) : (i : fin (n+2)) < ((i+1) : fin (n+2)) := sorry

which I thought was easy when I outlined the proof, but it turns out I couldn't bring to completion (one of the ways I tried is below). Does anyone see how to finish this? I can't seem to figure out how to use an alternative at the place I need this.

lemma fin_lt_succ (n : ) (i : fin (n + 1)) : (i : fin (n+2)) < ((i+1) : fin (n+2)) :=
begin
    apply fin.lt_iff_val_lt_val.mpr,
    have h1 : i.val < n+2, linarith [i.2],
    have h2 := @fin.coe_val_of_lt (n+1) i.val h1,
    sorry,
end

view this post on Zulip Jalex Stark (Aug 06 2020 at 14:33):

import tactic

lemma fin_lt_succ (n : ) (i : fin (n + 1)) : (i : fin (n+2)) < ((i+1) : fin (n+2)) :=
begin
  apply fin.lt_iff_val_lt_val.mpr,
  convert nat.lt_succ_self _,
  sorry
end

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:18):

this is a nightmare to prove.

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:19):

The case i = 0 is defeq to 0 < (0 + (0 + 1) % (n + (0 + 1) + 1)) % (n + bit0 (0 + 1)),

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:20):

Just refactor, it will be easier and will save you more pain later

view this post on Zulip Shing Tak Lam (Aug 07 2020 at 11:24):

Fwiw I've proven this (PM with Dan). I have a better proof that doesn't use norm cast and things, but I'm on my phone rn.

lemma fin_lt_succ (n : ) (i : fin (n + 1)) : (i : fin (n+2)) < (i+1) :=
begin
  cases i with i hi,
  change (_ : fin (n+2)).val < (_ : fin (n+2)).val,
  simp only [fin.coe_mk, coe_coe],
  norm_cast,
  rw [fin.coe_val_of_lt, fin.coe_val_of_lt]; omega,
end

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:25):

nice!

view this post on Zulip Shing Tak Lam (Aug 07 2020 at 11:26):

There's a few more fin lemmas that I was gonna PR today, but my internet decided to not work very well. I'll try and PR these to mathlib tomorrow (should these be PR-ed?)

view this post on Zulip Dan Stanescu (Aug 07 2020 at 14:05):

Kevin Buzzard said:

this is a nightmare to prove.

I really think this would be useful in mathlib. finis a great type to have for finite-length sequences, as the discussion initiated by @Patrick Thomas about partitions/Riemann sums also suggests. This result is very helpful when working with strict_mono sequences, which will be needed in many circumstances, most probably including that case (refining partitions). Kudos @Shing Tak Lam !


Last updated: May 14 2021 at 00:42 UTC