Is there a non-repeating list in Init or Std?

Stream: Is there code for X?

[Schrodinger ZHU Yifan]

Is there a lean version of NonRepeating list existing in Init or Std?

open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.List
open import Data.List.Relation.Unary.Any

data NonRepeating {a} {A : Set a} : (l : List A) → Set a where
  done : NonRepeating []
  rest : ∀ {x xs} → ¬ Any (x ≡_) xs → NonRepeating xs → NonRepeating (x ∷ xs)

record UniqueList {a} (A : Set a) : Set a where
  constructor _//_
  field
    l : List A
    wf : NonRepeating l

[Mario Carneiro]

not as a single type, but you can use List A and l.Nodup

[Mario Carneiro]

if you quotient up to permutation you get Finset A

[Schrodinger ZHU Yifan]

I end up with writing something:

inductive NoDup : List α → Prop
  | nil : NoDup []
  | cons a l : α ∉ l → NoDup l → NoDup (a :: l)

abbrev NoDupList α := @Subtype (List α) NoDup

def t : NoDupList Nat  := ⟨ [1, 2, 3], by
  apply NoDup.cons 1 [2, 3] (by simp)
  apply NoDup.cons 2 [3] (by simp)
  apply NoDup.cons 3 [] (by simp)
  apply NoDup.nil⟩

However, it is a little bit painful to use as lean cannot automatically give the proof of NoDup. ( you cannot writedef t : NoDupList Nat := ⟨ [1, 2, 3], by simp ⟩).

Is it possible to write a macro to generate the code? Could you please show me an example?

def t NoDupList Nat := NoDupList![1, 2, 3]
-- generates =>
def t : NoDupList Nat  := ⟨ [1, 2, 3], by
  apply NoDup.cons 1 [2, 3] (by simp)
  apply NoDup.cons 2 [3] (by simp)
  apply NoDup.cons 3 [] (by simp)
  apply NoDup.nil⟩

[Kevin Buzzard]

docs#List.Nodup is there already

[Schrodinger ZHU Yifan]

I see, it actually has by decide

[Eric Wieser]

{l : List α // l.Nodup} would be the canonical spelling I think

[Schrodinger ZHU Yifan]

How can I achieve something similar to (the following is rejected):

import Std.Data.List.Basic
open Std
inductive X :=
  | A
  | B (xs : { l: List (String × X) // l.map (·.1) |>.Nodup })

[Patrick Massot]

Interesting riddle. Minimized version:

import Std.Data.List.Basic
open Std

-- Works
inductive X' :=
  | A : X'
  | B : (l: List X') → X'

-- Fails
inductive X :=
  | A : X
  | B : (l: List X) → (hl : l.length < 3) → X

[Adam Topaz]

(deleted)

[Adam Topaz]

that wasn't the intended type, sorry

[Eric Wieser]

FWIW, l.map (·.1) |>.Nodup is effectively docs#List.NodupKeys

[Eric Wieser]

To save someone loading up Lean, Patrick's example fails with:

application type mismatch
  List.length l
argument has type
  _nested.List_1
but function has type
  List X → Nat

[Schrodinger ZHU Yifan]

Also, the following won't work.

import Mathlib.Data.List.AList

inductive X :=
  | A
  | B (xs : AList (α := String) (fun _ => X))

[Eric Wieser]

I think this is just a bug

[Eric Wieser]

Certainly it's a bug that _nested is appearing in the error message

[Eric Wieser]

I think it would be appropriate to file a Lean4 issue on github here

[Mario Carneiro]

I don't think so, AList is a subtype, which requires evaluating NodupKeys on the nested inductive type List (String x X)

[Mario Carneiro]

if you inline everything you will see it can't be defined

[Mario Carneiro]

this has approximately the same error:

inductive X :=
  | A
  | B
    (entries : List (Σ _:String, X))
    (nodupKeys : entries.NodupKeys)

commenting out the last line makes it work

[Schrodinger ZHU Yifan]

emmm, but you can do something like:

inductive X :=
  | private A' : X
  | private B' : (l: List α) → (hl : l.length < 3) → X

def X.B := X.B' (α := X)
def X.A := X.A'

[Mario Carneiro]

that's not the same thing, X.B' still quantifies over all types α

[Mario Carneiro]

note that X is universe bumped because of this

[Mario Carneiro]

An inductive type has constructors and also a recursor. Just because you define a more specific constructor wrapper doesn't mean the recursor is also made more specific

[Mario Carneiro]

if you did recursion on X you would have to deal with arbitrary other types α in the B' case

[Eric Wieser]

Mario Carneiro said:

if you inline everything you will see it can't be defined

In that case, the lean4 bug is "the error message should say this can't be done, and not just reveal some error in an implementation detail"

[Eric Wieser]

Is there a way to get at the "inlined" version that uses this _nested.List_1?

[Mario Carneiro]

No, I think that definition never actually exists in the environment

[Mario Carneiro]

It's hard to see much about it because it only ever shows up in error messages

[Mario Carneiro]

but the gist of it is that when compiling a nested inductive type, lean has to make copies of all inductive types involved in the "cycle" while creating the type of the recursor. You can see a bit of this in the simplified inductive:

inductive X :=
  | A
  | B
    (entries : List (Σ _:String, X))

#print X.rec

recursor X.rec.{u} : {motive_1 : X → Sort u} →
  {motive_2 : List ((_ : String) × X) → Sort u} →
    {motive_3 : (_ : String) × X → Sort u} →
      motive_1 X.A →
        ((entries : List ((_ : String) × X)) → motive_2 entries → motive_1 (X.B entries)) →
          motive_2 [] →
            ((head : (_ : String) × X) →
                (tail : List ((_ : String) × X)) → motive_3 head → motive_2 tail → motive_2 (head :: tail)) →
              ((fst : String) → (snd : (fun x ↦ X) fst) → motive_1 snd → motive_3 { fst := fst, snd := snd }) →
                (t : X) → motive_1 t

Here there are 3 motives for 3 mutually inductive types, which you might call X, List_Sigma_String_X and Sigma_String_X. During post-processing, these types are replaced with the types they are supposed to be standing in for, namely X, List ((_ : String) × X) and (_ : String) × X respectively.

The trouble is that the type List_Sigma_String_X created during this process isn't actually List _, so if you try to apply a function like List.NodupKeys it will be a type error. In lean 3 this type would actually stick around and you could see it in the reduction, but in lean 4 it disappears after elaboration so you just have a reference to a type _nested.List_1 that doesn't exist

[Eric Wieser]

I think the thing I was struggling with is why lean can't insert some conversion function between the temporary list and the real one; but I guess the answer is that that would amount to using a recursor of a type within its own definition which isn't allowed

[Schrodinger ZHU Yifan]

I am not sure what‘s agda’s vec equivalence in lean. but with that，I guess I can do it a different way like:

B takes an implicit (n : nat), then separate list into two finite vec, associated with some prop on the first vec of string.

Emmm, but it seems tedious to use.

[Schrodinger ZHU Yifan]

Oh, no it won’t. Vec does not give the same length. Only an upper bound.

[Mario Carneiro]

Eric Wieser said:

I think the thing I was struggling with is why lean can't insert some conversion function between the temporary list and the real one; but I guess the answer is that that would amount to using a recursor of a type within its own definition which isn't allowed

Right, this gets into inductive-recursive types if you want to do this (which are supported in agda but are strictly stronger in proof strength than what lean supports)

[Mario Carneiro]

it's not even about having the conversion function, having any function there which inspects the type nontrivially (like List.length) is already recursion

[Eric Wieser]

What type of inspection is trivial?

[Mario Carneiro]

Function.const

[Eric Wieser]

That's a pretty dubious meaning of inspect

[Eric Wieser]

It would be nice if the error message included the words "inductive-recursive types are not supported"

[Mario Carneiro]

that is, if you have some function which would type check even if the argument had type x : A for some variable type A

[Eric Wieser]

Would a custom elaborator work to build such a "function", or would that be elaborated fully before making the substitution?

[Mario Carneiro]

not sure what you mean

[Schrodinger ZHU Yifan]

Back to the problem, I think to achieve the constrains, one can do something like:

inductive Vec (α : Type) : Nat → Type :=
  | nil  : Vec α 0
  | cons : α → Vec α n → Vec α (n+1)

def Vec.NoDup (x : Vec α n) : Prop := sorry

inductive X : Type :=
  | A : X
  | B : {n : Nat} → {v : Vec String n // v.NoDup } → Vec X n → X

-- Mathlib version won't work
-- inductive X' : Type :=
--  | A : X'
--  | B : {n : Nat} → {v : Vector String n // v.val.Nodup } → Vector X' n → X'

I am not sure whether there is a better way to do this.