Why do I need to unfold here?

Stream: new members

[Bolton Bailey]

I got tripped up on the example below. myType is defined as a pair, but that it is or what it's a pair of is actually totally irrelevant to the lemma I'm proving. You can see the monad does not use the A,B values it unpacks. Yet it is still necessary to unfold the definition for the code to work. Why is this?

import Mathlib

def myType := ℕ × ℕ

example {F: Type} (a : F) :
    (fun stmt : myType =>
      (StateT.run (σ := List (List (F))) (m := Id) (α := Unit)
          (match stmt with
          | (A, B) => do
            let x ← get
            set ([] :: x)
            let x ← get
            set ([] :: x)
            let x ← get
            set ((a :: List.headD x []) :: List.tailD x [])
            let x ← get
            set ((a :: List.headD x []) :: List.tailD x [])
            let x ← get
            set ([] :: x)
            let x ← get
            set ([] :: x)
            let x ← get
            set ([] :: x)
            let x ← get
            set ((a :: List.headD x []) :: List.tailD x [])
            let x ← get
            set ([] :: x)
            let x ← get
            set ((a :: List.headD x []) :: List.tailD x []))
          [[]]).snd) =
    fun x => [[a], [a], [], [], [a, a], [], []] := by
  simp -- Doesn't do what I want
  unfold myType -- ???
  simp -- Now it does what I want

[Bolton Bailey]

Indeed, if I replace (A,B) with A it works on the first simp (unfortunately I don't think I can do this in my real code because the unpacking arises from a definition which is important for other things).

[Matt Diamond]

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20power.20of.20a.20type.20using.20cartesian.20product/near/419134912

[Matt Diamond]

Eric Wieser said:

def Foo : Type := Bar roughly means "forget everything you know about Bar other than how it is represented"

[Matt Diamond]

oh wait, sorry, I just misread your question

[Matt Diamond]

you're saying you understand the behavior of def but you're still not sure why it matters in this case?

[Bolton Bailey]

Yes

[Bolton Bailey]

I don't understand why it affects how simp works here. The whole do expression never references the arguments from that function which returns it.

[Bolton Bailey]

Frankly, I don't understand why, when I have a match expression like that, it doesn't just automatically disappear with simp.