clever copy

Stream: mathlib4

[Sébastien Gouëzel]

I'd like to define a Prop-valued version of RCLike for normed fields, in which I require that there exists an RCLike structure which is compatible with the given normed field structure. For this to be useful, I would like to be able to create a new RCLike structure in which the propeq becomes defeq, as in the following:

import Mathlib

/-- A copy of an `RCLike` field in which the `NormedField` field is adjusted to be become defeq
to a propeq one. -/
def RCLike.copy {𝕜 : Type*} (h : RCLike 𝕜) (hk : NormedField 𝕜)
    (h'' : h.toNormedField = hk) : RCLike 𝕜 where
   __ := hk
  ...

However, when trying to fill in the ..., I get into a maze of issues coming from the fact that the mul, add (and so on) fields of h and hk are different. I guess I could fill them by hand by putting enough @ around, but I'd be interested in a better strategy. Any idea?

[Sébastien Gouëzel]

For the record, I have a complete ugly construction, which fails for performance reasons (it works if I sorry out a few fields, but never completes when I unsorry them all -- I mean, no timeout, but the yellow bar is still there after 20 minutes). I'll try to split into smaller chunks to see if I get to something acceptable.

/-- A copy of an `RCLike` field in which the `NormedField` field is adjusted to be become defeq
to a propeq one. -/
def RCLike.copy {𝕜 : Type*} (h : RCLike 𝕜)  (hk : NormedField 𝕜)
    (h'' : h.toNormedField = hk) : RCLike 𝕜 where
  __ := hk
  toPartialOrder := h.toPartialOrder
  toDecidableEq := h.toDecidableEq
  complete := by
    convert @CompleteSpace.complete _ (_) h.toCompleteSpace <;> simp only [h'']
  lt_norm_lt := fun x y hx hy ↦ by simpa [h''] using h.lt_norm_lt x y hx hy
  -- star fields
  star := (@StarMul.toInvolutiveStar _ (_) (@StarRing.toStarMul _ (_) h.toStarRing)).star
  star_involutive :=
    @star_involutive _ (@StarMul.toInvolutiveStar _ (_) (@StarRing.toStarMul _ (_) h.toStarRing))
  star_mul x y := by
    convert @star_mul _ (_)  (@StarRing.toStarMul _ (_) h.toStarRing) x y <;> simp only [h'']
  star_add x y := by
    convert @StarRing.star_add _ (_) h.toStarRing x y <;> simp only [h'']
  -- algebra fields
  smul := (@Algebra.toSMul _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)).smul
  toFun := @Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra)
  map_one' := by
    let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
    convert @OneHom.map_one' _ _ _ (_) (@MonoidHom.toOneHom _ _ _ (_)
      (@RingHom.toMonoidHom _ _ _ (_) Z))
    simp only [h'']
  map_mul' x y := by
    let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
    convert @MulHom.map_mul' _ _ _ (_) (@MonoidHom.toMulHom _ _ _ (_)
      (@RingHom.toMonoidHom _ _ _ (_) Z)) x y <;>
    simp only [h'']
  map_zero' := by
    let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
    convert @ZeroHom.map_zero' _ _ _ (_) (@AddMonoidHom.toZeroHom _ _ _ (_)
      (@RingHom.toAddMonoidHom _ _ _ (_) Z)) <;>
    simp only [h'']
  map_add' x y := by
    let Z := (@Algebra.toRingHom _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra))
    convert @AddHom.map_add' _ _ _ (_) (@AddMonoidHom.toAddHom _ _ _ (_)
      (@RingHom.toAddMonoidHom _ _ _ (_) Z)) x y <;>
    simp only [h'']
  commutes' r x := by
    convert @Algebra.commutes' _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra) r x
    <;> simp only [h'']
  smul_def' r x := by
    convert @Algebra.smul_def' _ _ _ (_) (@NormedAlgebra.toAlgebra _ _ _ (_) h.toNormedAlgebra) r x
    <;> simp only [h'']
  norm_smul_le r x := by
    convert @NormedAlgebra.norm_smul_le _ _ _ (_) h.toNormedAlgebra r x <;> simp only [h'']
  -- RCLike fields
  re :=
    { toFun := h.re
      map_zero' := by
        convert @ZeroHom.map_zero' _ _ (_) _ (@AddMonoidHom.toZeroHom _ _ (_) _ h.re)
        simp only [h'']
      map_add' := by
        intro x y
        convert @AddHom.map_add' _ _ (_) _ (@AddMonoidHom.toAddHom _ _ (_) _ h.re) x y
        <;> simp only [h''] }
  im :=
    { toFun := h.im
      map_zero' := by
        convert @ZeroHom.map_zero' _ _ (_) _ (@AddMonoidHom.toZeroHom _ _ (_) _ h.im)
        simp only [h'']
      map_add' := by
        intro x y
        convert @AddHom.map_add' _ _ (_) _ (@AddMonoidHom.toAddHom _ _ (_) _ h.im) x y
        <;> simp only [h''] }
  I := h.I
  I_re_ax := by convert h.I_re_ax <;> simp only [h'']
  I_mul_I_ax := by convert h.I_mul_I_ax <;> simp only [h'']
  re_add_im_ax z := by convert h.re_add_im_ax z <;> simp only [h'']
  ofReal_re_ax r := by convert h.ofReal_re_ax r <;> simp only [h'']
  ofReal_im_ax r := by convert h.ofReal_im_ax r <;> simp only [h'']
  mul_re_ax z w := by convert h.mul_re_ax z w <;> simp only [h'']
  mul_im_ax z w := by convert h.mul_im_ax z w <;> simp only [h'']
  conj_re_ax z := by convert h.conj_re_ax z <;> simp only [h'']
  conj_im_ax z := by convert h.conj_im_ax z <;> simp only [h'']
  conj_I_ax := by convert h.conj_I_ax <;> simp only [h'']
  norm_sq_eq_def_ax z := by convert h.norm_sq_eq_def_ax z <;> simp only [h'']
  mul_im_I_ax z := by convert h.mul_im_I_ax z <;> simp only [h'']
  le_iff_re_im {z} {w} := by convert h.le_iff_re_im (z := z) (w := w) <;> simp only [h'']

[Eric Wieser]

This seems like an #xy problem to me; can't you just subst h'' to make things defeq in the context where you want this?

[Eric Wieser]

It's also possible to get the lift tactic to do the same thing I think

[Sébastien Gouëzel]

I need a Prop-version of RCLike that can say if any given normed field is like R or C. With your subst trick, I can do

class IsRorC (𝕜 : Type*) [hk : NormedField 𝕜] : Prop :=
  out : ∃ h : RCLike 𝕜, hk = h.toNormedField

noncomputable def RCLike.copy_of_normedField {𝕜 : Type*} (h : RCLike 𝕜) (hk : NormedField 𝕜)
    (h'' : hk = h.toNormedField) : RCLike 𝕜 where ...

noncomputable def IsRorC.rclike (𝕜 : Type*) [hk : NormedField 𝕜] [h : IsRorC 𝕜] : RCLike 𝕜 := by
  choose p hp using h.out
  exact p.copy_of_normedField hk hp

And then if I can start the proof of Hahn-Banach theorem, say, with

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [IsRorC 𝕜] {E : Type*}
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

theorem exists_extension_norm_eq (p : Subspace 𝕜 E) (f : p →L[𝕜] 𝕜) :
    ∃ g : E →L[𝕜] 𝕜, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ := by
  letI : RCLike 𝕜 := IsRorC.rclike 𝕜
  ...

with no other change to the proof. And this works great!

[Eric Wieser]

I was proposing something like this:

import Mathlib

class IsRorC (𝕜 : Type*) [hk : NormedField 𝕜] : Prop :=
  elimNormedField : ∃ h : RCLike 𝕜, hk = h.toNormedField

theorem IsRorC.elimNontriviallyNormedField (𝕜 : Type*) [hk : NontriviallyNormedField 𝕜] [IsRorC 𝕜] :
    ∃ h : RCLike 𝕜, hk = h.toNontriviallyNormedField := by
  refine IsRorC.elimNormedField.imp fun h heq => ?_
  cases hk
  congr

variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [IsRorC 𝕜] {E : Type*}
  [SeminormedAddCommGroup E] [NormedSpace 𝕜 E]

theorem exists_extension_norm_eq' (p : Subspace 𝕜 E) (f : p →L[𝕜] 𝕜) :
    ∃ g : E →L[𝕜] 𝕜, (∀ x : p, g x = f x) ∧ ‖g‖ = ‖f‖ := by
  obtain ⟨h, rfl⟩ := IsRorC.elimNontriviallyNormedField 𝕜
  sorry

[Sébastien Gouëzel]

That's nice! An issue I see is that you need to have one constructor for NormedField, one for NontriviallyNormedField, one for DenselyNormedField -- and if some day you run into some other situation where you can not subst, then it might get complicated. All this is avoided by the copy argument, at the expense of needing to construct RCLike.copy_of_normedField, so it looks a little bit more cumbersome for the API writer, but a little nicer for the API user, I think.