Zulip Chat Archive

Stream: general

Topic: map from sigma type


Kevin Buzzard (Nov 08 2021 at 19:28):

aargh I can't figure out a basic type theory thing. As part of LTE I want to relate binary sums to sigma types over a type with two terms, but I'm failing to write down the map from the sigma type to the binary sum:

import tactic

variables S T : Type

def X : bool  Type
| ff := S
| tt := T

def foo : Σ a, X S T a  S  T := -- the obvious map, sending (ff,s) to s and (tt,t) to t
λ x, @sigma.rec bool (X S T) (λ _, S  T) (λ b st, @bool.rec (λ _, S  T) (sum.inl st) (sum.inr st)) x
/-
type mismatch at application
  sum.inl st
term
  st
has type
  X S T b
but is expected to have type
  S
-/

Ideally I'd like to avoid the equation compiler because I'm doing this as a let in the middle of a tactic proof, but I could just break this definition out if necessary.

Eric Wieser (Nov 08 2021 at 19:32):

Fwiw, X is docs#cond

Eric Wieser (Nov 08 2021 at 19:33):

And if you're lucky we have docs#equiv.sum_equiv_sigma_bool

Kevin Buzzard (Nov 08 2021 at 19:34):

aah got it -- docs#sum_equiv_sigma_bool

Kevin Buzzard (Nov 08 2021 at 19:36):

so the key is to use match, which seems to me to somehow be strictly more powerful than sigma.rec the way I was using it because it forces x.2 to have the right type. Nice!

Eric Rodriguez (Nov 08 2021 at 19:37):

it also parses as Σ a, (X S T a → S ⊕ T) the way you wrote it, fyi

Kevin Buzzard (Nov 08 2021 at 19:38):

fortunately that wasn't true in my actual use case but thanks!

Eric Rodriguez (Nov 08 2021 at 19:48):

in your original code, this seems to work:

def foo : (Σ a, X S T a)  S  T := -- the obvious map, sending (ff,s) to s and (tt,t) to t
@sigma.rec _ _ (λ _, S  T) (λ b, @bool.rec_on (λ b, X S T b  S  T) b sum.inl sum.inr)

was a super pain to get the elaborator to work, though; I did it in tactic mode, turned on pp.all and show_term, and then worked backwards removing what could be removed and not what couldn't

Kevin Buzzard (Nov 08 2021 at 20:38):

Aah I had the motive wrong! no that's not it -- you moved st after the colon, that's the trick I was missing.

Kevin Buzzard (Nov 08 2021 at 20:45):

Yeah with that trick you don't even need the @s, like in the match case:

def foo' : (Σ a, X S T a)  S  T :=
λ x, sigma.rec (λ b, bool.rec (sum.inl) (sum.inr) b) x

Thanks!

Kyle Miller (Nov 08 2021 at 21:01):

Kevin Buzzard said:

so the key is to use match, which seems to me to somehow be strictly more powerful than sigma.rec the way I was using it because it forces x.2 to have the right type. Nice!

For those following along (like me), this is a match that implements it:

def foo'' : (Σ a, X S T a)  S  T
| ff, x := sum.inl x
| tt, y := sum.inr y

Kevin Buzzard (Nov 08 2021 at 21:04):

Yeah, I didn't try pattern matching with my original goal because I was in the middle of a proof, and pattern matching failed when I tried in my example above because of my bracket fail :D


Last updated: Dec 20 2023 at 11:08 UTC