Rewrites inside a complex goal

Stream: new members

[Michał Pacholski]

In this simple example, I have a theorem which would immediately solve the goal, but it fails to find an occurrence of the pattern, which to my eyes is right there.

import Mathlib

example
  (h : Continuous fun (x : EuclideanSpace ℝ (Fin 3)) ↦ (‖x‖ ^ 2)) :
  Continuous fun  (x : EuclideanSpace ℝ (Fin 3)) ↦  (∑ i, ‖x i‖ ^ 2)
   := by
  -- h : Continuous fun x ↦ ‖x‖ ^ 2
  -- ⊢ Continuous fun x ↦ ∑ i, ‖x i‖ ^ 2--
  -- I imagine this would solve the goal
  rw [EuclideanSpace.norm_sq_eq] at h
  -- but instead I get an error
  -- Tactic `rewrite` failed: Did not find an occurrence of the pattern
  --   ‖?x‖ ^ 2
  -- in the target expression
  --   Continuous fun x ↦ ‖x‖ ^ 2
  sorry

Does anyone know what am I doing wrong here?

[Jireh Loreaux]

It's just because x is a bound variable, and rw can't rewrite bound variables.

[Jireh Loreaux]

simp_rw will do this for you.

[Luigi Massacci]

You may also want to look at the conv tactic in the future

[Michał Pacholski]

@Jireh Loreaux simp_rw did the trick! Thank you, I never saw this tactic.
@Luigi Massacci conv is now my new best friend :smile:

[Ryan Smith]

How would you use conv here? I've read the tactic docs a couple of times but it's not clicked for me yet

[David Ledvinka]

import Mathlib

example
  (h : Continuous fun (x : EuclideanSpace ℝ (Fin 3)) ↦ (‖x‖ ^ 2)) :
  Continuous fun  (x : EuclideanSpace ℝ (Fin 3)) ↦  (∑ i, ‖x i‖ ^ 2)
   := by
  conv at h in ‖_‖ ^ 2 => rw [EuclideanSpace.norm_sq_eq]
  assumption

Basically you can use conv to go "inside" the binders so you can use rw. I seem to recall talks of rw eventually being able to rewrite in binders so that this trick won't be needed as much (but conv is still useful for other purposes such as if you only want to apply rw or simp to a particular part of the goal)

[Ryan Smith]

That makes a lot of sense. I wonder why rw can't do that but I can see why we need that.

[Michał Pacholski]

I stumbled upon another mysterious case, when rw failed, although the pattern is right there.

My goal is
⊢ inversionHomeo (inversionHomeo x) = x
which I want to transform to
⊢ (inversionHomeo.trans inversionHomeo) x = x
but the rewrite
rw [←Homeomorph.trans_apply inversionHomeo inversionHomeo x]
produces an error

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  inversionHomeo (inversionHomeo x)
in the target expression
  inversionHomeo (inversionHomeo x) = x

This time x is not a bound variable, so I don't see why would it fail. Below I attach the full example to reproduce the error. I apologize it's so lengthy, but when I tried running the tactic in an isolated theorem it worked without a problem (which the example also shows). It only fails in the cocycle case.

There's a couple more weird things. E.g. tactics that work well in an isolated theorem inversionHomeoInvolutive' fail for the same goal in case cocycle.

Btw. I tried all of simp_rw, rw! and conv. I couldn't get either to work.

import Mathlib

open CategoryTheory
-- First, define our building blocks as pure terms
def puncturedLine := TopologicalSpace.Closeds.compl (TopologicalSpace.Closeds.singleton (0 : ℝ))
abbrev P := (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj puncturedLine
-- Define the inversion map as a Homeomorphism (Iso in TopCat)
noncomputable
def inversionHomeo : puncturedLine ≃ₜ puncturedLine := {
  toFun := fun x ↦ ⟨x.val⁻¹, inv_ne_zero x.property⟩,
  invFun := fun x ↦ ⟨x.val⁻¹, inv_ne_zero x.property⟩,
  left_inv := by intro x; simp [inv_inv, Subtype.coe_eta],
  right_inv := by intro x; simp [inv_inv, Subtype.coe_eta],
  continuous_toFun := by
    -- As we proved before, this is a composition of continuous functions
    apply Continuous.subtype_mk
    apply Continuous.inv₀
    exact continuous_subtype_val
    intro x
    exact x.property,
  continuous_invFun := by
    apply Continuous.subtype_mk
    apply Continuous.inv₀
    exact continuous_subtype_val
    intro x
    exact x.property,
}

def V : Bool → Bool → TopologicalSpace.Opens ℝ :=
  fun | true, true   => ⊤
      | true, false  => puncturedLine
      | false, true  => puncturedLine
      | false, false => ⊤

noncomputable
def t : ∀ i j, (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj (V i j) ⟶
  (TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj (V j i) :=
  fun | true, true => 𝟙 _
      | true, false => (TopCat.isoOfHomeo inversionHomeo).hom
      | false, true => (TopCat.isoOfHomeo inversionHomeo).hom
      | false, false => 𝟙 _

theorem inversionHomeoInvolutive : inversionHomeo (inversionHomeo x) = x := by
  rw [←Homeomorph.trans_apply inversionHomeo inversionHomeo x]
  unfold inversionHomeo
  dsimp
  simp only [inv_inv]

theorem inversionHomeoInvolutive' : inversionHomeo (inversionHomeo x) = x := by
  unfold inversionHomeo
  dsimp
  simp only [inv_inv]

noncomputable
def circleGlueDataCore : TopCat.GlueData.MkCore := by
  constructor
  case J => exact Bool
  case U => exact fun _ => TopCat.of ℝ
  case V => exact V
  case t => exact t

  case V_id =>
    intro i
    cases i <;> rfl -- This is now definitionally true

  case t_id =>
    intro i
    cases i <;> rfl

  case t_inter =>
    intros i j k x hx_in_Vik
    cases i <;> cases j <;> cases k <;>
    dsimp [t, V, puncturedLine] at * <;>
    first | trivial
          | apply SetLike.coe_mem

  case cocycle =>
    -- We need to prove tjk ∘ tij = tik on the triple overlap
    intros i j k x hx_in_Vik
    cases i <;> cases j <;> cases k <;>
    dsimp [t, V] <;>
    rw [SetLike.coe_eq_coe] <;>
    {
      rw [←Homeomorph.trans_apply inversionHomeo inversionHomeo x]
      -- Tactic `rewrite` failed: Did not find an occurrence of the pattern
      --   inversionHomeo (inversionHomeo x)
      -- in the target expression
      --   inversionHomeo (inversionHomeo x) = x
      unfold inversionHomeo
      dsimp
      simp only [inv_inv]
    }
    -- these tactics worked for inversionHomeoInvolutive', but here, they don't
    -- {
    --   unfold inversionHomeo
    --   dsimp
    --   simp only [inv_inv]
    -- }
    -- {
    --   -- ths solves the goal, but I'm still confused why does the rewrite fails:
    --   change (inversionHomeo.trans inversionHomeo) x = x
    --   unfold inversionHomeo
    --   dsimp
    --   simp only [inv_inv]
    --   rfl
    -- }
    -- {
    --   -- either of thess of course also work:
    --   -- exact inversionHomeoInvolutive
    --   -- exact inversionHomeoInvolutive'
    -- }

[Aaron Liu]

you have ↑((TopologicalSpace.Opens.toTopCat (TopCat.of ℝ)).obj puncturedLine) and you have ↥puncturedLine and these are not reducibly defeq I think

[Michał Pacholski]

Ah, I see. When I change type of inversionHomeo to P ≃ₜ P, it works without any problem (of course as long as I use abbrev P := ... not def P := ..., which makes sense to me.

[Michał Pacholski]

Thank you!