Improve a proof related to funext

Stream: new members

[Shanghe Chen]

Hi I proved a theorem kind of related to funext, cast and Heq, which the background maybe from caregory theory:

theorem heq_funext3.{u, v} (α β : Sort u) (p : α = β)
    (f : α -> α -> Sort v) (g : β -> β -> Sort v)
    (q : (a : α) -> (b : α) -> f a b = g (cast p a) (cast p b))
    (h : (a a' a'' : α) -> (f a a') -> (f a' a'') -> (f a a''))
    (i : (b b' b'' : β) -> (g b b') -> (g b' b'') -> (g b b''))
    (j : (a a' a'' : α ) -> (x: f a a') -> (y : f a' a'') ->
            cast (q a a'') (h a a' a'' x y) = i (cast p a) (cast p a') (cast p a'') (cast (q a a') x) (cast (q a' a'') y))
      : HEq h i
    := by
  cases p
  simp at *
  let k : f = g := by
    apply funext
    intro x
    apply funext
    intro y
    exact q x y
  cases k
  simp at *
  apply funext
  intro a
  apply funext
  intro a'
  apply funext
  intro a''
  apply funext
  intro x
  apply funext
  intro y
  apply j

[Shanghe Chen]

any way to improve it? the repeated funext seems a little ugly

[Eric Wieser]

You're looking for the ext tactic

[Eric Wieser]

theorem heq_funext3.{u, v} (α β : Sort u) (p : α = β)
    (f : α -> α -> Sort v) (g : β -> β -> Sort v)
    (q : (a : α) -> (b : α) -> f a b = g (cast p a) (cast p b))
    (h : (a a' a'' : α) -> (f a a') -> (f a' a'') -> (f a a''))
    (i : (b b' b'' : β) -> (g b b') -> (g b' b'') -> (g b b''))
    (j : (a a' a'' : α ) -> (x: f a a') -> (y : f a' a'') ->
            cast (q a a'') (h a a' a'' x y) = i (cast p a) (cast p a') (cast p a'') (cast (q a a') x) (cast (q a' a'') y))
      : HEq h i
    := by
  cases p
  obtain rfl : f = g := by
    ext x y
    apply q
  simp only [cast_eq, heq_eq_eq] at *
  ext a a' a'' x y
  apply j

[Shanghe Chen]

Ah I don’t know ext can be used in this way. Thank you very much Eric. Your proof is extremely clean:tada:

[Kyle Miller]

Here's essentially the same proof:

theorem heq_funext3.{u, v} (α β : Sort u) (p : α = β)
    (f : α -> α -> Sort v) (g : β -> β -> Sort v)
    (q : (a : α) -> (b : α) -> f a b = g (cast p a) (cast p b))
    (h : (a a' a'' : α) -> (f a a') -> (f a' a'') -> (f a a''))
    (i : (b b' b'' : β) -> (g b b') -> (g b' b'') -> (g b b''))
    (j : (a a' a'' : α ) -> (x: f a a') -> (y : f a' a'') ->
            cast (q a a'') (h a a' a'' x y) = i (cast p a) (cast p a') (cast p a'') (cast (q a a') x) (cast (q a' a'') y))
      : HEq h i
    := by
  cases p
  cases (funext₂ q : f = g)
  dsimp at j
  rw [heq_eq_eq]
  ext
  apply j

[Kyle Miller]

Eric's obtain rfl : f = g := ... trick is neat. I guess you can write obtain rfl : f = g := funext₂ q as well.

[Kyle Miller]

By the way, the ext tactic's original purpose (or at least I think so, I don't actually know) is to do apply funext; intro for you repeatedly, but it's generalized to handle all sorts of extentionality arguments.

[Shanghe Chen]

Wow this is extremely nice too. Yeah ext and the related tactics are much more powerful than I expected :tada:

[Eric Wieser]

Isn't there also a funext tactic, which does that without any extra features? Or was that finally removed?