Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC