Decidability with fintype

Stream: new members

[Jérémie Turcotte]

Hi, I currently have a hypothesis

h1: ∃ (a : V), G.connected_component_mk a = A

I would like to break the exists to get said a. Cases gives me error "induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop". I know I can use choose or classical.some, but for interest of understanding how this works, I'd like to not use anything like that. Let me note that V is fintype, so it appears to me that this should be easy to do (algorithmically, one might just go through every a:V and find one). How would one code this, if possible? Thanks for your help.

[Matthew Ballard]

have ⟨a,h2⟩ := h1 destructures an existential proposition

[Jérémie Turcotte]

I get "invalid 'begin-end' expression, ',' expected" when I do this (I have indeed written , at the end of the line). And when I click inside the <> I get "unknown identifier 'a'", "unknown identifier 'h2'" as errors

[Matthew Ballard]

Is this Lean 3?

[Matthew Ballard]

I am going to guess it probably is, stop offering Lean 4 advice, and go to bed. :)

[Matt Diamond]

are you in term mode or tactic mode?

[Matt Diamond]

if you're in tactic mode it might explain why that destructuring syntax didn't work... but that's besides the point

[Jérémie Turcotte]

Yeah Lean 3

[Matt Diamond]

docs#fintype.choose exists, but it requires proof of uniqueness

[Jérémie Turcotte]

Tactic mode, inside a begin...end block

[Jérémie Turcotte]

Interesting, but sadly it is not unique

[Matt Diamond]

my instinct tells me that Lean probably won't allow you to computably choose a "random" element that satisfies some predicate

[Matt Diamond]

for example, you might try to take the finset of elements in the fintype and convert it to a list, but docs#finset.to_list is noncomputable

[Matt Diamond]

the reason the uniqueness proof is needed with fintype.choose is because it removes the element of randomness and narrows down the search to a single mathematically defined object

[Matt Diamond]

I'm far from a Lean expert, so it's possible that there's a method that I'm unaware of... perhaps someone else will weigh in

[Matt Diamond]

docs#nat.find only requires an existence proof, but (I think) that's because you have an order and you're specifically requesting the "least" one, so it's not random

[Matt Diamond]

if your fintype has a well founded order on it, you might be able to find what you need using docs#is_well_founded.fix

[Jérémie Turcotte]

Ok yeah I see what you mean. In my head something being finite (having cardinality n) means there is an bijection between that and {1,...n}, but that may not be true in this type theory stuff (I'm still pretty new) and so we can't computably choose one such bijection (im looking at docs#fintype.trunc_fin_bijection for instance but there is some weird trunc thing going on to maintain computability). I was mostly trying to use this for some decidability properties that are required for when adding stuff in the graph theory part of mathlib. I liked the idea of it being the most elementary possible, but I'm really close to just doing everything classically. Not sure how people working on mathlib feel about that?

[Matt Diamond]

I liked the idea of it being the most elementary possible, but I'm really close to just doing everything classically. Not sure how people working on mathlib feel about that?

Like are they okay with using the axiom of choice all over the place?

[Junyan Xu]

In my head something being finite (having cardinality n) means there is an bijection between that and {1,...n}, but that may not be true in this type theory stuff (I'm still pretty new) and so we can't computably choose one such bijection

You can choose the first element of a list using docs#list.find, but docs#multiset is a quotient of list where the order is forgotten, so there is no longer a well-defined first element, and docs#finset (which underlies docs#fintype) consists of multisets without duplicate elements. So you can't pick an element if it's it not unique, without using some extra structure (like a linear order to narrow down to a unique element) or choice. If you are in a proof and not constructing data, obtain ⟨a,h2⟩ := h1 should work though, because any two proofs of the same Prop are same to Lean, no matter what a you use in the proof.

[Yakov Pechersky]

Jérémie, are you trying to prove something using such an a : V, or construct data? Seems like the latter, since you are trying to eliminate into something that isn't Prop. How would your constructed data vary if you somehow chose a different a' : V?

[Kevin Buzzard]

Yeah, if cases doesn't work it sounds like you're abusing tactic mode ie your goal is not a true-false statement. Just use exists.somein this case.

[Patrick Johnson]

Jérémie Turcotte said:

In my head something being finite (having cardinality n) means there is a bijection between that and {1,...n}, but that may not be true in this type theory stuff (I'm still pretty new) and so we can't computably choose one such bijection

If something is finite, there indeed exists a bijection between it and $\left\{1,\dots,n\right\}$. It has nothing to do with computability.

[Junyan Xu]

Yeah that's actually the definition of docs#finite. However since it's a Prop you can't get back the bijection computably: no matter what bijection you use to prove finiteness, the resulting proofs are all equal; this is called proof irrelevance in type theory. The idea is that you can't get back lost/forgotten information computably. docs#fintype.trunc_fin_bijection uses a quotient (docs#trunc) to collapse all bijections to a single element; it is computable because a term in the trunc type carries no more information than the mere existence of a bijection. This "truncated" bijection can then be used to define other data that does not depend on the choice of the bijection.