Setless proof of `Fin2 1 -> Fin2 1 \neq Fin2 2 -> Fin2 2`

Stream: Type theory

[nrs]

Is there a way to talk about cardinality of functions without referring to mathlib's ZFC sets? I was surprised how non-obvious proving (Fin2 1 -> Fin2 1) \neq (Fin2 2 -> Fin2 2) was without calling simp [Nat.card] (it seems to me a cardinality argument is the obvious method), and then further realized that is is probably not provable without funext. Do we have any notion of size that would make sense for these functions, in a purely type theoretical setting? And as a bonus, can we prove this can't be proven without funext internally in Lean?

[Eric Wieser]

I assume you're missing some parentheses there?

[nrs]

whoops! fixed thanks

[Eric Wieser]

I assume this proof doesn't satisfy you?

import Mathlib

example : (Fin 1 → Fin 1) ≠ (Fin 2 → Fin 2) := by
  intro h
  simpa using congr(Fintype.card $h)

[Eric Wieser]

Certainly there's no mention of ZFC sets

[Eric Wieser]

But even the definition of Fintype uses funext, as Mathlib makes absolutely no effort to avoid this axiom, and only a very small amount of effort to avoid Classical.choice

[nrs]

hm the issue is there's a call to Classical.choice here, and I might be mistaken, but the definition of Set A as A -> Prop combined with Classical.choice might be enough to imply this holds only in a set-theoretical model

[Eric Wieser]

Set shouldn't be involved in the above at all

[nrs]

but you're right that there's no explicit mention of mathlib's ZFC sets. I wonder if we can avoid Classical.choice completely?

[nrs]

Eric Wieser said:

Set shouldn't be involved in the above at all

right but it is enough for there to be any type A -> Prop which would behave as Set (in the case Set with Classical.choice can only be realized in a set-theoretical model)

[Eric Wieser]

So it looks like docs#List.nodup_range is one source of the use of choice, which might be easy enough to remove

[Eric Wieser]

But I would be surprised if Lean accepts a PR that removes the use of choice there

[nrs]

Multiset.pi too it seems

[nrs]

Eric Wieser said:

But I would be surprised if Lean accepts a PR that removes the use of choice there

oh this is mostly out of interest in mapping out the metatheory of Lean

[Eric Wieser]

I'm curious if the use of choice in docs#Multiset.pi is unavoidable or trivial

[Eric Wieser]

That one is in mathlib not Lean, so I'd be happy to merge a de-choicification if the proof readability doesn't majorly suffer

[nrs]

it comes from the generated Multiset.pi.proof_1 which I don't know much about, am currently investigating what it means

[Eric Wieser]

It's probably easier just to look at the source of Multiset.pi, which contains a by block corresponding to that

[Eric Wieser]

Looks like docs#Multiset.Pi.cons_swap is to blame

[Eric Wieser]

Fixed in #19990

[nrs]

Very cool! Thanks a lot for taking the time, it's a very nice change for metatheoretical purposes!

[nrs]

I will one day have time to write that command I've been meaning to write that singles out relevant lemmas for investigating their axiom usage, instead of a wall of #print axioms