Extract computational procedure of `List.Subset`

Stream: Is there code for X?

[Palalansoukî]

I want to extract a computational information from subset relation of lists. That is, I want to define function like List.Subset.toCompSubset:

import Mathlib

namespace List

variable {α : Type*}

inductive CompSubset : List α → List α → Type _
  | refl (l) : CompSubset l l
  | perm : CompSubset l₁ l₂ → l₂ ~ l₃ → CompSubset l₁ l₃
  | cons : CompSubset l₁ l₂ → CompSubset l₁ (a :: l₂)
  | double : CompSubset l₁ (a :: a :: l₂) → CompSubset l₁ (a :: l₂)

def Subset.toCompSubset [DecidableEq α] {l₁ l₂ : List α} :
    l₁ ⊆ l₂ → CompSubset l₁ l₂ := sorry

end List

A naive approach would be to define it inductively based on the number of duplicate elements, but that's far too cumbersome. Is there a better way?

[Eric Wieser]

Presumably you want a computational l₂ ~ l₃ in the perm constructor too?

[Palalansoukî]

It would be nice to obtain one for Perm as well! However, there are likely several ways to express it. (Personally) a promising approach is treating it as a bijection Fin l₁.length to Fin l₂.length that preserves elements of l₁ and l₂.

[Eric Wieser]

At any rate, the answer to your titular question is "no, there is nothing to extract because List.Subset is erased at runtime / cannot be eliminated from."

You have to come up with an algorithm yourself, in which you can only use h : l₁ ⊆ l to eliminate unreachable branches (via False.elim or similar)

[Wrenna Robson]

I recently asked a very similar question (albeit there for Sublist but it is the same principle). #Is there code for X? > Sublist elimination to Type

[Wrenna Robson]

Indeed @Eric Wieser, I don't know how you feel but it might be useful to merge those topics if they can.

[Wrenna Robson]

Palalansoukî said:

It would be nice to obtain one for Perm as well! However, there are likely several ways to express it. (Personally) a promising approach is treating it as a bijection Fin l₁.length to Fin l₂.length that preserves elements of l₁ and l₂.

We essentially have this now - docs#List.Perm.idxBij

[Wrenna Robson]

I cannot promise it is the most efficient algorithm (it seems likely that it is not) but it does work.

[Wrenna Robson]

We have a similar constructor for Subperm and Sublist though I think there is an error in it for the latter (in that it does indeed calculate an injection but it is not order-preserving, which in a sense is an issue with the approach I am using I think).

[Wrenna Robson]

One can use the approach as in the topic I linked to make it work for Sublist. Subset should also be doable but I am not sure one can construct it in the same way. Maybe though.

[Palalansoukî]

That's interesting. I think similar issues exist in various places. Indeed, List.Perm and List.Subset lack recursion, making them difficult to work with.

By the way, my original question was solved by myself, more straightforwardly than expected.

import Mathlib

namespace List

variable {α : Type*} [DecidableEq α]

def remove (a : α) : List α → List α := List.filter (· ≠ a)

@[simp] lemma remove_nil (a : α) : [].remove a = [] := by simp [List.remove]

@[simp] lemma eq_remove_cons {l : List α} :
    (ψ :: l).remove ψ = l.remove ψ := by induction l <;> simp_all [List.remove];

lemma remove_def (a b : α) (l : List α) :
    remove a (b :: l) = if a = b then remove a l else b :: remove a l := by
  simp [remove, List.filter]; grind

lemma mem_remove_iff {l : List α} : b ∈ l.remove a ↔ b ∈ l ∧ b ≠ a := by
  simp [List.remove]

inductive CompSubset : List α → List α → Type _
  | refl (l) : CompSubset l l
  | perm : CompSubset l₁ l₂ → l₂ ~ l₃ → CompSubset l₁ l₃
  | add (a : α) :
    CompSubset l₁ l₂ → CompSubset l₁ (a :: l₂)
  | double {a : α} :
    CompSubset l₁ (a :: a :: l₂) → CompSubset l₁ (a :: l₂)

lemma count_def (a b : α) (l : List α) :
    count a (b :: l) = if a = b then count a l + 1 else count a l := by
  simp [count]; grind

lemma perm_normalize (l : List α) (a : α) : l ~ replicate (l.count a) a ++ l.remove a :=
  match l with
  |     [] => by simp
  | b :: l => by
    by_cases h : a = b
    · simp [h, List.replicate, perm_normalize l]
    · suffices b :: l ~ replicate (count a l) a ++ b :: remove a l by simpa [h, remove_def, count_def]
      calc
        b :: l ~ b :: (replicate (l.count a) a ++ l.remove a) := by simp [perm_normalize l]
             _ ~ replicate (count a l) a ++ b :: remove a l   := Perm.symm perm_middle

namespace CompSubset

def iterated_double {l₁ l₂ : List α} {a : α} (h : k > 0)
    (c : l₁.CompSubset (replicate k a ++ l₂)) : l₁.CompSubset (a :: l₂) :=
  match k with
  |     1 => c
  | k + 2 => iterated_double (k := k + 1) (by simp) c.double

def trans {l₁ l₂ l₃ : List α} (c₁ : l₁.CompSubset l₂) (c₂ : l₂.CompSubset l₃) : l₁.CompSubset l₃ :=
  match c₂ with
  |     refl _ => c₁
  | perm c₂ hp => (c₁.trans c₂).perm hp
  |   add b c₂ => (c₁.trans c₂).add b
  |  double c₂ => (c₁.trans c₂).double

def cons {l₁ l₂ : List α} (c : l₁.CompSubset l₂) (a) : (a :: l₁).CompSubset (a :: l₂) :=
  match c with
  |     refl _ => CompSubset.refl _
  | perm c₂ hp => (CompSubset.cons c₂ a).perm (by simp [hp])
  |   add b c₂ => ((c₂.cons a).add b).perm (Perm.swap a b _)
  |  double (a := b) (l₂ := l₂) c₂ =>
    have : (a :: l₁).CompSubset (b :: b :: a :: l₂) := (c₂.cons a).perm (by grind)
    this.double.perm (Perm.swap a b l₂)

end CompSubset

def Subset.toCompSubst {l₁ l₂ : List α} (h : l₁ ⊆ l₂) : l₁.CompSubset l₂ :=
  match l₂ with
  |      [] =>
    have : l₁ = [] := by simpa using h
    this ▸ CompSubset.refl []
  | a :: l₂ =>
    if ha : a ∈ l₁ then
      have : l₁.CompSubset (replicate (l₁.count a) a ++ l₁.remove a) := (CompSubset.refl l₁).perm (perm_normalize l₁ a)
      have c₁ : l₁.CompSubset (a :: remove a l₁) := this.iterated_double (count_pos_iff.mpr ha)
      have : remove a l₁ ⊆ l₂ := by grind only [= subset_def, usr eq_or_mem_of_mem_cons, mem_remove_iff]
      have c₂ : (remove a l₁).CompSubset l₂ := Subset.toCompSubst this
      c₁.trans (c₂.cons a)
    else
      have : l₁ ⊆ l₂ := by grind
      CompSubset.add _ (Subset.toCompSubst this)

end List