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]) _))

[aron]

Ooh. @Robin Arnez could you explain this a bit? I can't see how it expresses the requirement that the order doesn't matter. And does that requirement mean I can't use this recursor to return one arbitrary element from a non-empty set?

[Robin Arnez]

It's the cons_cons part that requires you to prove that swapping the order doesn't change the outcome. If you try to just extract an element this condition will fail:

def Finset.extractElement (x : Finset α) : Option α :=
  x.consRec none (fun a _ _ _ => some a) <| by
    intro a b s has hbs hab ih
    simp [hab]
    -- goal is False

... unless you trunc or squash it:

def Finset.extractElement (x : Finset α) : Option (Trunc α) :=
  x.consRec none (fun a _ _ _ => some (.mk a)) <| by
    intro a b s has hbs hab ih
    simp [eq_true (Trunc.eq _ _)]

[Jakub Nowak]

Taking arbitrary element of nonempty Finset would require using axiom of choice. But axiom of choice is not computable, that's why you can only produce Prop, and not Type. See Classical.choice.
You can in some sense take an arbitrary element of an Finset, but only if you provide the proof, that it doesn't matter which arbitrary element is taken. Or in other words, you must prove that the function acting on this arbitrary element gives the same result for any element. This is more-or-less what cons_cons is for.