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

Stream: new members

[Miguel Negrão]

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)
inst✝¹: Monad m
inst✝: LawfulMonad m
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...

[Miguel Negrão]

full code here.

[Jireh Loreaux]

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]

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]

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]

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

[Kevin Buzzard]

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

[Jireh Loreaux]

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

[Miguel Negrão]

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

[Jireh Loreaux]

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

[Jireh Loreaux]

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

[Miguel Negrão]

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]

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]

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]

while Prod.eta does...

[Miguel Negrão]

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]

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]