Getting stuck with a HEq goal in 3.5.2

Stream: Analysis I

[Dan Abramov]

Here's a definition from the book:

/-- An alternate definition of a tuple, used in Exercise 3.5.2 -/
@[ext]
structure SetTheory.Set.Tuple (n:ℕ) where
  X: Set
  x: SetTheory.Set.Fin n → X
  surj: Function.Surjective x

Then this exercise asks us to prove equality of tuples:

/-- Exercise 3.5.2 -/
theorem SetTheory.Set.Tuple.eq {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := by
  constructor
  · rintro rfl
    simp
  intro h
  ext o
  constructor
  · intro ho
    let x : t.X := ⟨o, ho⟩
    have ⟨m, hm⟩ := t.surj x
    have : (t.x m) = o := by simp_all only [x]
    rw [← this, h m]
    use (t'.x m).property
  intro ho
  let x' : t'.X := ⟨o, ho⟩
  have ⟨m, hm⟩ := t'.surj x'
  have : (t'.x m) = o := by simp_all only [x']
  rw [← this, (h m).symm]
  use (t.x m).property
  sorry -- ⊢ HEq t.x t'.x

As you can see I tried to use ext, hoping that proving t.X = t'.X would be sufficient. However, since t.x type depends on t.X, and t'.x type depends on t'.X, I'm stuck with this goal that I don't know how to solve:

⊢ HEq t.x t'.x

I thought that using congr or something would help but I couldn't figure out where to place it.

In the end, after a lot of fiddling and consultations with ChatGPT, I arrived at this:

theorem SetTheory.Set.Tuple.eq' {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := by
  constructor
  · rintro rfl
    simp
  intro h
  rcases t  with ⟨tX, tx, tsurj⟩
  rcases t' with ⟨tX', tx', tsurj'⟩
  have hX : tX = tX' := by
    apply Set.ext
    intro o
    constructor
    · intro ho
      let x : tX := ⟨o, ho⟩
      have ⟨m, hm⟩ := tsurj x
      have : (tx m) = o := by simp_all only [x]
      rw [← this, h m]
      use (tx' m).property
    intro ho
    let x' : tX' := ⟨o, ho⟩
    have ⟨m, hm⟩ := tsurj' x'
    have : (tx' m) = o := by simp_all only [x']
    rw [← this, (h m).symm]
    use (tx m).property
  subst hX
  have hx : tx = tx' := by
    ext m
    apply h
  subst hx
  rfl

As you can see, in this proof the idea is to destructure both tuples with rcases first, establish memberwise equality and chip away at them with subst and rfl.

However, that seems to defeat the @[ext] placed on Tuple which makes me think that either that @[ext] is misplaced or there has to be some more idiomatic way to approach this. Ideally, I wish there some tactic or lemma that would let me ext on the tuple but then use my t.X = t'.X result to close the entire thing at the end:

theorem SetTheory.Set.Tuple.eq'' {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := by
  constructor
  · rintro rfl
    simp
  intro h
  have hX : t.X = t'.X := by
    ext o
    constructor
    · intro ho
      let x : t.X := ⟨o, ho⟩
      have ⟨m, hm⟩ := t.surj x
      have : (t.x m) = o := by simp_all only [x]
      rw [← this, h m]
      use (t'.x m).property
    intro ho
    let x' : t'.X := ⟨o, ho⟩
    have ⟨m, hm⟩ := t'.surj x'
    have : (t'.x m) = o := by simp_all only [x']
    rw [← this, (h m).symm]
    use (t.x m).property
  ext
  -- ???

Is that not possible in Lean?

If this is not possible, should the @[ext] marker be removed on Tuple (and a hint to use rcases added) to avoid sending the reader on the wrong path?

[Dan Abramov]

Also, in general, is there a way to solve an HEq goal? Or is it a dead end?

[Kenny Lau]

@Dan Abramov sometimes you might need to write your own Ext lemma, the standard way to deal with HEq is turn them into casted equality

[Kenny Lau]

i.e. equality with cast

[Kyle Miller]

@Kenny Lau Often I find it's easiest to work with casted equalities by turning them into HEqs, but depending on the specifics both directions can be useful. (E.g., rw can't rewrite with HEq, so a casted eq can be necessary.)

[Kyle Miller]

@Dan Abramov The congr! tactic can turn ⊢ HEq t.x t'.x back into t = t', but that's square one!

[Dan Abramov]

Thanks! I'm afraid I don't know what to do with casts here so I'm not sure if there are nicer approaches.

[Kyle Miller]

Which thing are you calling a cast? The coercion arrows?

There's a notion of a cast where if you have equal types, you cast the value from one to the other, which is different. Coercions tend not to be these kinds of casts.

[Kenny Lau]

I'm talking about cast

[Kyle Miller]

@Kenny Lau The question is to Dan.

[Dan Abramov]

Oh I meant I'm not sure what to do with @Kenny Lau 's suggestion.

[Kenny Lau]

no matter which path you take, you're basically stuck until you can get one of the types to be a free variable, and then you can subst the equality

[Kenny Lau]

so... generalize might be your friend

[Kyle Miller]

Dan Abramov said:

As you can see, in this proof the idea is to destructure both tuples with rcases first, establish memberwise equality and chip away at them with subst and rfl.

That seems like the right approach, deconstruct everything in sight.

With your proof, to start proving the HEq t.x t'.x case I got as far as this

  · apply Function.hfunext rfl
    intro a b hab
    cases hab
    have := h a
    /-
    a : (Fin n).toSubtype
    this : ↑(t.x a) = ↑(t'.x a)
    ⊢ HEq (t.x a) (t'.x a)
    -/

but then it's clear that there's the task of proving that t.X.toSubtype = t'.X.toSubtype, so the step of proving the X's are the same is needed, and you'll want to substitute, so may as well deconstruct everything.

[Kyle Miller]

That's also something that you already proved right after ext o, than the X's are the same, and it's annoying now that you don't have that proof available in the second case.

[Kyle Miller]

I think it's OK if you don't use ext directly.

Basically, @[ext] generates its proof by destructuring everything. It's bundling that up, so that you can avoid deconstructing things when it's not necessary.

[Dan Abramov]

I guess a split like this might make sense for the exercise?

With Tuple.ext being prefilled and Tuple.eq being left to the reader.

/-- An alternate definition of a tuple, used in Exercise 3.5.2 -/
structure SetTheory.Set.Tuple (n:ℕ) where
  X: Set
  x: SetTheory.Set.Fin n → X
  surj: Function.Surjective x

@[ext]
lemma SetTheory.Set.Tuple.ext {n:ℕ} {t t':Tuple n}
    (hX : t.X = t'.X)
    (hx : ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object)) :
    t = t' := by
  rcases t with ⟨tX, tx, tsurj⟩
  rcases t' with ⟨tX', tx', tsurj'⟩
  subst hX
  congr
  ext m
  apply hx

theorem SetTheory.Set.Tuple.eq {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := by
  constructor
  · rintro rfl
    simp
  intro h
  ext o
  · constructor
    · intro ho
      let x : t.X := ⟨o, ho⟩
      have ⟨m, hm⟩ := t.surj x
      have : (t.x m) = o := by simp_all only [x]
      rw [← this, h m]
      use (t'.x m).property
    intro ho
    let x' : t'.X := ⟨o, ho⟩
    have ⟨m, hm⟩ := t'.surj x'
    have : (t'.x m) = o := by simp_all only [x']
    rw [← this, (h m).symm]
    use (t.x m).property
  apply h

[Kyle Miller]

Yeah, that might make sense.

I just tried doing it from scratch, and it's basically the one you got from ChatGPT consultations:

theorem SetTheory.Set.Tuple.eq {n:ℕ} (t t':Tuple n) :
    t = t' ↔ ∀ n : Fin n, ((t.x n):Object) = ((t'.x n):Object) := by
  constructor
  · rintro rfl
    simp
  obtain ⟨X, x, surj⟩ := t
  obtain ⟨X', x', surj'⟩ := t'
  dsimp
  intro h
  have : X = X' := by
    ext o
    constructor
    · intro ho
      obtain ⟨m, hm⟩ := surj ⟨o, ho⟩
      have := h m
      simp only [hm] at this
      simp only [this]
      apply Subtype.property
    · intro ho
      obtain ⟨m, hm⟩ := surj' ⟨o, ho⟩
      have := h m
      simp only [hm] at this
      simp only [← this]
      apply Subtype.property
  cases this
  simp
  ext n
  exact h n

[Dan Abramov]

Nice, thanks for confirming! It's the first time I run into this issue so this is actually quite illuminating

[Dan Abramov]

Sent https://github.com/teorth/analysis/pull/281

[Kyle Miller]

A fancy feature for you: rather than use have then subst, you can do obtain rfl : X = X' := by ...

[Dan Abramov]

Is there some general lesson here? When you're comparing structures with different (but provably same) types inside, you have to get rid of the structure so you're able to subst inside them?

[Kyle Miller]

More generally, when you have types that are equal, you can't usually do anything with it until the types are the same. One of the main tools to get types to be the same is to subst any equations, and to do that you want equations between free variables.

This shows up for structures with dependent fields, but you also see it for equations between functions with dependently typed arguments. To deal with it, you "start from the top", eliminating equations, causing the next types to be the same, letting you eliminate more, making more types be the same, and so on.

Kenny mentioned generalize, which is a good tool for replacing subexpressions with free variables, when that's possible. Using cases on a structure could be thought of as a kind of generalization too (it replaces t and all the t projections with fresh variables, ones that forget they ever came from a t, so they're not quite so dependent anymore). Another is making auxiliary lemmas, like your SetTheory.Set.Tuple.eq, that hide away some cases/subst/congr argument, an argument you wouldn't be able to so easily do if t and t' weren't variables.