Zulip Chat Archive

Stream: general

Topic: Dealing with heq and Sigma types


view this post on Zulip Patrick Lutz (Nov 11 2020 at 19:49):

When proving that some type is equivalent to a Sigma type, how do you deal with heqs that pop up? Here's an example

import tactic

variables (A B : Type) (S : set A)

example : (A  B)  Σ (f : S  B), {φ : A  B //  (s : A) (h : s  S), φ s = f s, h } :=
{ to_fun := λ g, λ s, g s.1, g, λ _ _, rfl⟩⟩,
  inv_fun := λ f, φ⟩, φ.1,
  left_inv := λ _, rfl,
  right_inv := begin
    rintros f, φ, h⟩,
    ext,
    { cases x, dsimp only, tauto },
    { -- heq occurs here
      sorry, }
  end }

How should the final sorry be proved? By the way, this example is by Kevin Buzzard. The actual, more complicated, situation that inspired this is here if you're curious.

view this post on Zulip Reid Barton (Nov 11 2020 at 19:58):

Turn back and go another way

example : (A  B)  Σ (f : S  B), {φ : A  B //  (s : A) (h : s  S), φ s = f s, h } :=
{ to_fun := λ g, λ s, g s.1, g, λ _ _, rfl⟩⟩,
  inv_fun := λ p, p.2.1,
  left_inv := λ _, rfl,
  right_inv := begin
    rintros f, φ, h⟩,
    have : f = λ s, φ s.1, sorry,
    subst this,
  end }

view this post on Zulip Patrick Lutz (Nov 11 2020 at 20:03):

ohh, nice

view this post on Zulip Patrick Lutz (Nov 11 2020 at 20:03):

what exactly does subst do?

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 20:03):

(note that Reid changed inv_fun -- λ ⟨f, φ⟩ is not good style when defining data, as you are here.

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 20:04):

subst takes a proof of A = B and replaces all the A's everywhere by B's, or possibly the other way around

view this post on Zulip Reid Barton (Nov 11 2020 at 20:04):

oh yeah, I did that just in case it would help and then forgot to mention it

view this post on Zulip Bryan Gin-ge Chen (Nov 11 2020 at 20:04):

(Reid's sorry can be filled with simp [h].)

view this post on Zulip Kevin Buzzard (Nov 11 2020 at 20:04):

it's like rw h at * except that it's more powerful because it rewrites under binders. It literally removes A from the picture.

view this post on Zulip Patrick Lutz (Nov 11 2020 at 20:05):

oh, I see

view this post on Zulip Patrick Lutz (Nov 11 2020 at 20:05):

Kevin Buzzard said:

(note that Reid changed inv_fun -- λ ⟨f, φ⟩ is not good style when defining data, as you are here.

why is this bad?

view this post on Zulip Reid Barton (Nov 11 2020 at 20:07):

If you look at the goal in the original right_inv it's got some _match_1 or whatever junk in it

view this post on Zulip Reid Barton (Nov 11 2020 at 20:08):

more importantly, the version which matches in the lambda is less likely to reduce when applied to something

view this post on Zulip Reid Barton (Nov 11 2020 at 20:08):

though maybe in a case as simple as this one it doesn't really matter, not sure

view this post on Zulip Patrick Lutz (Nov 11 2020 at 20:09):

by the way, even though the example was originally by Kevin, I was the one who introduced the angle brackets


Last updated: May 08 2021 at 09:11 UTC