How do I unfold `.1`?

Stream: new members

[Richard Kiss]

I'm using UInt8for certain functions for efficiency which means there are a lot of casts which I fastidiously unfold until I get to .1. Then I'm stuck. How can I unfold this? The underlying type that has me stuck this time is Fin UInt8.size. I tried unfold Fin.val and simp [Fin.val] but nothing happens.

[Eric Wieser]

Can you make a #mwe?

[Richard Kiss]

at the core is a complex recursive function with multiple deep match branches, so it'll be challenging. But I'll try to create a smaller version that exhibits the issue

[Richard Kiss]

okay, I figured out what's up here. I had a definition def OP_SHA256 : UInt8 := 11 (an opcode) and I needed to unfold it. Computer programmer brain forgot constants work differently in lean

[Richard Kiss]

In my attempt at a more minimal example, I can get stuck at the same point, but rfl solves it. Is there a way to see what sub-tactics rfl uses so I try some of those?

[Richard Kiss]

I get to

int_to_atom ({ natCast := fun n ↦ Int.ofNat n }.1
   { ofNat := UInt8.ofNat 11 }.1.1.1) = instOfNatAtom.1

[Richard Kiss]

it seems like it's clear these are all constants, but simp [int_to_atom] just blows up to a big mess

[Richard Kiss]

okay, this has something to do with how OfNat works and how it "hides" the underlying Nat (11 in this case) in the instance function

[Richard Kiss]

Here's an #mwe:

example: Int.ofNat (Fin.val (UInt8.val (11: UInt8))) = 11 := by
  unfold UInt8.val
  unfold Fin.val
  sorry

It's easy to prove the example with rfl. But I eventually get stuck when using just unfold and simp.

[Richard Kiss]

one reduce does it! But reduce is not well documented and I don't yet know what it does

[Kevin Buzzard]

Is there a way to see what sub-tactics rfl uses so I try some of those?

show_term rfl. But all it does it tries to unify the goal with Eq.refl [LHS], it's not applying any sub-tactics AFAIK.

[Kyle Miller]

If you know what it's supposed to be, you can use the change tactic, which should be able handle anything rfl/reduce should

example: Int.ofNat (Fin.val (UInt8.val (11: UInt8))) = 11 := by
  change 11 = _
  sorry

[Kyle Miller]

It looks like simp is actually able to reduce this one, though perhaps using lemmas you don't have imported.

example (a : Int) : Int.ofNat (Fin.val (UInt8.val (11: UInt8))) = a := by
  simp?
  -- simp only [UInt8.val_val_eq_toNat, UInt8.reduceToNat, Int.ofNat_eq_coe, Nat.cast_ofNat]
  sorry

(the a is to prevent simp from proving it with rfl)

[Richard Kiss]

Here's the solution with just unfold and simp of the #mwe.

example: Int.ofNat (11: UInt8).val.val = (11: Int) := by
  unfold Fin.val
  unfold UInt8.val
  unfold UInt8.instOfNat
  unfold UInt8.ofNat
  unfold Fin.ofNat
  simp [Int.ofNat]

Now I just need to unwind the casting and get my mind around how that works.

[Matt Diamond]

a lot of unfolding is a code smell, IMHO... there should be APIs that make it easier to move between types

for example, if you want a UInt8 as an Int, you can just do Int.ofNat (11 : UInt8).toNat, and the example becomes

example : Int.ofNat (11: UInt8).toNat = (11: Int) := by simp

[Matt Diamond]

Of course it's a toy example and you could solve it with rfl, but I think it's instructive that simp works here while it fails to solve Int.ofNat (11: UInt8).val.val = (11: Int) without imports. Things are easier when you take advantage of functions that are designed to facilitate casting.

[Matt Diamond]

(And with imports, simp can solve your version thanks to docs#UInt8.val_val_eq_toNat, which re-writes it to use UInt8.toNat.)

[Richard Kiss]

I was on v4.6.1 and some of this stuff seems to only be in 4.7.0-rc2, so I'm upgrading