Stream: new members

Topic: Using norm_fin

Cactus (Anton) Golov (Feb 07 2022 at 16:55):

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


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 (Feb 07 2022 at 17:10):

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,


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

Filippo A. E. Nuccio (Feb 07 2022 at 17:11):

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 (Feb 07 2022 at 17:13):

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 (Feb 07 2022 at 17:14):

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 (Feb 07 2022 at 17:14):

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 (Feb 07 2022 at 17:17):

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 (Feb 07 2022 at 17:23):

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

Cactus (Anton) Golov (Feb 07 2022 at 17:24):

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

Cactus (Anton) Golov (Feb 07 2022 at 17:58):

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!

Last updated: Dec 20 2023 at 11:08 UTC