ContMDiff puzzle

Stream: new members

[Dominic Steinitz]

Why don't I need 2 rw terms (one for each occurrence) and I can't work out what Lean is telling me from the error message.

import Mathlib

open Function Set
open IsManifold Manifold

example : 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) = (𝓡 1).prod (𝓡 1) :=
 modelWithCornersSelf_prod

variable (f : EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) →
              EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))

example :
  ContMDiffOn ((𝓡 1).prod (𝓡 1))
              ((𝓡 1).prod (𝓡 1)) ⊤ f
              {x | x.1 0 > 0 ∨ x.1 0 < 0}
  ↔ ContMDiffOn 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
                𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) ⊤ f
                {x | x.1 0 > 0 ∨ x.1 0 < 0} := by
  constructor
  · intro h
    have h0 : ContMDiffOn ((𝓡 1).prod (𝓡 1)) ((𝓡 1).prod (𝓡 1)) ⊤ f
              {x | x.1 0 > 0 ∨ x.1 0 < 0} := h
    have h1 : 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) = (𝓡 1).prod (𝓡 1) :=
      modelWithCornersSelf_prod
    rw [← h1] at h
    exact h
  · intro h
    have h0 : ContMDiffOn 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
                          𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) ⊤ f
              {x | x.1 0 > 0 ∨ x.1 0 < 0} := h
    have h1 : 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) = (𝓡 1).prod (𝓡 1) :=
      modelWithCornersSelf_prod
    rw [h1] at h
    exact h

[Dominic Steinitz]

In case anyone is interested. I still don't know why my original attempt failed though.

import Mathlib

open Function Set
open IsManifold Manifold

example : 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) = (𝓡 1).prod (𝓡 1) :=
 modelWithCornersSelf_prod

variable (f : EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) →
              EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))

example  : ContMDiffOn ((𝓡 1).prod (𝓡 1))
              ((𝓡 1).prod (𝓡 1)) ⊤ f
              {x | x.1 0 > 0 ∨ x.1 0 < 0}
  ↔ ContMDiffOn 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
                𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) ⊤ f
                {x | x.1 0 > 0 ∨ x.1 0 < 0} := by
  have ha2b : ContMDiff
    𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    ((𝓡 1).prod (𝓡 1))
    ⊤
    (id : EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) →
          EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) := by
    rw [contMDiff_iff]
    constructor
    · exact continuous_id
    · intro x y
      exact contDiffOn_id

  have hb2a : ContMDiff
    ((𝓡 1).prod (𝓡 1))
    𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    ⊤
    (id : EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1) →
          EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) := by
    rw [contMDiff_iff]
    constructor
    · exact continuous_id
    · intro x y
      exact contDiffOn_id
  constructor
  · intro h
    have h0 : ContMDiffOn ((𝓡 1).prod (𝓡 1)) ((𝓡 1).prod (𝓡 1)) ⊤ f
              {x | x.1 0 > 0 ∨ x.1 0 < 0} := h
    have h1 : ContMDiffOn
              𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
              ((𝓡 1).prod (𝓡 1)) ⊤ (f ∘ id)
              {x | x.1 0 > 0 ∨ x.1 0 < 0} :=
               ContMDiffOn.comp h0
                (ContMDiffOn.mono (contMDiffOn_univ.mpr ha2b) (Set.subset_univ _)) (fun ⦃a⦄ a ↦ a)
    have h2 : ContMDiffOn
              𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
              𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) ⊤ (id ∘ f ∘ id)
              {x | x.1 0 > 0 ∨ x.1 0 < 0} :=
      ContMDiffOn.comp (contMDiffOn_univ.mpr hb2a) h1 (Set.subset_univ _)
    exact h2
  · intro h
    have h0 : ContMDiffOn 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
                          𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) ⊤ f
              {x | x.1 0 > 0 ∨ x.1 0 < 0} := h
    have h1 : ContMDiffOn
              ((𝓡 1).prod (𝓡 1))
              𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
              ⊤ (f ∘ id)
              {x | x.1 0 > 0 ∨ x.1 0 < 0} :=
               ContMDiffOn.comp h0
                (ContMDiffOn.mono (contMDiffOn_univ.mpr hb2a) (Set.subset_univ _)) (fun ⦃a⦄ a ↦ a)
    have h2 : ContMDiffOn
              ((𝓡 1).prod (𝓡 1))
              ((𝓡 1).prod (𝓡 1))
               ⊤ (id ∘ f ∘ id)
              {x | x.1 0 > 0 ∨ x.1 0 < 0} :=
      ContMDiffOn.comp (contMDiffOn_univ.mpr ha2b) h1 (Set.subset_univ _)
    exact h2

[Aaron Liu]

Dominic Steinitz said:

Why don't I need 2 rw terms (one for each occurrence)

That's just how rw works: it rewrites all occurrences

[Aaron Liu]

if you don't want it to rewrite all occurrences you can specify which occurrences you want with (occs := [1, 2, 5]) (or specify the ones you don't want with (occs := .neg [3, 4, 6]))

[Dominic Steinitz]

I have an example here (not an MWE)

rw [Set.image_pair, Set.image_pair]

if I remove the second rw then my proof fails.

So now I am confused.

[Aaron Liu]

That's because you're rewriting with different arguments

[Aaron Liu]

rw will only rewrite with one set of arguments at a time

[Aaron Liu]

so if you rw [add_zero, add_zero, add_zero] on
1 + 0 + 0 = 0 + (1 + 0) + 0 will transform the goal into
1 + 0 = 0 + (1 + 0) + 0, and then
1 = 0 + 1 + 0, and then
1 = 0 + 1

[Aaron Liu]

see how it rewrites all the occurrences with one instantiation at a time

[Aaron Liu]

so first it rewrites all the 1 + 0 + 0 into 1 + 0, and then it rewrites all the 1 + 0 into 1, and then it rewrites all the 0 + 1 + 0 into 0 + 1

[Michael Rothgang]

To re-state what Aaron said: rw searches for the first match of the pattern, and then rewrites this as often as it can. nth_rw <n> only rewrites the n-th occurrence. simp_rw is more like "rw all the occurrences of all the patterns" (but not quite, it uses simp internally, i.e. operates differently).

[Dominic Steinitz]

That's great - thanks for the explanation :smiley:

The rw does succeed but the re-written term then gives a difficult to understand error message.

type mismatch
  h
has type
  @ContMDiffOn ℝ DenselyNormedField.toNontriviallyNormedField (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    Prod.normedAddCommGroup Prod.normedSpace (ModelProd (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)))
    (instTopologicalSpaceModelProd (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)))
    𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    instTopologicalSpaceProd
    (prodChartedSpace (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1))
      (EuclideanSpace ℝ (Fin 1)))
    (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) Prod.normedAddCommGroup Prod.normedSpace
    (ModelProd (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)))
    (instTopologicalSpaceModelProd (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)))
    𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    instTopologicalSpaceProd
    (prodChartedSpace (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1))
      (EuclideanSpace ℝ (Fin 1)))
    ⊤ f {x | x.1 0 > 0 ∨ x.1 0 < 0} : Prop
but is expected to have type
  @ContMDiffOn ℝ DenselyNormedField.toNontriviallyNormedField (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    Prod.normedAddCommGroup Prod.normedSpace (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    PseudoMetricSpace.toUniformSpace.toTopologicalSpace 𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) instTopologicalSpaceProd
    (chartedSpaceSelf (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)))
    (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) Prod.normedAddCommGroup Prod.normedSpace
    (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) PseudoMetricSpace.toUniformSpace.toTopologicalSpace
    𝓘(ℝ, EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1)) (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))
    instTopologicalSpaceProd (chartedSpaceSelf (EuclideanSpace ℝ (Fin 1) × EuclideanSpace ℝ (Fin 1))) ⊤ f
    {x | x.1 0 > 0 ∨ x.1 0 < 0} : Prop

[Dominic Steinitz]

I vaguely understand it - I guess there is some sort of type class machinery lurking in the background which means you can't rewrite things that are equal.

[Dominic Steinitz]

And I do have a way of doing what I want to do (and which seems entirely reasonable to do) so I am happy to leave it as one of the world's great unresolved mysteries.