Idea: Helper for speeding up Decidable on symmetric props

Stream: mathlib4

[Chris Wong]

The Decidable instance for Injective (docs#Fintype.decidableInjectiveFintype) takes the straightforward approach – it checks that every pair of inputs is mapped to distinct outputs.

However, this does twice as much work as necessary: if we've checked (a, b), we don't need to check (b, a).

I wonder if there's an easy way to skip the redundant pairs, perhaps using docs#Sym2 ?

I'm not sure how common it is to prove injectivity etc. with decide, but cutting the runtime in half sounds pretty cool.

(Context is writing this proof and thinking about why it might be slow :smile: )

[Edward van de Meent]

At best you're still only halving the number of checks tho

[Edward van de Meent]

I guess the best way to go about this might be to transform it by saying that for symmetric relations, xs.Pairwise r iff (xs : Finset).Pairwise r, at which point I think using decide should only do the lower triangle...

[Edward van de Meent]

docs#List.Pairwise

[Chris Wong]

I'm not sure what you mean by List.Pairwise. We're talking about Fintype here so it's already a Finset.

[Edward van de Meent]

I'm thinking that since it eventually is a quotient of lists by permutations, you may be able to make it reduce like this

[Chris Wong]

Hmm, that seems like a lot of work. I'm hoping we can just go decidable_of_iff' with docs#Sym2.fromRel_prop or similar and get the speedup for free.

[Aaron Liu]

This wasn't that hard, only tricky part was getting access to the underlying list. Also, removed [DecidableEq α]

import Mathlib.Data.Fintype.Basic

theorem Set.pairwise_list_iff_of_symmetric_of_nodup {α : Type*} {r : α → α → Prop} (hr : Symmetric r) {xs : List α} (hxs : xs.Nodup) :
    {x | x ∈ xs}.Pairwise r ↔ xs.Pairwise r := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    rw [List.nodup_cons] at hxs
    rw [List.set_of_mem_cons, Set.pairwise_insert, List.pairwise_cons, ih hxs.right, and_comm]
    apply and_congr_left'
    apply forall₂_congr
    intro b hb
    have : x ≠ b := by rintro rfl; exact hxs.left hb
    rw [eq_true this, true_implies]
    apply and_iff_left_of_imp
    apply hr

instance {α β : Type*} [Fintype α] [DecidableEq β] : DecidablePred (@Function.Injective α β) := fun f ↦
  Quotient.recOnSubsingleton (motive := (· = Finset.univ.val → Decidable f.Injective)) Finset.univ.val
    (fun (xs : List α) (h : Multiset.ofList xs = Finset.univ.val) ↦ decidable_of_iff (xs.Pairwise (f · ≠ f ·)) <| by
      have hd : xs.Nodup := by
        rw [← Multiset.coe_nodup, h]
        exact Finset.univ.nodup
      rw [← Set.pairwise_list_iff_of_symmetric_of_nodup (fun _ _ h ↦ h.symm) hd, Function.injective_iff_pairwise_ne]
      simp_rw [← Multiset.mem_coe, h, Finset.mem_val, Finset.mem_univ, Set.setOf_true, Set.pairwise_univ]) rfl

[Chris Wong]

Nice! Looks like this can apply to any symmetric reflexive relation.

[Chris Wong]

I guess the two advantages with the List.Pairwise approach are

1. We skip explicitly constructing the set of unordered pairs
2. We skip checking the diagonal (which lets us drop DecidableEq on the input type)

I'm curious about the performance impact of (1).

I believe we can address (2) in the Sym2 approach using docs#Finset.offDiag (or an alternative implementation that drops DecidableEq?) and docs#Finset.decidableDforallFinset .

[Eric Wieser]

I think at least one of @Yury G. Kudryashov and I have a DecidableEq-free version of offDiag, which is also more efficient

[Chris Wong]

That's cool! Unfortunately Finset.offDiag returns ordered pairs. We'll need something that combines Finset.offDiag and docs#Finset.sym2 I think

[Chris Wong]

I'm coming back around to Aaron/Edward's approach... we can package it up in def Finset.SymmetricPairwise := Quotient.lift List.Pairwise ... that hides the quotient shenanigans

[Kyle Miller]

@Chris Wong If you work down through Finset.sym2, Multiset.sym2, and List.sym2, the definition is

protected def List.sym2 : List α → List (Sym2 α)
  | [] => []
  | x :: xs => (x :: xs).map (fun y => s(x, y)) ++ xs.sym2

If you modify this to be

protected def List.offDiagSym2 : List α → List (Sym2 α)
  | [] => []
  | x :: xs => xs.map (fun y => s(x, y)) ++ xs.offDiagSym2

I think that gives you everything off the diagonal.

It shouldn't be so bad to prove that xs.offDiagSym2 = xs.sym2.filter (fun s => \neg s.IsDiag), and then you can build everything up again. Once you have Finset.offDiagSym2, you can make a Fintype instance for {s : Sym2 _ // \neg s.IsDiag }. One that doesn't use DecidableEq.

[Kyle Miller]

@Aaron Liu's instance is more straightforward and has less overhead. It avoids creating a list of all the unordered pairs, and instead it goes straight to computing.

Still, it'd be worth having the deleted diagonal sym2 theory worked out more.

[Chris Wong]

Another optimization is, if f is expensive, we want to avoid evaluating it repeatedly, so we want to check (xs.map f).Nodup instead. Which seems harder to generalize.

[Chris Wong]

:thinking:

import Mathlib

open List in
theorem Function.injective_iff_lift_nodup_map_univ {α β} [Fintype α] (f : α → β) :
    Injective f ↔
      Quotient.lift
        (fun xs => (xs.map f).Nodup)
        (fun xs ys (h : xs ~ ys) => by simp [(h.map f).nodup_iff])
        Finset.univ.val :=
  sorry

example {α β} (f : α → β) [Fintype α] [DecidableEq β] : Decidable (Function.Injective f) :=
  decidable_of_iff' _ (Function.injective_iff_lift_nodup_map_univ f)

[Yury G. Kudryashov]

One more optimization (at least, for large lists) in case β is a LinearOrder: use Chain' (. < .) ((xs.map f).mergeSort (. ≤ .)).

[Chris Wong]

Look ma! No quotients!

import Mathlib

variable {α : Type*} {β : Type*}

/--
A function `f` is injective on a `Finset` `s` if the image of `s` under `f` has no duplicates.
-/
theorem Finset.injOn_iff_nodup_map_val (f : α → β) (s : Finset α) :
    Set.InjOn f s ↔ (s.val.map f).Nodup := by
  induction s using Finset.cons_induction with
  | empty => simp
  | cons x xs hx h =>
    simp [Set.injOn_insert (show x ∉ (xs : Set α) by simpa)]
    tauto

/--
A function `f` with a finite domain is injective if its range has no duplicates.

This is useful for computation, as the right-hand side is usually more efficient.
-/
theorem Function.injective_iff_nodup_map_univ [Fintype α] (f : α → β) :
    Injective f ↔ (Finset.univ.val.map f).Nodup := by
  simpa [Set.injective_iff_injOn_univ] using Finset.injOn_iff_nodup_map_val f Finset.univ

example (f : α → β) [Fintype α] [DecidableEq β] : Decidable (Function.Injective f) :=
  decidable_of_iff' _ (Function.injective_iff_nodup_map_univ f)

[Chris Wong]

#21975 :octopus: