Zulip Chat Archive

Stream: general

Topic: Lost notations


view this post on Zulip Patrick Massot (Mar 05 2020 at 22:21):

For expository purposes, I'm trying to rewrite part of filter theory. But Lean loses its notations. In the following code (ran with Lean 3.5.1, not yet 3.6.0), do you see set membership and set inclusion notations disappearing from tactic state? Do you understand why?

import tactic
open set

structure base_de_filtre (X : Type*) :=
(ι        : Type*)
(s        : ι  set X)
(defaut   : ι)
(inter    :  i j,  k, s k  s i  s j)

structure filtre (X : Type*) :=
(sets             : set (set X))
(univ_sets        : univ  sets)
(sets_of_superset :  {U V}, U  sets  U  V  V  sets)
(inter_sets       :  {U V}, U  sets  V  sets  U  V  sets)

def filtre_de_base {X : Type*} (B : base_de_filtre X) : filtre X :=
{ sets := {U |  i : B.ι, B.s i  U},
  univ_sets := begin
    use B.defaut,
    intros x hx,
    trivial,
  end,
  sets_of_superset := begin
    rintros U V i, hi hUV,
    use i,
    change B.s i  V,
    transitivity U ; assumption,
  end,
  inter_sets := begin
    rintros U V i, hi j, hj,
    cases B.inter i j with k hk,
    use k,
    intros x hx,
    exact hi (hk hx).1, hj (hk hx).2,
  end }

This is driving me crazy.


view this post on Zulip Patrick Massot (Mar 05 2020 at 22:23):

I see tactic states like:

1 goal
X : Type ?,
B : base_de_filtre X
⊢ set.mem univ {U : set X | ∃ (i : B.ι), set.subset (B.s i) U}

view this post on Zulip Patrick Massot (Mar 05 2020 at 22:24):

I just noticed the strange Type ? in the pasted state. Removing all Type* makes Lean use notations again!

view this post on Zulip Patrick Massot (Mar 05 2020 at 22:26):

Thanks to everybody (from every universe) who helped me fixing this.

view this post on Zulip Patrick Massot (Mar 05 2020 at 22:39):

I'm still interested in reading more explanation about why Lean is losing notations here.

view this post on Zulip Floris van Doorn (Mar 05 2020 at 22:41):

I could reproduce it, and it looks really weird. No idea why this happens.

view this post on Zulip Mario Carneiro (Mar 06 2020 at 00:17):

I recall @Chris Hughes filed a bug about this a while back

view this post on Zulip Mario Carneiro (Mar 06 2020 at 00:18):

The use of universe metavariables causes structure literals to unfold notations like has_mem.mem for some reason

view this post on Zulip Mario Carneiro (Mar 06 2020 at 00:19):

(This isn't actually a notation issue in the sense of printing; set.mem has no notation, only has_mem.mem. The question is why has_mem.mem was unfolded)

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 07:02):

Is it the issue which is fixed by writing Type u instead of Type *?

view this post on Zulip Kevin Buzzard (Mar 06 2020 at 11:16):

weird coincidence -- this just happened to me when bundling subgroups. For me the universe u trick fixes it.


Last updated: May 14 2021 at 03:27 UTC