Deciding Multiset.Rel for a partial equivalence

Multiset.Rel r s t holds when the elements of s and t can be matched one-to-one along r. For a general decidable r this is a bipartite-matching problem, but when r is symmetric and transitive on the elements involved, the greedy strategy — match each element of s to the first r-related element of t and discard the pair — is complete. This file implements the greedy matcher as a Boolean function on lists, proves it decides Multiset.Rel, and packages the result as a Decidable instance. The matcher recurses structurally, so the instance reduces in the kernel and concrete goals close by decide.

Main definitions

• List.isPermBy p l₁ l₂: greedy matching of l₁ against l₂ along the Boolean relation p — the algorithm of List.isPerm, with p in place of ==.

Main results

• Multiset.rel_coe_iff_exists: Rel r ↑l₁ ↑l₂ iff some reordering of l₂ is componentwise r-related to l₁.
• List.isPermBy_iff_rel': isPermBy p decides Multiset.Rel (p · ·), given symmetry and transitivity of p on a predicate covering both lists.
• Multiset.rel_symm_of_symm_on, Multiset.rel_trans_of_trans_on: symmetry and transitivity of Rel r from the corresponding properties of r on the members alone.
• Multiset.Rel.decidableRel: DecidableRel (Rel r) for decidable symmetric transitive r.

Implementation notes

Core's List.isPerm_iff proves the greedy matcher correct only under LawfulBEq, which forces p to coincide with equality. The lemmas here assume instead that p is symmetric and transitive on a predicate P covering the lists' members — the form a consumer needs when p is defined by recursion and its equivalence properties are only available beneath a termination bound (see RootedTree/DecEq.lean). The unconditional Std.Symm/IsTrans version is a corollary.

[UPSTREAM] candidate.

theorem Multiset.rel_coe_iff_exists {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {l₁ : List α} {l₂ : List β} : Rel r ↑l₁ ↑l₂ ↔ ∃ (l' : List β), List.Forall₂ r l₁ l' ∧ l'.Perm l₂

Rel r on coerced lists: some reordering of l₂ is componentwise r-related to l₁. The list-level reading of Multiset.Rel.

theorem Multiset.rel_symm_of_symm_on {α : Type u_1} {r : α → α → Prop} {s t : Multiset α} (hs : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → r x y → r y x) (h : Rel r s t) : Rel r t s

Rel r is symmetric when r is symmetric on the members.

theorem Multiset.rel_trans_of_trans_on {α : Type u_1} {r : α → α → Prop} {s t u : Multiset α} (ht : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ t → ∀ (z : α), z ∈ u → r x y → r y z → r x z) (h₁ : Rel r s t) (h₂ : Rel r t u) : Rel r s u

Rel r is transitive when r is transitive on the members.

def List.isPermBy {α : Type u_1} (p : α → α → Bool) : List α → List α → Bool

Greedy matching of l₁ against l₂ along p: pair each element of l₁ with the first p-related element of l₂, removing it. The algorithm of List.isPerm, with p in place of ==. Complete for Multiset.Rel (p · ·) when p is symmetric and transitive on the members (isPermBy_iff_rel').

Equations

• List.isPermBy p [] x✝ = x✝.isEmpty
• List.isPermBy p (a :: l₁) x✝ = match List.findIdx? (p a) x✝ with | some i => List.isPermBy p l₁ (x✝.eraseIdx i) | none => false

theorem List.rel_of_isPermBy {α : Type u_1} {p : α → α → Bool} {l₁ l₂ : List α} (h : isPermBy p l₁ l₂ = true) : Multiset.Rel (fun (a b : α) => p a b = true) ↑l₁ ↑l₂

Soundness of the greedy matcher against Multiset.Rel, hypothesis-free.

theorem List.isPermBy_refl {α : Type u_1} {p : α → α → Bool} (l : List α) : (∀ (x : α), x ∈ l → p x x = true) → isPermBy p l l = true

isPermBy p is reflexive when p is reflexive on the members.

theorem List.isPermBy_of_rel {α : Type u_1} {p : α → α → Bool} {P : α → Prop} (Ssymm : ∀ (x y : α), P x → P y → p x y = true → p y x = true) (Strans : ∀ (x y z : α), P x → P y → P z → p x y = true → p y z = true → p x z = true) {l₁ l₂ : List α} (hP₁ : ∀ (x : α), x ∈ l₁ → P x) (hP₂ : ∀ (x : α), x ∈ l₂ → P x) (h : Multiset.Rel (fun (a b : α) => p a b = true) ↑l₁ ↑l₂) : isPermBy p l₁ l₂ = true

Completeness of the greedy matcher against Multiset.Rel, given symmetry and transitivity of p on a predicate P covering both lists.

theorem List.isPermBy_iff_rel' {α : Type u_1} {p : α → α → Bool} {P : α → Prop} (Ssymm : ∀ (x y : α), P x → P y → p x y = true → p y x = true) (Strans : ∀ (x y z : α), P x → P y → P z → p x y = true → p y z = true → p x z = true) {l₁ l₂ : List α} (hP₁ : ∀ (x : α), x ∈ l₁ → P x) (hP₂ : ∀ (x : α), x ∈ l₂ → P x) : isPermBy p l₁ l₂ = true ↔ Multiset.Rel (fun (a b : α) => p a b = true) ↑l₁ ↑l₂

The greedy matcher decides Multiset.Rel, given symmetry and transitivity of p on a predicate P covering both lists.

theorem List.isPermBy_iff_rel {α : Type u_1} {p : α → α → Bool} (hs : ∀ (x y : α), p x y = true → p y x = true) (ht : ∀ (x y z : α), p x y = true → p y z = true → p x z = true) {l₁ l₂ : List α} : isPermBy p l₁ l₂ = true ↔ Multiset.Rel (fun (a b : α) => p a b = true) ↑l₁ ↑l₂

The greedy matcher decides Multiset.Rel for an unconditionally symmetric and transitive p.

theorem List.isPermBy_iff {α : Type u_1} {p : α → α → Bool} (hs : ∀ (x y : α), p x y = true → p y x = true) (ht : ∀ (x y z : α), p x y = true → p y z = true → p x z = true) {l₁ l₂ : List α} : isPermBy p l₁ l₂ = true ↔ ∃ (l' : List α), Forall₂ (fun (a b : α) => p a b = true) l₁ l' ∧ l'.Perm l₂

Characterization of the greedy matcher for a symmetric transitive p, the analogue of List.isPerm_iff: some reordering of l₂ is componentwise p-related to l₁.

theorem List.isPermBy_beq_iff_perm {α : Type u_2} [BEq α] [LawfulBEq α] {l₁ l₂ : List α} : isPermBy (fun (x1 x2 : α) => x1 == x2) l₁ l₂ = true ↔ l₁.Perm l₂

On a lawful BEq, the greedy matcher at (· == ·) decides permutation: isPermBy generalizes core's List.isPerm (compare List.isPerm_iff).

@[implicit_reducible]

instance Multiset.Rel.decidableRel {α : Type u_1} {r : α → α → Prop} [DecidableRel r] [Std.Symm r] [IsTrans α r] : DecidableRel (Rel r)

Multiset.Rel r is decidable, and computably so, for a decidable symmetric transitive r: decided by the greedy matcher on representatives, which reduces in the kernel.

Equations

• Multiset.Rel.decidableRel s t = Quotient.recOnSubsingleton₂ s t fun (l₁ l₂ : List α) => decidable_of_iff (List.isPermBy (fun (a b : α) => decide (r a b)) l₁ l₂ = true) ⋯