typing error for ⊆

Stream: new members

[Justus Springer]

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]

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]

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]

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]

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]

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]

Thank you, that has helped me a lot!

[Mario Carneiro]

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]

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