## Stream: new members

### Topic: List membership

#### Rob Simmons (Jun 10 2021 at 13:27):

I hope this "oh no help" question is acceptable here... I'm coming after a long break from Agda, and was trying to do some list membership definitions, reprising this Agda:

data _∈_ {a} {A : Set a} : A → List A → Set a where
Z : ∀{x xs} → x ∈ x :: xs
S : ∀{x y xs} (n : x ∈ xs) → x ∈ y :: xs


my first attempt looked like this, but I'm getting a universe error (universe level of type_of(arg #2) of 'isin.z' is too big for the corresponding inductive datatype), which I'm taking to mean that I'm surely doing something that I didn't mean to be doing:

inductive isin {A} : A -> List A -> Type where
| z : (x : A) -> (l : List A) -> isin x (x :: l)
| s : (x : A) -> (y : A) -> (l : List A) -> isin x l -> isin x (y :: l)


(also, some beginner guidance as to how I could find such a definition and associated lemmas, if they exist, would be awesome)

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:28):

Are you trying to define an inductive predicate?

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:28):

If so then the syntax is wrong.

#### Rob Simmons (Jun 10 2021 at 13:29):

Actually I think I figured out the problem by looking more closely at the Agda definition again: I needed to specify {A : Type} in the Lean definition! Because it was trying to generalize {A} to {A : Type u} which wouldn't work.

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:30):

Wait, I want to be sure that you are trying to define an inductive predicate, since I am Agda illiterate. Can you confirm?

#### Rob Simmons (Jun 10 2021 at 13:30):

Yes. The top data definition is an Agda inductive definition

#### Rob Simmons (Jun 10 2021 at 13:30):

The bottom inductive definition is me trying to transliterate that inductive definition into Lean

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:32):

This is the correct syntax:

inductive is_in { β : Type } : β → list β → Prop
| cons (x : β) (l : list β) : is_in x (x::l)
| trans (x y : β) (l : list β) : is_in x l → is_in x (y::l)


#### Huỳnh Trần Khanh (Jun 10 2021 at 13:34):

But honestly I wouldn't use an inductive predicate since an inductive predicate is uncomputable and a computable definition is just more natural.

#### Rob Simmons (Jun 10 2021 at 13:34):

Yes that seems like what I was trying to express, except that is there a reason for it to be a Prop instead of a Type?

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:34):

Aren't propositions types? But because of proof irrelevance, they are in a different universe, called Prop.

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:34):

Type is short for Type 0.

#### Rob Simmons (Jun 10 2021 at 13:36):

Hmm... I'm going to want to do induction over this definition, will Prop allow me to do that?

#### Rob Simmons (Jun 10 2021 at 13:36):

Seems like this now works as the definition I want:

inductive is_in {α: Type} (x : α) : List α -> Type where
| z {l : List α} : is_in x (x :: l)
| s {y : α} {l : List α} : is_in x l -> is_in x (y :: l)


#### Huỳnh Trần Khanh (Jun 10 2021 at 13:37):

Rob Simmons said:

Hmm... I'm going to want to do induction over this definition, will Prop allow me to do that?

Then yes. Prop allows you to do that. And you have proof irrelevance too, which can be really helpful in proofs.

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:37):

Also, you can specify a decision procedure for the inductive predicate. Type doesn't let you do that.

#### Horatiu Cheval (Jun 10 2021 at 13:37):

But honestly I wouldn't use an inductive predicate since an inductive predicate is uncomputable and a computable definition is just more natural.

But inductive predicates are in many cases easier to reason about (and I would say even more intuitive, but that's a matter of taste)

#### Huỳnh Trần Khanh (Jun 10 2021 at 13:38):

I agree. I was just commenting on that specific instance.

#### Horatiu Cheval (Jun 10 2021 at 13:41):

Hmm... I'm going to want to do induction over this definition, will Prop allow me to do that?

But if you choose to do it with Prop and then will want to define data, i.e. things in Type by induction, (or recursion, however you prefer to call it) on isin proofs then you won't be able to. So you should also take into consideration what you intend to do with isin

#### Yakov Pechersky (Jun 10 2021 at 14:28):

I do not agree that an inductive predicate is uncomputable. docs#list.decidable_mem

#### Rob Simmons (Jun 10 2021 at 15:03):

Thanks, this is helpful. Do you have any guidance as to whether I can find something similar that someone else might have already done?

#### Yakov Pechersky (Jun 10 2021 at 15:06):

Similar to what? Definitions of data structures? Or predicates on them?

#### Huỳnh Trần Khanh (Jun 10 2021 at 15:07):

Rob Simmons said:

Thanks, this is helpful. Do you have any guidance as to whether I can find something similar that someone else might have already done?

If you want to learn how Lean generally works, you can clone mathlib and read the source code. Don't worry, the source code is generally very readable.

#### Horatiu Cheval (Jun 10 2021 at 16:53):

I don't have the code anymore, but I actually tried to work with a similar inductive definition but for list inclusion, and as Type, not Prop (which as a coincidence was also based on some Agda code), that would also carry the information of "if x is the i-th element in the list l and l is included in l2, then this occurence of x is the j-th element of l2".

#### Horatiu Cheval (Jun 10 2021 at 16:55):

But I eventually ended up dropping it, because it didn't work well with the termination checking, and I didn't want to have to deal with termination proofs all over my code.

#### Yakov Pechersky (Jun 10 2021 at 16:58):

I am actually working on a proof of exactly this at the moment:

lemma sublist_iff_nth_eq {l l' : list α} :
l <+ l' ↔ ∃ (f : ℕ ↪o ℕ), ∀ (ix : ℕ), l.nth ix = l'.nth (f ix) :=
begin
split,
{ intro H,
induction H with xs ys y H IH xs ys x H IH,
{ simp },
{ obtain ⟨f, hf⟩ := IH,
simpa using hf },
{ obtain ⟨f, hf⟩ := IH,
refine ⟨⟨⟨λ ix, if ix = 0 then 0 else (f ix.pred).succ, _⟩, _⟩, _⟩,
{ rintro ⟨_|a⟩ ⟨_|b⟩,
{ simp },
{ simpa using (nat.order_embedding_succ_pos f a₂).ne },
{ simp },
{ simp } },
{ rintro ⟨_|a⟩ ⟨_|b⟩;
simp [nat.succ_le_succ_iff] },
{ rintro ⟨_|i⟩,
{ simp },
{ simpa using hf ix } } } },
{ rintro ⟨f, hf⟩,
sorry
},
end


#### Horatiu Cheval (Jun 10 2021 at 17:09):

That's wonderful! It looks like the idea I ended up with after dropping the inductive definition, but yours is more advanced and much better integrated with the standard library.

#### Horatiu Cheval (Jun 10 2021 at 17:10):

What does the righthookarrow with an o to its right mean? (sorry, I'm not at my computer and I can't type unicode)

#### Yakov Pechersky (Jun 10 2021 at 17:14):

It means an docs#order_embedding. Basically, a function f with the property that if x <= y then f x <= f y.

#### Horatiu Cheval (Jun 10 2021 at 17:19):

And do you think I would hit any major obstacle if I were to adapt it to use subtype instead of exists? Because ideally I would need to define data based on that index

#### Yakov Pechersky (Jun 10 2021 at 17:20):

What do you mean? You mean build such a function, given the prop that sublist?

Yes

#### Horatiu Cheval (Jun 10 2021 at 17:24):

Your construction of f seems constructive at first sight

#### Yakov Pechersky (Jun 10 2021 at 17:52):

Is this more of the thing you're thinking of?

def list_embed [decidable_eq α] : Π (l l' : list α), ℕ → ℕ
| []        _         := id
| _         []        := id
| (x :: xs) (y :: ys) := λ i, if x = y
then list_embed xs ys (i + 1)
else (list_embed (x :: xs) ys i) + 1


#### Horatiu Cheval (Jun 10 2021 at 17:59):

But this would mean than any list is included in the empty list, right?

#### Yakov Pechersky (Jun 10 2021 at 17:59):

This is just a mapping function. It might behave how you expect it to if you have an (h : l <+ l') hypothesis. Haven't tried it out.

#### Yakov Pechersky (Jun 10 2021 at 18:00):

It's the mathlib style of "define a total function, but it behave correctly only under some assumption"

#### Horatiu Cheval (Jun 10 2021 at 18:01):

Oh, I see what you mean. I'll try it out, thank you, this was very helpful

#### Mario Carneiro (Jun 10 2021 at 19:19):

By the way @Huỳnh Trần Khanh , I think Rob Simmons is using lean 4, that snippet is valid lean 4. @Rob Simmons We generally assume you are using lean 3 unless you are on the #lean4 or #mathlib4 streams

Last updated: Dec 20 2023 at 11:08 UTC