## Stream: new members

### Topic: typing error for ⊆

#### Justus Springer (Mar 18 2021 at 18:15):

Hello!
I'm currently learning lean and when playing around with basic properties of sets and images, I encountered a behavior which I find strange:

import data.set.basic

variables (X Y : Type) (f : X → Y)

open set

-- (1) works
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
begin
split,
{ intros h x hxS,
exact h (mem_image_of_mem f hxS) },
{ rintros h y ⟨x, hxS, hfx⟩,
rw ← hfx,
exact h hxS,
}
end

-- (2) works
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
begin
split,
{ exact λ h x hxS, h (mem_image_of_mem f hxS) },
{ exact λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS, }
end

-- (3) doesn't work: "function expected at h, term has type f '' S ⊆ T"
/-
example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
⟨λ h x hxS, h (mem_image_of_mem f hxS), λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS⟩
-/

-- (4) works (??)

example (S : set X) (T : set Y) : f '' S ⊆ T → S ⊆ f⁻¹' T :=
λ h x hxS, h (mem_image_of_mem f hxS)


I tried to incrementally translate the tactic-style proof of (1) into a term-proof. However, example (3), which I believed to be a quite canonical translation of (2) into a term proof, throws me the following error at the application of h:

function expected at
h
term has type
f '' S ⊆ T


I find this weird because I thought the term X ⊆ Y was _definitionally equal_ to ∀ ⦃a⦄, a ∈ X → a ∈ Y, i.e. a function type. Even weirder, when I only prove one implication as in (4), it works fine. Can someone help me understand what's going on here? Thanks!

#### Anne Baanen (Mar 19 2021 at 08:44):

The error goes away if you remind Lean of what you're trying to do:

example (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
⟨show f '' S ⊆ T -> S ⊆ f⁻¹' T, from λ h x hxS, h (mem_image_of_mem f hxS), λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS⟩


#### Anne Baanen (Mar 19 2021 at 08:45):

With set_option pp.all true, we can find a metavariable in the type of h:

function expected at
h
term has type
@has_subset.subset.{0} (set.{0} Y) ?m_1 (@set.image.{0 0} X Y f S) T


#### Anne Baanen (Mar 19 2021 at 08:47):

The metavariable is the ?m_1, which means there are some implicit arguments that Lean hasn't figured out by the time it checks that h is a function.

#### Anne Baanen (Mar 19 2021 at 08:49):

If we look at the definition of has_subset.subset, we see that this is the has_subset (set Y) instance, i.e. the definition of "S \subset T for sets is just ∀ {x], x ∈ S -> x ∈ T".

#### Anne Baanen (Mar 19 2021 at 08:53):

Why this happen in term mode and not in tactic mode is that the elaborator, which fills in these metavariables, tries to solve problems in a specific order, and apparently this order did not work well for this proof.

#### Justus Springer (Mar 19 2021 at 11:27):

Thank you, that has helped me a lot!

#### Mario Carneiro (Mar 19 2021 at 21:09):

Here's another version that works:

theorem T (S : set X) (T : set Y) : f '' S ⊆ T ↔ S ⊆ f⁻¹' T :=
⟨λ h x hxS, h (mem_image_of_mem f hxS), λ h y ⟨x, hxS, hfx⟩, hfx ▸ h hxS⟩


The only difference is that the example is now a theorem

#### Mario Carneiro (Mar 19 2021 at 21:10):

The issue is that it hasn't figured out what has_subset instance is being used by the time it sees h being used as a function. This is only a problem when the statement and proof are elaborated together, as happens in example and def

Last updated: May 08 2021 at 03:17 UTC