Using norm_fin

Stream: new members

[Cactus (Anton) Golov]

Hi, I'm playing with this sudoku implementation in Lean and I occasionally run into the issue that expressions involving fins won't reduce. Cases like this:

import data.fin
import tactic.norm_num
import tactic.norm_fin

constant f : nat → Prop

example (n : fin 9) (Hn : n = 7) (H : f (↑(3 * (↑n / 3 % 3)) + 2)) : f 0 :=
begin
  rw Hn at H,
  norm_num at H,
  norm_fin at H,
end

(playground link)
Here, I'd like to eventually get H : f 8 as an assumption, but norm_num doesn't simplify that expression, and norm_fin gives me an "invalid begin-end expression, ',' expected" error that I don't understand.
Do I need to use norm_fin here, and if so, how? (Interestingly, for goals, norm_num seems to be enough.)

[Alex J. Best]

The issue is that norm_num doesn't know to apply docs#fin.coe_bit0 and bit1.
You can get it to do what you want with

  norm_num [fin.coe_bit0, fin.coe_bit1] at H,

instead.
norm_fin looks like it is useful when the whole expression lives in fin n rather than just some part.

[Filippo A. E. Nuccio]

Also, looking at docs#tactic.norm_fin.normalize_fin it seems that it can only normalize expression at the goals. This should be the reason for you error "invalid begin-end expression" because when it reads at H it does not understand what is going on.

[Cactus (Anton) Golov]

Hmm, for some reason adding [fin.coe_bit0, fin.coe_bit1] gives the error norm_num failed to simplify, even when just norm_num at H works.

[Cactus (Anton) Golov]

Filippo A. E. Nuccio said:

Also, looking at docs#tactic.norm_fin.normalize_fin it seems that it can only normalize expression at the goals. This should be the reason for you error "invalid begin-end expression" because when it reads at H it does not understand what is going on.

Ah, thanks, I see. That makes sense.

[Alex J. Best]

Full code:

import data.fin.basic
import tactic.norm_num
import tactic.norm_fin

constant f : nat → Prop

example (n : fin 9) (Hn : n = 7) (H : f (↑(3 * (↑n / 3 % 3)) + 2)) : f 0 :=
begin
  rw Hn at H,
  norm_num [fin.coe_bit0, fin.coe_bit1] at H,
end

[Cactus (Anton) Golov]

Oh, maybe this is due to me not knowing how modules work; I have data.fin instead of data.fin.basic, and when I try to import data.fin.basic I get "module not found in search path". Or is this just mathlib being out of date?

[Alex J. Best]

Yeah looks like it changed in #9524 which was a little while back

[Cactus (Anton) Golov]

Ah, thanks, I see. Let me try updating and seeing if that fixes it :) Thanks for the help!

[Cactus (Anton) Golov]

Thanks, it seems to work (though unfortunately it looks like the sudoku widget code seems to be broken by the update...)
Edit: ah no, seems like it works, awesome!