Zulip Chat Archive

Stream: new members

Topic: Equality of function on intersection


view this post on Zulip Emiel Lanckriet (Aug 13 2020 at 14:02):

I tried to define a theorem where one of the conditions was an equality on an intersection, but I run into problems with types.
Here is a minimal example of the problem:

example {X Y : Type*} {A B : set X} (f : A  Y) (g: B  Y)
    (h :  (x  A  B), f x = g x) : Prop := true

Do I need to cast stuff or use coe in some form? How do I resolve this?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:07):

Your problem is that terms of type set X are terms, not types, so you can't define functions on them without thinking a bit more carefully.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:09):

Given A : set X there is a corresponding type, called a subtype of X. Lean will call it \u A where \u is some little up-arrow. But now you can see the problem -- if Lean uses subtypes then if x is in A \cap B, the set, then x : X, so f x doesn't make sense

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:11):

import tactic

open set

example {X Y : Type*} {A B : set X} (f : A  Y) (g: B  Y)
  (h :  x : A  B, f x.1, inter_subset_left _ _ x.2 = g x.1, inter_subset_right _ _ x.2) : Prop := true

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:13):

x : A ∩ B means that x is a term of type equal to the subtype corresponding to A \cap B, so x is actually a pair: there's x.1, which is a term of type X, and there's x.2, which is a proof that x is in A \cap B. We need to evaluate f on something-corresponding-to-x, but f only eats pairs <x,p> where p is a proof that x is in A, so you have to supply the proof that if x is in A \cap B then x is in A directly

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:14):

If you think that this is a bit of a weird way to go about things, then you might want to consider the more normal type theory way to go about this stuff which would be to define f on all of X, and just let it be some junk value outside A. Then none of these problems occur.

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:15):

This is why we have 0/0=1 in Lean -- it's just more convenient to let / be defined on all of a field k rather than just the subset of non-zero elements of k.

view this post on Zulip Kenny Lau (Aug 13 2020 at 14:16):

0/0=0 btw

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:18):

0/0=junk value

view this post on Zulip Emiel Lanckriet (Aug 13 2020 at 14:38):

Okay, thanks, but I want to demand that f and g are continuous on their respective domains later (taking X and Y to be topological spaces), so how should I define these junk values in that case?

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 14:55):

you can still say they're continuous on A and B by using filters. This is the technique used in mathlib. We say something about it in the perfectoid paper

view this post on Zulip Emiel Lanckriet (Aug 13 2020 at 15:21):

Okay, I'll look into it, thanks.

view this post on Zulip Eric Wieser (Aug 13 2020 at 15:46):

Would it be possible to allow

 x : A  B, f x.1, inter_subset_left _ _ x.2 = g x.1, inter_subset_right _ _ x.2)

to be written

 x : A  B, f (x : A) = g (x : B)

in @Kevin Buzzard's example? Do those coe / lifts exist? If not, would it be sensible to add them?

view this post on Zulip Eric Wieser (Aug 13 2020 at 15:55):

This seems to work:

instance coe_left_inter {X : Type*} {A B : set X} : has_coe (A  B) A :=  λ x, x.1, inter_subset_left _ _ x.2 
instance coe_right_inter {X : Type*} {A B : set X} : has_coe (A  B) B :=  λ x, x.1, inter_subset_right _ _ x.2 

example {X Y : Type*} {A B : set X} (f : A  Y) (g: B  Y)
  (h :  x : A  B, f x = g x) : Prop := true

view this post on Zulip Kevin Buzzard (Aug 13 2020 at 16:42):

did you try recompiling mathlib afterwards? Kind of looks dangerous...

view this post on Zulip Eric Wieser (Aug 13 2020 at 17:35):

No, I didn't. I assume using has_lift instead of has_coe would avoid any danger, but frankly I have no idea

view this post on Zulip Eric Wieser (Aug 13 2020 at 17:42):

Asked over at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Coercions.20on.20subtypes/near/206845831, since this isn't really a "new members" question any more.


Last updated: May 12 2021 at 05:19 UTC