Zulip Chat Archive

hi! I have a goal in which I want to rewrite (10 : fin 256).val to 10: image.png
I don't understand why simp doesn't do this. if I understand fin correctly, 10 : fin 256 is really a pair of a nat 10 and a proof that 10 < 256 right?

Lynn (Jul 09 2022 at 15:30):

this actually works somehow but I feel like there must be a better way?

  rw (show (10 : fin 256).val = 10, by refl),
  rw (show (97 : fin 256).val = 97, by refl),
  rw (show (87 : fin 256).val = 87, by refl),

Kevin Buzzard (Jul 09 2022 at 15:37):

These things are not just equal, they're definitionally equal, so you can probably use the change tactic if your goal is sufficently small.

import tactic

example (x : ℕ) : (10 : fin 256).val + x = x + 10 :=
begin
  change 10 + _ = _,
  apply add_comm,
end

-- or just don't change it at all
example (x : ℕ) : (10 : fin 256).val + x = x + 10 :=
begin
  apply add_comm,
end

Lynn (Jul 09 2022 at 15:46):

I see, thank you! so, here is my proof, let's see if I can simplify the proof a lot using change …

def nibble (n : fin 16) : fin 256 :=
  (if n < 10
    then ↑n + char.to_nat '0'
    else ↑n - 10 + char.to_nat 'a')

def nibble_alt (n : fin 16) : fin 256 := ↑n + (if n<10 then 48 else 87)

lemma nibble_eq : nibble = nibble_alt :=
begin
  funext, simp [nibble, nibble_alt],
  by_cases h: n < 10, rw if_pos h, rw if_pos h,
  rw (show '0'.to_nat = 48, by refl), simp,
  rw if_neg h, rw if_neg h, rw (show 'a'.to_nat = 97, by refl),
  norm_num,
  rw fin.eq_iff_veq,
  rw fin.add_def,
  rw fin.add_def,
  rw fin.sub_def,
  rw nat.mod_add_mod,
  rw add_assoc,
  rw (show (10 : fin 256).val = 10, by refl),
  rw (show (97 : fin 256).val = 97, by refl),
  rw (show (87 : fin 256).val = 87, by refl),
  rw nat.mod_eq_sub_mod,
  norm_num, rw ←nat.sub_add_comm, transitivity 256 + 97 - 10,
  norm_num, simp, norm_num,
end

Lynn (Jul 09 2022 at 15:47):

comments/suggestions are very welcome, it feels like it's 3x as long as it should be :exhausted: it always feels like maybe I am not utilising the full power of Lean

Ruben Van de Velde (Jul 09 2022 at 15:48):

Can dec_trivial solve it?

Lynn (Jul 09 2022 at 15:48):

wow! it can! what is this amazing tactic?

Ruben Van de Velde (Jul 09 2022 at 15:50):

It's lean just enumerating all the possible values of fin

Lynn (Jul 09 2022 at 15:50):

wow, cool, I was silently wondering the whole time if it could do that

Ruben Van de Velde (Jul 09 2022 at 15:52):

(the more there is to enumerate, the slower it gets, of course, so that's something to look out for)

Lynn (Jul 09 2022 at 15:59):

hmm… maybe I should browse more tactics, instead of browsing mathlib docs for the next super-low-level nat/fin lemma that gets me a little bit closer to the goal, which is what I spent most of my time doing when writing proofs in Lean

Ruben Van de Velde (Jul 09 2022 at 16:00):

Both can be useful, certainly

Lynn (Jul 09 2022 at 16:00):

I just now learned that there is a plugin(?) to make norm_num work with fin, that should be super helpful too

Kyle Miller (Jul 09 2022 at 16:13):

@Yakov Pechersky Is it within scope to have norm_fin be able to handle the coercion to nat? For example,

example : ((10 : fin 256) : ℕ) = 10 :=
begin
  norm_fin,
end

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib