Zulip Chat Archive

Stream: general

Topic: Lost notations

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,
  sets_of_superset := begin
    rintros U V i, hi hUV,
    use i,
    change B.s i  V,
    transitivity U ; assumption,
  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.

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}

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!

Patrick Massot (Mar 05 2020 at 22:26):

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

Patrick Massot (Mar 05 2020 at 22:39):

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

Floris van Doorn (Mar 05 2020 at 22:41):

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

Mario Carneiro (Mar 06 2020 at 00:17):

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

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

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)

Kevin Buzzard (Mar 06 2020 at 07:02):

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

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