Equality of function on intersection

Stream: new members

[Emiel Lanckriet]

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?

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Kenny Lau]

0/0=0 btw

[Kevin Buzzard]

0/0=junk value

[Emiel Lanckriet]

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?

[Kevin Buzzard]

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

[Emiel Lanckriet]

Okay, I'll look into it, thanks.

[Eric Wieser]

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?

[Eric Wieser]

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

[Kevin Buzzard]

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

[Eric Wieser]

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

[Eric Wieser]

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.