Pointing out contradiction during case destruction

Stream: new members

[Scott Buckley]

I have a proof state with an assumption i : Fin 0. Obviously this isn't possible, but i'm wondering if there's a neat way to dispatch the current goal in this case. I could perform the following:

rcases i with ⟨i, contra⟩ ; cases contra

but my spider senses tell me there is probably a more elegant way to do this, apart from using apply (Fin.elim0 i). Let's imagine Fin.elim0 didn't already exist.

I find it very satisfying when it's possible to use something like rcases x with ⟨x, rfl⟩ to both extract an equality and globally rewrite using that equality (obviously not with Fin assumptions). I figure that's possible because rfl is the constructor for equality, so it's just doing more destruction there, and identifying a contradiction is a different kind of animal. But still, are there any neat tricks around things like this?

[Yaël Dillies]

example (i : Fin 0) : False := by
  obtain ⟨_, ⟨⟩⟩ := i

is one option

[Vlad]

cases i.2

[Kevin Buzzard]

@loogle Fin 0

[Scott Buckley]

@Yaël Dillies that's exactly what I was looking for!

rcases i with ⟨i, ⟨⟩⟩

I hadn't seen the empty mk notation before. I'll still use Fin.elim0, but i'm glad to have learned something new :) I guess there we are just destructing i.2 without specifying any new term names or recursive destructors. very cool.

[loogle]

:search: Fin.elim0, Fin.subsingleton_zero, and 285 more

[Kevin Buzzard]

(oh sorry, you already knew about docs#Fin.elim0)

[Eric Wieser]

apply i.elim0 also works if you're optimizing for shortness

[Scott Buckley]

Thanks everybody. I cant believe how quick all these replies were haha

[Eric Wieser]

Or even exact ![] i maybe!

[Scott Buckley]

Eric Wieser said:

exact ![] i

This didn't work for me. Can you walk me through how that's supposed to work?

[Vlad]

![] is docs#Matrix.vecEmpty, defined as docs#Fin.elim0. The issue here is that ![] contains values of types in Sort (u+1), and proofs belong to propositions in Sort 0.