WellFounded List SSubset

Stream: Is there code for X?

[Ka Wing Li]

I am trying to prove the following, but seem to get stuck.

instance :HasSSubset (List α) :=
  ⟨λ l₁ l₂ => l₁ ⊆ l₂ ∧ ¬ l₂ ⊆ l₁⟩

instance List.isWellFounded_ssubset : IsWellFounded (List α) (· ⊂ ·) := by
  sorry

[Ka Wing Li]

I am trying to use SubRelation based on List.length but seems do not go well.

[Ka Wing Li]

Is there any lemma on subset and length of list? I can only find lemmas with sublists but it is not helpful.

[Aaron Liu]

I don't think this one is true.

[Kenny Lau]

Aaron Liu said:

I don't think this one is true.

i'm quite sure it is

[Aaron Liu]

import Mathlib

instance {α : Type*} : HasSSubset (List α) :=
  ⟨λ l₁ l₂ => l₁ ⊆ l₂ ∧ ¬ l₂ ⊆ l₁⟩

theorem List.subset_iff {α : Type*} [DecidableEq α] (l l' : List α) : l ⊆ l' ↔ l.toFinset ⊆ l'.toFinset := by
  apply forall_congr'
  intro a
  rw [List.mem_toFinset, List.mem_toFinset]

theorem List.ssubset_iff {α : Type*} [DecidableEq α] (l l' : List α) : l ⊂ l' ↔ l.toFinset ⊂ l'.toFinset := by
  apply and_congr
  · exact subset_iff l l'
  · exact (subset_iff l' l).not

instance List.isWellFounded_ssubset {α : Type*} : IsWellFounded (List α) (· ⊂ ·) := by
  classical
  conv =>
    enter [2, a, b]
    rw [List.ssubset_iff]
  change IsWellFounded (List α) (InvImage (· ⊂ ·) List.toFinset)
  infer_instance