Reindexing a dependent product

Stream: Is there code for X?

[Oliver Nash]

I've tripped up on an extremely elementary type theory issue and would appreciate some help.

[Oliver Nash]

How can I close the sorrys in the following:

import data.equiv.basic

def foo {ι ι' : Type*} (σ : ι ≃ ι') (α : ι → Type*) (α' : ι' → Type*)
  (e : ∀ ⦃i j⦄, σ i = j → α i ≃ α' j) : (Π i, α i) ≃ Π i', α' i' :=
{ to_fun    := λ f i', e (σ.apply_symm_apply i') $ f $ σ.symm i',
  inv_fun   := λ F i, (e rfl).symm $ F $ σ i,
  left_inv  := λ f, by { ext i, simp only, sorry, }, -- stuck because `α i` is different type to `α (σ.symm (σ i))`
  right_inv := sorry, }

[Oliver Nash]

(It's likely this exists somewhere in Mathlib but I couldn't find it.)

[Oliver Nash]

Ah, this is basically docs#equiv.Pi_congr

[Oliver Nash]

Sorry for the noise.

[Kyle Miller]

Just to share tips for how to bash through these sorts of dependent type issues, I've learned about how generalize, generalize_proofs, and revert can be very helpful. The strategy is to try to generalize things until the goal is completely parameterized (make it be universally quantified over everything in sight that's causing you problems) and then try to use the hypotheses to do substitutions. Then you can usually figure out what technical lemma you should write.

Doing the first part of this for the first sorry:

def foo {ι ι' : Type*} (σ : ι ≃ ι') (α : ι → Type*) (α' : ι' → Type*)
  (e : Π ⦃i j⦄, σ i = j → α i ≃ α' j) : (Π i, α i) ≃ Π i', α' i' :=
{ to_fun    := λ f i', e (σ.apply_symm_apply i') $ f $ σ.symm i',
  inv_fun   := λ F i, (e rfl).symm $ F $ σ i,
  left_inv  := λ f, begin
    ext i,
    simp only,
    rw equiv.symm_apply_eq,
    generalize hy : f (σ.symm (σ i)) = y,
    generalize_proofs ha hb,
    generalize hy' : f i = y',
    revert ha hb y y',
    generalize hi' : σ.symm (σ i) = i',
    intro ha,
    rw equiv.apply_eq_iff_eq at ha,
    subst ha,
    rintros _ y y' rfl rfl,
    refl,
  end,
  right_inv := sorry, }

[Kyle Miller]

Conceptually, this is a strategy to make it easier to do simultaneous rewrites, which you often need to do when you have dependent types. It also helps make the goal more proof irrelevant -- you don't really want to be spending time rewriting things inside proofs.

[Oliver Nash]

Oh wow, thanks very much. I've spent the bulk of today fighting with the type system and nearly going mad. I need to go and organise dinner now but I'll try again this evening and see if I can get there with these tips.

[Oliver Nash]

I've reduced my goal to this (copied from context: typeclasses can be relaxed):

import analysis.normed_space.multilinear

universes u₁ u₂ u₃ u₄ u₅

variables {ι : Type u₁} {𝕜 : Type u₂} {E : ι → Type u₄} {F : Type u₃}
variables [decidable_eq ι] [fintype ι] [nondiscrete_normed_field 𝕜]
variables [normed_group F] [normed_space 𝕜 F]
variables [∀ i, normed_group (E i)] [∀ i, normed_space 𝕜 (E i)]

def multilinear_map.dom_dom_congr_linear_equiv' {ι' : Type u₅} [decidable_eq ι'] (σ : ι ≃ ι')
  (E' : ι' → Type u₄) [∀ i, normed_group (E' i)] [∀ i, normed_space 𝕜 (E' i)]
  (e : ∀ i',  E (σ.symm i') ≃ₗ[𝕜] E' i') :
  multilinear_map 𝕜 E F ≃ₗ[𝕜] multilinear_map 𝕜 E' F :=
sorry

It's somewhat maddening to have burned hours on something so vacuous (albeit I did gain some limited expertise with dependent functions).

[Kyle Miller]

Here's a possible technical lemma for then dealing with the dependent rewrite:

def foo {ι ι' : Type*} (σ : ι ≃ ι') (α : ι → Type*) (α' : ι' → Type*)
  (e : Π ⦃i j⦄, σ i = j → α i ≃ α' j) : (Π i, α i) ≃ Π i', α' i' :=
{ to_fun    := λ f i', e (σ.apply_symm_apply i') $ f $ σ.symm i',
  inv_fun   := λ F i, (e rfl).symm $ F $ σ i,
  left_inv  := λ f, begin
    ext i,
    simp only,
    rw equiv.symm_apply_eq,
    have : ∀ {i i'} (ha : σ i' = σ i) (hb : σ i = σ i) {y : α i'} {y' : α i},
      f i' = y → f i = y' → e ha y = e hb y',
    { intros i i' ha,
      rw equiv.apply_eq_iff_eq at ha,
      subst ha,
      rintros _ _ _ rfl rfl,
      refl },
    apply this _ rfl rfl rfl,
  end,
  right_inv := sorry, }

[Kyle Miller]

I extracted it from one of the goals from the first proof. I'm sure it could be simplified more.

[Oliver Nash]

Thanks, I really better run now but I'll study this later.

[Kyle Miller]

The first time I'd seen one of these rewrite lemmas was when @Mario Carneiro kindly showed how it was done (I suppose he was sort of the Virgil to dependent type hell).

[Patrick Massot]

Kyle, it would be very nice if you could write a blog post about these tricks in the community blog. This kind of wisdom has been explicitly in scope of our blog from the beginning, but we haven't seen any such post up to now. You would need to find a simpler first example of course.

[Floris van Doorn]

This is basically docs#equiv.Pi_congr modulo docs#forall_eq (but where p is a family of types instead of a predicate). (Oh, I now see this was mentioned)

[Oliver Nash]

I returned to this and created #10432 since it's nearly impossible to use docs#equiv.Pi_congr and docs#equiv.Pi_congr' without these lemmas. @Kyle Miller thank you very much for the tips btw: I would never have learned the required black magic without your help.