Subst with an expression

Stream: Is there code for X?

[Snir Broshi]

In foo I would like to rw [h] but "motive is not type correct" (using rw! does work, but Mathlib seems hesitant to adopt it, so I prefer not to use it).
Instead I can use foo_helper where the hypothesis is an equality of variables, so I can subst.
Is there a way to solve this directly in foo, perhaps using some generalize magic?

import Mathlib

variable {α β : Type*} {P : α → β → Prop} {Q : (a : α) → Sym2 { b : β // P a b } → Prop}

lemma foo_helper {a₁ a₂ : α} {b₁ b₂ : β} (h : a₁ = a₂) {h₁ h₂ h₃ h₄ h₅ h₆} :
    let T := Σ a : α, Subtype (Q a)
    (⟨a₁, s(⟨b₁, h₁⟩, ⟨b₂, h₂⟩), h₃⟩ : T) = ⟨a₂, s(⟨b₁, h₄⟩, ⟨b₂, h₅⟩), h₆⟩ := by
  subst h
  rfl

lemma foo {f : β → α} {b₁ b₂ : β} (h : f b₁ = f b₂) {h₁ h₂ h₃ h₄ h₅ h₆} :
    let T := Σ a : α, Subtype (Q a)
    (⟨f b₁, s(⟨b₁, h₁⟩, ⟨b₂, h₂⟩), h₃⟩ : T) = ⟨f b₂, s(⟨b₁, h₄⟩, ⟨b₂, h₅⟩), h₆⟩ := by
  exact foo_helper h

[Snir Broshi]

This becomes harder if I need another rewrite afterwards to finish, e.g. here's foo but with the pair on the RHS swapped so I need Sym2.eq_swap:

import Mathlib

variable {α β : Type*} {P : α → β → Prop} {Q : (a : α) → Sym2 { b : β // P a b } → Prop}

lemma foo2 {f : β → α} {b₁ b₂ : β} (h : f b₁ = f b₂) {h₁ h₂ h₃ h₄ h₅ h₆} :
    let T := Σ a : α, Subtype (Q a)
    (⟨f b₁, s(⟨b₁, h₁⟩, ⟨b₂, h₂⟩), h₃⟩ : T) = ⟨f b₂, s(⟨b₂, h₅⟩, ⟨b₁, h₄⟩), h₆⟩ := by
  rw! [h, Sym2.eq_swap]
  rfl

[Jakub Nowak]

Snir Broshi said:

using rw! does work, but Mathlib seems hesitant to adopt it

Why is that? I use it often, it makes things easier. I've grepped rw! and it looks like it's already being used a few times in some proofs in mathlib.

[Snir Broshi]

idk, it's currently used in exactly 4 proofs across 3 files in Mathlib.
I think Mathlib.Tactic.Common has to import it for it to gain more usage

[Jakub Nowak]

Hm, I've tried writing these without rw! and was kinda surprised that conv did a dependant rewrite (of h₃).

import Mathlib

variable {α β : Type*} {P : α → β → Prop} {Q : (a : α) → Sym2 { b : β // P a b } → Prop}

lemma foo2 {f : β → α} {b₁ b₂ : β} (h : f b₁ = f b₂) {h₁ h₂ h₃ h₄ h₅ h₆} :
    (⟨f b₁, s(⟨b₁, h₁⟩, ⟨b₂, h₂⟩), h₃⟩ : Σ a : α, Subtype (Q a)) = ⟨f b₂, s(⟨b₂, h₅⟩, ⟨b₁, h₄⟩), h₆⟩ := by
  -- same effect as `rw! [h]; clear h`
  generalize ha : f b₁ = a₁ at *
  generalize f b₂ = a₂ at *
  subst h ha

  -- same effect as `rw! [Sym2.eq_swap]; rfl`
  conv_lhs =>
    enter [2, 1]
    exact Sym2.eq_swap

[Snir Broshi]

Woah, amazing, thanks! So the at * is the solution to result is not type correct. Hmm, generalize confuses me

[Jakub Nowak]

Yes, generalize .. at * has more or less the same effect as defining the helper function. Without at * generalize will only rewrite the goal, which makes the goal not type correct, because you also need to do dependant rewrite of h₁, h₂, h₃, h₄, h₅, and h₆.

[Jakub Nowak]

E.g. in the expression ⟨f b₁, ⟨s(⟨b₁, h₁⟩, ⟨b₂, h₂⟩), h₃⟩⟩ the type of h₁ is P (f b₁) b₁, but in ⟨a₁, ⟨s(⟨b₁, h₁'⟩, ⟨b₂, h₂'⟩), h₃'⟩⟩ the type of h₁' needs to be P a₁ b₁, so you can't use h₁ directly.

[Violeta Hernández]

These are exactly the sorts of problems rw! is designed to solve, and I'd recommend you make use of it.

[Snir Broshi]

Relevant update: #13686 was just merged, and it adds import Mathlib.Tactic.DepRewrite to Mathlib.Tactic.Common :tada:
So I think I'll have no qualms using rw! moving forward

[Violeta Hernández]

(deleted)