cases on finite vs. infinite

Stream: new members

[Patrick Lutz]

Suppose I know that some property holds when X is fintype and when X is infinite. How do I prove that it holds for all X? I am fine with using classical logic/choice if need be. MWE

constant foo : Type → Prop
axiom finite_foo (X : Type) [fintype X] : foo X
axiom infinite_foo (X : Type) [infinite X] : foo X

example (X : Type) : foo X := sorry

[Kevin Buzzard]

What's the definition of infinite? I don't have access to lean right now

[Patrick Lutz]

class infinite (α : Type*) : Prop :=
(not_fintype : fintype α → false)

[Patrick Lutz]

There's also set.infinite for saying a subset of a type X is infinite

[Patrick Lutz]

If I should be using that instead, that's fine too

[Kevin Buzzard]

The infinite class you quoted above just says not a fintype so it should be easy to do with that class

[Kevin Buzzard]

You can just do cases on nonempty (fintype X) right?

[Markus Himmel]

(deleted)

[Patrick Lutz]

Kevin Buzzard said:

You can just do cases on nonempty (fintype X) right?

Yeah, I guess that sounds right. I was trying to do cases on infinite and for some reason was getting stuck proving that something that's not infinite is fintype

[Kevin Buzzard]

You might want to look at where nonempty is defined because there will be a useful lemma in the API saying that if you're not nonempty then there's a map to false

[Patrick Lutz]

Kevin Buzzard said:

You might want to look at where nonempty is defined because there will be a useful lemma in the API saying that if you're not nonempty then there's a map to false

hmm, it looks like nonempty is in core/init/logic.lean but I don't see anything about having a map to false.

[Kevin Buzzard]

I want something which says not nonempty X -> (X -> false)

[Patrick Lutz]

okay, wait, I found it with library_search

[Kevin Buzzard]

Assume h : not nonempty X, intro x, apply h, use x

[Kevin Buzzard]

So that should be all you need

[Patrick Lutz]

not_nonempty_iff_imp_false

[Patrick Lutz]

Okay, now I have the proof

example (X : Type) : foo X :=
begin
    by_cases h : nonempty (fintype X),
    exact nonempty.elim h (λ (x : fintype X), @finite_foo X x),
    exact @infinite_foo X (not_nonempty_fintype.mp h),
end

which seems simple enough to satisfy me. Thanks for the help @Kevin Buzzard!

[Patrick Lutz]

I think the main thing I didn't think of was doing cases on nonempty (fintype X) though in retrospect it makes sense I guess