test unique pair from two lists for a property, output bool

Stream: Is there code for X?

[Jared green]

i tried to write this:

variable {a :Type}[h : DecidableEq a] (l1 l2: List a) (f : a -> a -> Bool)
∃! s: a × a, s.1 ∈ l1 ∧ s.2 ∈ l2 ∧ f s.1 s.2

as a filtering condition over a list of pairs of lists. but then lean cant tell if thats decidable.

[Aaron Liu]

It seems like there are no definitions mentioning both docs#Decidable and docs#ExistsUnique.

If you add [DecidableEq a] then typeclass search finds
Decidable (∃ a ∈ l1, ∃ b ∈ l2, f a b ∧ ∀ c ∈ l1, ∀ d ∈ l2, f c d → a = c ∧ b = d)

[Edward van de Meent]

i imagine it might be easier to filter using List.product?

[Jared green]

yes it would, but i dont know the function

[Jared green]

list.existunique or list.one or something

[Edward van de Meent]

something like ((l1.product l2).filter (fun s => f s.1 s.2 = true)).length = 1

[Edward van de Meent]

import Mathlib

variable (α : Type) (l1 l2 : List α) [DecidableEq α] (f : α → α → Bool)

#synth Decidable (((l1.product l2).dedup.filter (fun s => f s.1 s.2 = true)).length = 1)