## Stream: new members

### Topic: Help with rw and simp and (x.fst, x.snd)

#### Miguel Negrão (Mar 31 2023 at 11:38):

I'm having trouble getting either rw or simp to substitute (x.fst, x.snd) by x. The goal I have is

(fun state => (fun x => pure (x.fst, x.snd)) <=< f state) = f

This is where I got from using simp, but simp doesn't appear to be able to go any further. If I was able then substitute (x.fst, x.snd) with x, then I can remove the lambda, and then I have pure <=< f state which should be easy to prove is f state, and then I would get f. But at the moment I'm stuck on rewriting (x.fst, x.snd) to x.

I've proved the following without issue with simp

have h : ∀x : Prod α β, (x.fst, x.snd) = x := by simp

But if I try to use that in the goal above with rw or simp it fails. For instance below is what happens with rw [h]

Main.lean:384:18
Tactic state
case cell.mk
bc: Type (u + 1)
m: Type (u + 1)  Type (u + 1)
h:  {α β : Type} (x : α × β), (x.fst, x.snd) = x
s: Type u
s: s
f: s  b  m (c × s)
(fun state => (fun x => pure (x.fst, x.snd)) <=< f state) = f
Messages (1)
Main.lean:384:16
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
(?x.fst, ?x.snd)
case cell.mk
m: Type (u + 1)  Type (u + 1)
h:  {α β : Type} (x : α × β), (x.fst, x.snd) = x
s: s
f: s  b  m (c × s)
(fun state => (fun x => pure (x.fst, x.snd)) <=< f state) = f

The type of x in fun x is c × s✝ so it should be a normal Prod.

I think I'm probably missing something...

full code here.

#### Jireh Loreaux (Mar 31 2023 at 12:40):

rw can't see under the binder, try using simp_rw. Or just forget the have h and instead of rw [h] you can just use simp only [Prod.mk.eta]

#### Miguel Negrão (Mar 31 2023 at 13:01):

simp_rw is from Mathlib, but if I import Mahtlib suddenly simp doesn't get hung up in the same place, it finishes the whole goal in one go. So it appears with Mathlib simp becomes more powerful !

theorem cell_id_comp {m : Type (u+1) -> Type (u+1)} [Monad m] [LawfulMonad m] (cell : Cell m b c) :  cellCatCompose cellCatId cell = cell := by
cases cell with
| arrm f => simp [cellCatCompose, cellCatId, Bind.kleisliLeft]
| cell p => simp [cellCatCompose, cellCatId, Bind.kleisliLeft]

Thanks for letting me know about simp_rw, it might come in handy in another situation where I need to do substitutions under binders.

#### Jireh Loreaux (Mar 31 2023 at 13:14):

You don't need simp_rw, simp only [h] should work (or whatever lemma simp calls to solve your have h). This should avoid you needing to make mathlib a dependency if you would prefer to avoid it.

It's not surprising that simp becomes more powerful with mathlib though: mathlib adds lots of @[simp] tagged lemmas.

#### Miguel Negrão (Mar 31 2023 at 14:20):

Without import Mathlib simp only [h]does not do anything to the goal...

#### Kevin Buzzard (Mar 31 2023 at 14:29):

You can use squeeze_simp to find out which lemmas are being used.

#### Jireh Loreaux (Mar 31 2023 at 14:30):

Kevin, this is Lean 4. I think it's simp? now.

#### Miguel Negrão (Mar 31 2023 at 14:33):

There is some subtle issue with my h, actually without using Mathlib simp only [Prod.eta] works.

#### Jireh Loreaux (Mar 31 2023 at 14:34):

The issue with your h is that you gave it for α β : Type not α β : Type _.

#### Jireh Loreaux (Mar 31 2023 at 14:35):

But docs4#Prod.eta is the right thing to use

#### Miguel Negrão (Mar 31 2023 at 14:41):

Ok, so after simp only [Prod.eta], simp doesn't do the eta reduction in

(p.fst, fun state => (fun x => pure x) <=< Prod.snd p state) = p

I mean changing (fun x => pure x) to pure. Should I pass an explicit eta reduction theorem to simp ? Btw, ading Prod.eta to the list of theorems I'm passing to simp also works, I don't need to use simp only apparently.

#### Miguel Negrão (Mar 31 2023 at 14:42):

But ok, the important thing here is that I got stuck because my version of Prod.eta didn't have the right universes.

#### Miguel Negrão (Mar 31 2023 at 14:44):

But even with the following version of h it doesn't work with simp:

have h  {α : Type _} {β : Type _} (p : α × β) : (p.1, p.2) = p := rfl

#### Miguel Negrão (Mar 31 2023 at 14:44):

while Prod.eta does...

#### Miguel Negrão (Mar 31 2023 at 14:47):

Similarly the following also doesn't manage to get simp to do the eta reduction...

have h2  {α : Type _} {β : Type _} (f : α → β) : (λ x ↦ f x) = f := rfl

I'm a bit lost here...

#### Miguel Negrão (Mar 31 2023 at 15:05):

Jireh Loreaux disse:

Kevin, this is Lean 4. I think it's simp? now.

Right, in lean 4 it's simp?. With that I can see what else I needed to add to make it work only in Lean 4 without Mathlib:

simp only [cellCatCompose, cellCatId, Bind.kleisliLeft, map_pure, Prod.eta, bind_pure]

Last updated: Dec 20 2023 at 11:08 UTC