List membership

Stream: new members

[Rob Simmons]

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]

Are you trying to define an inductive predicate?

[Huỳnh Trần Khanh]

If so then the syntax is wrong.

[Rob Simmons]

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]

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]

Yes. The top data definition is an Agda inductive definition

[Rob Simmons]

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

[Huỳnh Trần Khanh]

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)

Is that your approach?

[Huỳnh Trần Khanh]

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]

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]

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

[Huỳnh Trần Khanh]

Type is short for Type 0.

[Rob Simmons]

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

[Rob Simmons]

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]

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]

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

[Horatiu Cheval]

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]

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

[Horatiu Cheval]

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]

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

[Rob Simmons]

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]

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

[Huỳnh Trần Khanh]

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]

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]

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]

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,
      use f.trans (nat.add_order_embedding 1),
      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]

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]

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]

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

[Horatiu Cheval]

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]

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

[Horatiu Cheval]

Yes

[Horatiu Cheval]

Your construction of f seems constructive at first sight

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

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

[Horatiu Cheval]

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

[Mario Carneiro]

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