Type-valued induction on Finset?

Stream: new members

[aron]

I can see there are multiple induction principles for Finsets, like cons_induction, induction, induction_on, etc. But the motive returns Prop for all of them. Is there no induction for it that can be used to return a Type?

I wouldn't mind using a match in a recursive function but because it's a complex type I don't think it's possible to match on it in the way that I'd like to, like Finset.induction does: matching on the empty set in one case and on an existing set with a new item inserted in the other.

Similarly, Finset.rec or Finset.recOn also expose the internals of the type, which I don't want to deal with. How can I do this?

[aron]

Or is this not possible because extracting one item from the set at a time would require the axiom of choice? but why? it's a finite set, and besides Finset is a Type, not a Prop

[Aaron Liu]

The elements of the finset are unordered, but all the induction principles have to build up in some order

[Robin Arnez]

Yeah it's the same reason you can't write a fully generic safe, computable fold over a Finset (if you think about it, recursors behave similarly to folds). Except you can write a recursor if you add a requirement that the order doesn't matter. Multiset already has this with docs#Multiset.rec so you can straightforwardly extend it to Finset:

import Mathlib

@[elab_as_elim]
def Finset.consRec {α : Type u} {motive : Finset α → Sort v} (empty : motive ∅)
    (cons : ∀ (a : α) (s : Finset α) (h : a ∉ s), motive s → motive (.cons a s h))
    (cons_cons : ∀ (a b : α) (s : Finset α) (ha : a ∉ s) (hb : b ∉ s) (hab : a ≠ b) (ih : motive s),
      cons a _ (by simp [hab, ha]) (cons b s hb ih) ≍ cons b _ (by simp [hab.symm, hb]) (cons a s ha ih))
    (s : Finset α) : motive s :=
  Finset.casesOn s (Multiset.rec
    (fun _ => empty)
    (fun a s ih nd => cons a ⟨s, nd.of_cons⟩ (Multiset.nodup_cons.mp nd).1 (ih nd.of_cons))
    (fun a b s ih => Function.hfunext (by rw [Multiset.cons_swap])
      fun nd1 nd2 _ => cons_cons _ _ ⟨s, nd1.of_cons.of_cons⟩ _ _
        (by simp only [Multiset.nodup_cons, Multiset.mem_cons, not_or] at nd1; simp [nd1]) _))