set like equivalence of lists without converting to finsets

Stream: Is there code for X?

[Jared green]

is there an equivalent of

l1 : List a
l2 : List a
l1 ⊆  l2 && l2 ⊆ l1

other than

List.isPerm l1 l2

that will work on lists of different lengths and different numbers of duplicates

[Kenny Lau]

I don't think they're equivalent

[Kenny Lau]

but why do you need such a predicate?

[Kenny Lau]

can you give us more context?

[Jared green]

i know they arent exactly the same, but i asked the same question earlier and isPerm is the answer i got, but it turned out not to be general enough for what i was doing. a shorter form of 'they are subsets of each other' would shorten my code a bit. and i dont want to have to import finset unnecessarily.

[Kenny Lau]

what is your code doing?

[Jared green]

restricted resolution where the literals in the clause pairs are the same but just one has opposing polarity. the rest of resolution is done elsewhere

import Batteries.Data.List.Basic
import Mathlib.Data.List.Defs
import Mathlib.Order.Defs.PartialOrder
import Mathlib.Data.List.Sublists

def Clause := List (Nat × Bool) deriving DecidableEq, Membership
variable {a : Type}
variable {toProp : Nat -> Prop}

def isResolvable (c1 c2 : Clause) : Bool :=
  let lits1 := c1.map (·.1)
  let lits2 := c2.map (·.1)
  lits1 ⊆  lits2 && lits2 ⊆ lits1 &&
  (c1.product c2).all₂ (fun l1 l2 => (l1.1.1 = l1.2.1 && l2.1.1 = l2.2.1  &&
  l1.1.2 != l1.2.2 && l2.1.2 != l2.2.2)  -> l1.1.1 = l2.1.1) (c1.product c2)

def generateResolvents (clauses : List Clause) : List Clause :=
  List.flatten (
    List.map (fun c1 =>
      (List.filter
      (fun c2 => c1 == c2 || isResolvable c1 c2) clauses).map
      (fun c2 => c1.inter c2)
      ) clauses)

[Jakub Nowak]

What's wrong with converting to finsets?

[Yury G. Kudryashov]

If you don't care about multiplicities, then you can say {x | x ∈ l1} = {x | x ∈ l2}.

[Jakub Nowak]

Yury G. Kudryashov said:

If you don't care about multiplicities, then you can say {x | x ∈ l1} = {x | x ∈ l2}.

That's undecidable though.

[Jakub Nowak]

But l0.toFinset = l1.toFinset is decidable.

[Jared green]

nothing in particular is wrong with converting to finset, however given that every other set operation and predicate has a functional equivalent for lists that doesn't do such a conversion(except existsunique), why wouldn't this one?

[Jakub Nowak]

You should think about what gives most readable code. For me l0.toFinset = l1.toFinset is easy to understand. I don't think l0.eqAsSets l1 is better, because it pretty much says exactly the same, but in english. Unless you can come up with a better name for this property, I don't see much need for this.