Proof of Distinct Elements

Stream: lean4

[HenrikT]

Hi,
i am currently trying to prove a result in Lean4 without using Mathlib. However as i am not very versed in Lean i am kinda stuck. Maybe you guys can give me some advice ?

The Problem i am trying to solve is:
Given a List l, a proper Sublist sub of that List l contains an element e that is not in l.
I wrote this as the following theorem,

theorem list_prop_sub_ex_element_outside
(l : List α) (subset_l : sub ⊆ l) (neq_l : sub.toSet ≠ l.toSet) (length_l : l.length = length)  (l_nodup : l.Nodup) :
 ∃ (e : α), e ∈ l → e ∉ sub := by sorry

I tried a proof by induction over the length of l, the base case i managed to solve as it yields a contradiction. However the induction step is unclear to me.
Does anyone has some tips on how to solve this ?

Thanks in advance :)

[Kenny Lau]

what is length?

[HenrikT]

Its Nat
from l.length

[Kenny Lau]

what's your proof on pen-and-paper?

[Robin Arnez]

The problem becomes trivial depending on what your definition of List.toSet is

[HenrikT]

I don't have a pen-and-paper proof. I only tried doing it in LEAN4

[HenrikT]

How so ?

[Robin Arnez]

Is this your definition?

def List.toSet (l : List α) : α → Prop := fun x => x ∈ l

theorem list_prop_sub_ex_element_outside
    (l : List α) (subset_l : sub ⊆ l) (neq_l : ¬sub.toSet = l.toSet) :
    ∃ (e : α), e ∈ l ∧ e ∉ sub := by
  false_or_by_contra; rename_i h
  simp only [not_exists, not_and, Classical.not_not] at h
  apply neq_l
  ext a
  exact ⟨fun h' => subset_l h', h a⟩

[HenrikT]

my definition of List.toSet is

  def toSet : List α -> Set α
  | .nil => ∅
  | .cons h tail => (fun e => e = h) ∪ (List.toSet tail)

[Robin Arnez]

What is Set? I thought you worked without mathlib..?

[HenrikT]

Its from BasicLeanDataStructures/List/Basic.lean

[Kevin Buzzard]

@HenrikT maybe you should post a #mwe so that people can actually understand what the question is

[Robin Arnez]

Can you provide a link?

[Kevin Buzzard]

Right now we're just playing guessing games with your definitions

[HenrikT]

Set is imported from BasicLeanDataStructes/Set/Basic.lean

[Robin Arnez]

From where?

[Robin Arnez]

It's neither lean core, batteries or mathlib, is it custom repository?

[Kevin Buzzard]

Henrik can you click on the #mwe link so you can see what I'm suggesting you do in order to ask your question in a way that people can understand?

[HenrikT]

give me a second, i'll look up where it is from

[Robin Arnez]

Is it this? https://github.com/monsterkrampe/Basic-Lean-Datastructures

[HenrikT]

Yes

[Robin Arnez]

I don't like these definitions but

theorem list_prop_sub_ex_element_outside
    (l : List α) (subset_l : sub ⊆ l) (neq_l : ¬sub.toSet = l.toSet) :
    ∃ (e : α), e ∈ l ∧ e ∉ sub := by
  false_or_by_contra; rename_i h
  simp only [not_exists, not_and, Classical.not_not] at h
  apply neq_l
  funext a
  ext
  change a ∈ sub.toSet ↔ a ∈ l.toSet
  simp only [List.mem_toSet]
  exact ⟨fun h' => subset_l h', h a⟩

[Kenny Lau]

HenrikT said:

I don't have a pen-and-paper proof. I only tried doing it in LEAN4

Lean is not magic, particularly when you yourself said that you're not "very versed in Lean", you really need a maths proof first

[HenrikT]

Ok thank you very much, i'll try to understand it and ask back if i have any further questions. Also can you elaborate why you dont like the definition for sets. Is there a way it could be improved ?

[Robin Arnez]

I don't like that List.toSet is defined inductively when it could've just been fun x => x ∈ l

[Robin Arnez]

Also there's way too few API about Set in that library to make it any useful

[HenrikT]

Alright, maybe i'll suggest this change then.
Thanks for your help guys :)