Zulip Chat Archive

Stream: new members

Topic: typing error for ⊆


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip Justus Springer (Mar 19 2021 at 11:27):

Thank you, that has helped me a lot!

view this post on Zulip 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

view this post on Zulip 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