A possible diamond

Stream: general

[Riccardo Brasca]

In a proof I am working on I got an error I don't fully understand, and it's possibly a diamond. The error is in number_theory/discriminant/basic, in the flt-regular repo, branch RB_possible_diam. Before spending some time to provide a minimal example, I would ask if someone immediately recognize the error. The type of this and the goal are quite long with set_option pp.all true, but almost identical. diff tells me that the only difference is

             @subtype.decidable_eq.{0} nat
               (λ (x : nat),
                  @has_lt.lt.{0} nat nat.has_lt x
                    (@power_basis.dim.{u v} K L
                       (@euclidean_domain.to_comm_ring.{u} K (@field.to_euclidean_domain.{u} K _inst_7))
                       (@division_ring.to_ring.{v} L (@field.to_division_ring.{v} L _inst_8))
                       _inst_10 pb))
               (λ (a b : nat), nat.decidable_eq a b) a b)

instead of

             classical.prop_decidable
               (@eq.{1}
                  (fin
                     (@power_basis.dim.{u v} K L
                        (@euclidean_domain.to_comm_ring.{u} K (@field.to_euclidean_domain.{u} K _inst_7))
                        (@division_ring.to_ring.{v} L (@field.to_division_ring.{v} L _inst_8))
                        _inst_10 pb)) a b))

Does someone recognize this error?

[Eric Wieser]

There's probably a mis-stated lemma somewhere

[Eric Wieser]

Which of those is your goal, and which is the lemma application?

[Riccardo Brasca]

The goal is

(vandermonde (⇑(algebra_map L E) ∘ ⇑(pb.basis))).det ^ 2 = 0

that is also the type of this (without set_option pp.all true). Let me see if I can produce a reasonable self contained example.

[Alex J. Best]

The error goes away if I get rid of the open locale classical and add all the decidable_eq iota arguments lean asks for

[Riccardo Brasca]

Being a stupid mathematician who doesn't know anything about classical I am very happy with this solution

[Eric Wieser]

Right, the underlying problem is either:

• you have a definition without a decidable argument (fine), but you unfold it (not fine) rather than adding a lemma that introduces the decidable argument
• you have a lemma that needs a decidable argument in its _statement_, but you let it fall back to the classical one (not fine)

[Eric Wieser]

Can you paste a permalink to the relevant lines?

[Riccardo Brasca]

Here it is

[Riccardo Brasca]

Note that both the lemma and this are actually false, but it doesn't matter.

[Eric Wieser]

Gitpod seems to run out of memory while trying to open that unfortunately... I had a bad cache

[Riccardo Brasca]

I've sorried the error

[Riccardo Brasca]

exact this should close the goal, but it doesn't.

[Eric Wieser]

As Alex suggests, you should remove open_locale classical, add decidable to all the lemmas with complaints in their statements, then add back open_locale classical

[Riccardo Brasca]

In any case I am trying to avoid open_locale classical and adding decidable_eq ι where is needed.

[Riccardo Brasca]

Ah, I should have both open_locale classical and decidable_eq ι?

[Yaël Dillies]

No no no.

[Yaël Dillies]

What you don't want is to put a classical.dec_something into the type of a lemma.

[Eric Wieser]

Riccardo Brasca said:

Ah, I should have both open_locale classical and decidable_eq ι?

Only if you want the former. It's fine to have it if it makes things convenient inside defs and proofs, but it can lead to traps in lemmas

[Yaël Dillies]

It's fine if it's in the proof, because you never need to match the proof.

[Eric Wieser]

In proofs you can always use tactic#classical, which is less of a trap

[Yaël Dillies]

That's what the classical linter checks.

[Eric Wieser]

I think the best approach is:

• Use the classical tactic in proofs that need it
• For noncomputable defs, create a very small section around only the def, and use open_locale classical in that section

[Eric Wieser]

Having open_locale classical at the top is a trap waiting to be sprung

[Eric Wieser]

So for instance;

-- it's fine to use the classical decidable_eq argument inside this def, because it's already
-- noncomputable anyway
section
open_locale classical
/-- Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define
`discriminant A ι b` as the determinant of `trace_matrix A ι b`. -/
def discriminant [fintype ι] (b : ι → B) := (trace_matrix A b).det
end

-- this needs a `decidable_eq` argument otherwise it's not general enough
lemma discriminant_def [fintype ι] [decidable_eq ι] (b : ι → B) :
  discriminant A b = (trace_matrix A b).det := by convert rfl

[Riccardo Brasca]

Sorry for the stupid question, but is this the same as adding [decidable_eq ι] to the def?

[Riccardo Brasca]

And in any case I should add noncomputable, right?

[Riccardo Brasca]

You should write a small tutorial for mathematicians :rolling_on_the_floor_laughing: . I've always thought putting

open_locale classical
noncomputable theory

at the beginning of the file means "let's do standard mathematics and forget about this CS stuff".

[Kyle Miller]

One of the "I don't care about decidability" solutions/band-aids is to use convert (and sometimes convert_to) in place of exact. It's able to deal with differing decidable instances.

[Kyle Miller]

(I haven't looked at what you're doing to see if it applies, but it can be a useful way to avoid redesigning definitions, even if that might be the right thing to do.)

[Eric Wieser]

Riccardo Brasca said:

Sorry for the stupid question, but is this the same as adding [decidable_eq ι] to the def?

No, because adding decidable_eq ι means that all the lemmas about it need to as well

[Eric Wieser]

Riccardo Brasca said:

And in any case I should add noncomputable, right?

You have noncomputable theory at the top of the file so that's not needed. If you want to remind yourself which things are computable, then remove noncomputable theory and add noncomputable wherever lean complains.

[Eric Wieser]

noncomputable theoryis indeed an "I don't care about this" lever, but open_locale classical just hides it until it bites you later

[Bryan Gin-ge Chen]

Riccardo Brasca said:

You should write a small tutorial for mathematicians :rolling_on_the_floor_laughing: . I've always thought putting

open_locale classical
noncomputable theory

at the beginning of the file means "let's do standard mathematics and forget about this CS stuff".

Perhaps we should have a new library note on this topic?

[Riccardo Brasca]

If I do

section
open_locale classical
/-- Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define
`discriminant A ι b` as the determinant of `trace_matrix A ι b`. -/
noncomputable
def discriminant [fintype ι] (b : ι → B) := (trace_matrix A b).det
end

lemma discriminant_def [fintype ι] (b : ι → B) : discriminant A b = (trace_matrix A b).det := rfl

it immediately complains because failed to synthesize type class instance for... [decidable_eq ι]. And if I add it I am not able to prove the lemma anymore. I am sure I am doing something wrong here...

[Eric Wieser]

Right, that's why in my comment I said:

-- this needs a `decidable_eq` argument otherwise it's not general enough
lemma discriminant_def [fintype ι] [decidable_eq ι] (b : ι → B) :
  discriminant A b = (trace_matrix A b).det := by convert rfl

[Eric Wieser]

That lemma needs [decidable_eq ι] because it's about trace_matrix

[Eric Wieser]

And one of the arguments to trace_matrix needs decidable_eq

[Riccardo Brasca]

OK, I don't care to add [decidable_eq ι], but rfl doesn't prove it.

[Eric Wieser]

Right, you need by convert rfl because you have to prove the two different decidable instances are equal

[Kyle Miller]

One of the tools in the toolbox for the mathematician who doesn't care about decidability is by convert rfl. Not sure if that works here

[Riccardo Brasca]

It doesn't :unamused:

[Riccardo Brasca]

Sorry, it does

[Eric Wieser]

I'm confused Riccardo; it worked in the snippet I posted

[Eric Wieser]

I think you're running into this because docs#algebra.trace_form needs a decidable_eq argument, but you could argue "it's noncomputable anyway, what's the point"

[Eric Wieser]

If you replaced that argument with the classical instance in the definition of docs#algebra.trace_form, then all the pain would fall inside mathlib and flt-regular wouldn't run into it

[Riccardo Brasca]

It's det that requires a decidable_eq I think, not trace_form.

[Riccardo Brasca]

There is no decidable_eq in docs#algebra.trace_form if I am not blind.

[Eric Wieser]

Ah you're right

[Riccardo Brasca]

OK, things are better and better. But now this line has become very slow. It think that everything comes from ¬discriminant A b = 0 and discriminant A b ≠ 0, but I am not even sure what ≠ means.

[Eric Wieser]

decidable_eq only matters when an ite / if is involved. It doesn't affect what = means

[Riccardo Brasca]

Maybe it's because I removed open_locale classical or whatever, but in practice the proofs where ≠ is involved are now broken.

[Eric Wieser]

I'm waiting for gitpod...

[Eric Wieser]

Anywhere you do rw discriminant you introduce a diamond

[Eric Wieser]

You have to use rw discriminant_def instead

[Riccardo Brasca]

Ah, this is good to know!

[Eric Wieser]

The problem you're running into with that by convert h line is weird

[Eric Wieser]

It looks like it might be a bug in the classical tactic

[Eric Wieser]

In that without the by convert it fails with:

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  λ (a b : ι), _inst (a = b)
inferred
  λ (a b : ι), classical.prop_decidable (a = b)

But _inst is precisely classical.prop_decidable, tactic#classical just isn't letting you know that

[Riccardo Brasca]

Writing discriminant_def instead of discriminant indeed fixes all the issues!

[Eric Wieser]

Not the slowdown though, right?

[Riccardo Brasca]

No

[Eric Wieser]

On gitpod this takes forever:

lemma zero_of_not_linear_independent [is_domain A] {b : ι → B} (hli : ¬linear_independent A b) :
  discriminant A b = 0 :=
begin
  by_contra h,
  sorry
end

Is this just gitpod?

[Riccardo Brasca]

Same here, I had to add classical at the beginning of the proof.

[Kyle Miller]

My short (and incomplete and opinionated) tutorial for mathematicians who don't want to learn much about decidability but still want to contribute to mathlib:

Decidability is a mechanism for helping us write definitions that are "computable," which has something to do with constructive mathematics, something classical mathematicians tend not to be familiar with. We say a Prop is decidable if there is some algorithm that can decide whether it is true or false; Godel proved no such algorithm exists for all Props. In classical mode, we pretend there is a noncomputable "algorithm" that can make these decisions.

1. Feel free to use open_locale classical and noncomputable theory. It will likely lead to less work down the road if you use the classical tactic instead of open_locale classical, but then you'll need to add all the decidable instances Lean will ask you for. It's up to you to decide which road to take.
2. Sometimes you will have things that will surprisingly not rewrite, or you'll have exacts that won't go through. This might be because of decidable instances not lining up (from the fake classical one being equal to but not being defeq to a real decidable instance). Try using convert_to to "refresh" these instances, or to surgically change one part of an expression to create a new goal that looks like the rw lemma you're trying to use; in this case, you can usually use convert to apply the rw lemma. For example, if both sides look the same but refl doesn't work, try convert rfl.
3. When you submit a PR to mathlib, be prepared for decidability experts to help you reconfigure your code to be more general (and maybe for them to tell you how much of a mess you've made of things -- but proving things at all is usually the hard part). This work will help people in the future avoid needing to use these convert/convert_to tricks.

It can also be worth running things by the decidability experts on Zulip ahead of time, since they'll likely have tricks to make a lot of this decidability wrangling less painful.

[Eric Wieser]

Riccardo Brasca said:

Same here, I had to add classical at the beginning of the proof.

I think this is a nasty bug somewhere (in by_contra or the instance lookup)

[Kyle Miller]

How can classical have a bug? It just adds classical.prop_decidable to the context and resets the instance cache. (If there's a bug, it must be really nasty.)

[Eric Wieser]

Kyle Miller said:

How can classical have a bug? It just adds classical.prop_decidable to the context and resets the instance cache. (If there's a bug, it must be really nasty.)

The bug is that it adds the instance as a have not a let

[Eric Wieser]

Which means subsequent tactics can end up with diamonds they can't resolve

[Riccardo Brasca]

Kyle Miller said:

1. Feel free to use open_locale classical and noncomputable theory. It will likely lead to less work down the road if you use the classical tactic instead of open_locale classical, but then you'll need to add all the decidable instances Lean will ask you for. It's up to you to decide which road to take.
   

This is what I've always done. But I discovered today it's not completely true...

[Kyle Miller]

Including step 2? That's the key part for this to actually be workable. (If annoying and many times painful!)

[Riccardo Brasca]

This is the original reason I opened this thread. If you look at the first message, I had

open_locale classical
noncomputable theory

at the beginning of the file, but I encountered a strange error at some point.

[Eric Wieser]

Eric Wieser said:

I think this is a nasty bug somewhere (in by_contra or the instance lookup)

The instance trace starts looking for docs#eq.decidable and docs#decidable_eq_of_decidable_le which starts a massive search for order instances

[Riccardo Brasca]

But indeed this may be because I was using rw [discriminant] instead of rw [discriminant_def], let me see.

[Kyle Miller]

@Riccardo Brasca Did you try convert this at the beginning? If the only difference is that decidable instance in the type, then it should have worked.

[Riccardo Brasca]

I got a timeout.

[Eric Wieser]

Ah, here's the problem in zero_of_not_linear_independent; you need to rw discriminant_def at h. If you do that, the by convert h goes away, and it is much faster

[Patrick Massot]

Kyle Miller said:

In classical mode, we pretend there is a noncomputable "algorithm" that can make these decisions.

This simply isn't true.

[Kyle Miller]

@Patrick Massot docs#classical.dec?

[Patrick Massot]

You can pretend anything you want but mathematicians don't pretend there is an algorithm here.

[Patrick Massot]

This kind of wording really isn't helping anything.

[Riccardo Brasca]

@Eric Wieser thank you! Now everything seems to be working normal. I am not sure I've understood what was the problem at the beginning, and why I cannot simply put open_locale classical, but I am happy anyway.

[Kyle Miller]

@Patrick Massot Thanks for the feedback that the scare quotes and wording aren't effective. How would you say it?

[Patrick Massot]

The main point is that going to classical mode is declaring not to be interested in computability aspects. It's not "pretending" false things.

[Eric Wieser]

@Riccardo Brasca, the problem comes down to the fact that when you forget to put decidable_eq T in a lemma statement, then either:

• You have no open_locale classical, and lean complains at you that you must add the argument. If you add this argument, your lemma is now as general as it need to be, and applies to all decision procedures.
• You have open_locale classical, and lean inserts classical.dec_eq or equivalent. As a result, your lemma is now about the classical.dec_eq instance, and not about arbitrary decision algorithms any more

The problem with the second outcome is that a later lemma inevitably introduces a decision algorithm such as "nat equality is obvious", and your lemma doesn't apply to it because your lemma is only about "the algorithm chosen using choice"

[Patrick Massot]

A more useful explanation is to give more details about how Lean uses decidable stuff. But I think this is already covered in TPIL.

[Eric Wieser]

I have a WIP linter that would have identified this problem, but I haven't found time to get it working properly

[Riccardo Brasca]

And then why it is OK to have open_locale classical for definitions?

[Eric Wieser]

It's about whether the instance appears on the LHS or the RHS of the :=. Letting classical instances leak into your type (aka statement) instead of parameterizing your type is almost always a bad idea, letting them leak into your implementation (aka proof) is fine

[Eric Wieser]

Perhaps a better spelling would have been to use the classical tactic in discriminant

/-- Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we define
`discriminant A ι b` as the determinant of `trace_matrix A ι b`. -/
def discriminant [fintype ι] (b : ι → B) := by classical; exact (trace_matrix A b).det

-- this needs a `decidable_eq` argument otherwise it's not general enough
lemma discriminant_def [fintype ι] [decidable_eq ι] (b : ι → B) :
  discriminant A b = (trace_matrix A b).det := by convert rfl

which also avoids the open_locale classical

[Reid Barton]

The real problem here is the idea that matrix.det "depends" on the decidable_eq ι instance at all

[Eric Wieser]

What would you propose? If you replaced that with a classical instance, this wouldn't work:

import linear_algebra.matrix.determinant
import data.matrix.notation

#eval matrix.det ![![(1 : ℤ), 2], ![3, 4]]

[Reid Barton]

That seems fine

[Riccardo Brasca]

Ok, I think I understand now the issue with my code. I can go home and let the discussion to you :sweat_smile:

[Reid Barton]

It's not like the definition of matrix.det is a good algorithm anyways

[Reid Barton]

Tying together the definition of a thing with the way to compute that thing just leads to a definition which is bad for both reasoning about and computing

[Reid Barton]

Unfortunately, I think mathlib is too far down this road already

[Eric Wieser]

Ah, your argument being that in lean4 we can still attach an efficient determinant implementation to a noncomputable definition?

[Reid Barton]

You could do it in Lean 3

[Eric Wieser]

Oh, actually I think I agree with your original claim after all

[Eric Wieser]

The only reason it requires decidable_eq is because docs#multilinear_map.map_add' uses it in a proof field

[Eric Wieser]

That's ridiculous, we can just use the classical instance in that field

[Eric Wieser]

Or put a [decidable_eq \io] argument on it

[Johan Commelin]

Reid Barton said:

Unfortunately, I think mathlib is too far down this road already

We always boast that mathlib isn't scared of large refactors. So this seems like a challenge. If we know what to do, let's just turn the library on its head.

[Eric Wieser]

Eric Wieser said:

Or put a [decidable_eq \io] argument on it

I'm going ahead with this to see what happens

[Mario Carneiro]

Eric Wieser said:

What would you propose? If you replaced that with a classical instance, this wouldn't work:

import linear_algebra.matrix.determinant
import data.matrix.notation

#eval matrix.det ![![(1 : ℤ), 2], ![3, 4]]

If we want to remove the decidability argument here, I would suggest having matrix.gaussian_elim_det and prove matrix.gaussian_elim_det = matrix.det

[Eric Wieser]

The decidability argument isn't even used in the computation, I don't think

[Eric Wieser]

It's used in a type it doesn't need to be in

[Mario Carneiro]

In fact, I think you can't even do gaussian elimination in an arbitrary ring, so we would need it to be a separate definition anyway

[Reid Barton]

There are polynomial-size arithmetic circuits (using only ring operations) to compute determinants but for computations that come up in practice, yeah, you would usually be working over a ring (or field!) where a better algorithm is available

[Mario Carneiro]

huh, I just checked wikipedia and all the listed O(n^3) algorithms require a field

[Reid Barton]

I don't remember whether the arithmetic circuits are O(n^3), might be O(n^4). It was not so easy to find this stuff.

[Mario Carneiro]

Is it possible to extend the ring to a field of fractions? There might be characteristic constraints

[Mario Carneiro]

Aha: http://page.mi.fu-berlin.de/rote/Papers/pdf/Division-free+algorithms.pdf

[Mario Carneiro]

indeed it's O(n^4)

[Eric Wieser]

Eric Wieser said:

It's used in a type it doesn't need to be in

#10140 (wip, needs propagating downstream)

[Eric Wieser]

This makes declaring multilinear_maps slightly harder, but using them easier

[Reid Barton]

Reid Barton said:

That seems fine

To be explicit, the simplest version of what I suggest would be to rename the current definition to matrix.det_naive_impl and wrap it in a by classical wrapper named matrix.det (like you suggested Riccardo do for discriminant), and continue to have all the lemmas be about the new matrix.det. Then in your #eval you have to type #eval matrix.det_naive_impl, but this isn't a big deal because if you wanted to compute the determinant of a matrix that wasn't tiny you would have needed to select a less naive implementation anyways.

[Reid Barton]

It seems pretty clear to me that being able to write #eval matrix.det instead of #eval matrix.det_naive_impl is not worth paying this decidable_eq tax whenever you just want to prove stuff.

[Reid Barton]

Of course if it happens that in this case the decidable_eq instance was unnecessary anyways then that's fine too.

[Kyle Miller]

Johan Commelin said:

Reid Barton said:

Unfortunately, I think mathlib is too far down this road already

We always boast that mathlib isn't scared of large refactors. So this seems like a challenge. If we know what to do, let's just turn the library on its head.

There's a way that almost works, and if we had an additional feature (erased_param) I think it should be very possible. The idea of erased_param is that it marks arguments that the VM should erase, in addition to the Prop arguments it already erases.

Here's what goes wrong right now. A variant of decidable but for types rather than props could be

class computable {α : Type*} (x : α) :=
(value : α)
(property : value = x)

so then if x is some noncomputable thing, computable.value x could potentially give a computable version. However, this x argument "infects" everything with noncomputableness, even if it is never used, like in this contrived example:

inductive unit' | mk

instance : nonempty unit' := ⟨unit'.mk⟩

noncomputable def unit'.mk' : unit' := classical.choice infer_instance

noncomputable -- (!)
instance unit'.mk'.computable : computable unit'.mk' :=
{ value := unit'.mk,
  property := by { generalize : unit'.mk' = x, cases x, refl, } }

If it were possible to write the class as

class computable {α : Type*} (x : erased_param $ α) :=
(value : α)
(property : value = x)

then (assuming in my ignorance that all the engineering challenges can be worked out) that instance wouldn't be noncomputable anymore and you would be allowed to do #eval computable.value unit'.mk'.

Other systems have this feature, like Agda.

[Kyle Miller]

(Instances of computable are free to depend on as many computable and decidable instances as they might want.)

[Reid Barton]

Kyle, didn't you have a version of something like this before that used erased? Does

class computable {α : Type*} (x : erased α) :=
(value : α)
(property : erased.mk value = x)

work?

[Kyle Miller]

Yeah, it's possible to mimic this using docs#erased, but I couldn't really get it to work in a smooth way.

[Kyle Miller]

In particular, using typeclass inference to build general computable instances from others. (I didn't try that hard, to be honest.)

[Reid Barton]

I guess what I would try is to put every instance in the form computable (erased.mk _) and have instances like [computable (erased.mk a)] [computable (erased.mk b)] : computable (erased.mk (a + b))... but you probably already tried that

[Reid Barton]

Maybe for Prop the fact that we have connectives that already work on the "erased" form is important, I don't know.

[Mario Carneiro]

That instance would have exposed noncomputable a and b though

[Kyle Miller]

Here were some experiments: https://gist.github.com/kmill/3808acff688ff3c0f26bc743146bcf4a

The problem is that computable (erased.mk _) poisons computability, so you need something else. I tried some notation:

notation `omni `:0 s := ( ⟨_, s, rfl⟩ : erased _)

("omniscient"). This lets you write computable (omni _) without that poisoning.

[Mario Carneiro]

but now that extra syntax is going to get in the way of typeclass inference

[Kyle Miller]

That was indeed the problem, and I couldn't find any way around that.

[Mario Carneiro]

I wonder if this is enough information for Leo to implement first-class docs#erased in the compiler? If erased A was defeq to A then everything would work

[Eric Wieser]

Reid Barton said:

Of course if it happens that in this case the decidable_eq instance was unnecessary anyways then that's fine too.

Turns out I'm wrong, while the instance is unnecessary in multilinear_map, it's still needed by docs#equiv.perm.sign

[Yakov Pechersky]

Does the laplacian expansion of det also need decidable_eq? Probably, since it's a sum over fintypes?

[Eric Wieser]

Isn't (-1)^(i + j) meaningless if your indices aren't ordered?

[Eric Wieser]

I feel like any attempt to generalize that term will require decidability

[Yakov Pechersky]

BTW reading the paper Mario shared, we have clows, called cycle, and cycles, which are cycle.nodup

[Kyle Miller]

Maybe if you want to avoid decidable_eq in matrix.det you could create a finset (bool × finset (n × n)), where finset (n × n) represents the graph of a permutation of n and the bool is its sign. Given one of these containing all permutations, you can define the determinant using the sum-over-permutations definition.

What might work for creating this is taking a list n representative l for finset.univ, calculating list.permutations l and zipping each with l, showing there are no dups so these lists can be written as a finset (n × n), then working out the sign sequence for these partitions and zipping the finsets with that, showing the resulting list has no dups to create a finset, and then showing the resulting finset didn't depend on the list n representative. It seems like decidable_eq isn't needed for any of these steps. (Though I'm not sure it's worth it.)

[Reid Barton]

FWIW given that fintype is constructive, it's odd that it doesn't provide decidable equality--it's not any of the standard constructive meanings of "finite".

[Yakov Pechersky]

This is because of the definition of list.nodup doesn't require decidable equality, iirc

[Yakov Pechersky]

At least, why it doesn't require it. Could one use it to provide a decidable_eq instance?

[Kyle Miller]

It doesn't need one because it's a Prop. If list.nodup were a decidable_pred, I think you could manufacture a decidable_eq.

[Reid Barton]

I think a faster way to describe Kyle's construction is to see that fintype X is basically trunc of a bijection fin n -> X, so if you have a matrix indexed by X you can precompose the rows and columns by that bijection and then take the determinant of that n x n matrix.

[Reid Barton]

The usual notion of finiteness would be trunc of an equiv fin n -> X.

[Kyle Miller]

That's a lot better than what I suggested.

[Reid Barton]

You still need to check that this isn't dependent on the bijection but if you don't mind admitting classical reasoning to prove this then there's certainly no problem.

[Kyle Miller]

docs#fintype.trunc_equiv_fin

[Eric Wieser]

Which requires decidable equality

[Reid Barton]

This is assuming decidable_eq--so having decidable equality is exactly being able to upgrade from bijection to equiv (since fin n definitely has decidable equality)

[Eric Wieser]

What are you referring to by bijection here? subtype bijective?

[Reid Barton]

In fact now I realize that what's weird about fintype is precisely that it mixes trunc and bijection, when most constructive settings don't even have both of these as distinct concepts.

[Reid Barton]

The point is that docs#fintype.complete is a Prop, when it "should" be some kind of witness data

[Eric Wieser]

Do we have fintype.trunc_fin_embedding that says fin (card X) embeds into a finite type X?

[Eric Wieser]

That wouldn't need decidable equality, which I think is what you were saying above.

[Kyle Miller]

It's funny how there's a difference between trunc {f : fin n -> X // bijective f}, which is whether the type's elements can be listed (but you don't know where in the list any given element is), and trunc {f : X -> fin n // bijective f} which is whether each element can be numbered (but you can't list out the elements). The second one implies decidable equality, and the first is basically fintype.

[Kyle Miller]

@Eric Wieser This should do:

def fintype.trunc_fin_bijective (α : Type*) [fintype α] :
  trunc {f : fin (fintype.card α) → α // function.bijective f} :=
begin
  generalize hn : fintype.card α = n,
  dunfold fintype.card finset.card at hn,
  refine quot.rec_on_subsingleton (@finset.univ α _).1
    (λ l (h : ∀ x : α, x ∈ l) (nd : l.nodup) (hn : l.length = n), trunc.mk _)
    finset.mem_univ_val finset.univ.2 hn,
  subst hn,
  use λ i, l.nth_le i i.property,
  split,
  { intros i j,
    rw nd.nth_le_inj_iff,
    exact fin.ext },
  { intro x,
    specialize h x,
    rw list.mem_iff_nth_le at h,
    obtain ⟨i, hi, rfl⟩ := h,
    exact ⟨⟨i, hi⟩, rfl⟩, },
end

[Kyle Miller]

#10141

[Kyle Miller]

Mario Carneiro said:

Aha: http://page.mi.fu-berlin.de/rote/Papers/pdf/Division-free+algorithms.pdf

Speaking of which, someone coincidentally posted a codegolf challenge about a division-free O(n^4) determinant algorithm yesterday: https://codegolf.stackexchange.com/questions/236835/birds-algorithm-for-computing-determinants

[Yaël Dillies]

Yes @pajonk, I think we can agree that a 1x1 matrix is not really a matrix

I believe that $0 \times 1$ and $1 \times 0$ matrices exist, and that they are different. :rolling_on_the_floor_laughing:

[Mario Carneiro]

lean says that "they are different" doesn't typecheck

[Yaël Dillies]

So they are very different!

[Yury G. Kudryashov]

"They are different" probably means that they are not docs#heq and I'm not sure that we can prove it.

[Riccardo Brasca]

I encountered another problem similar to the first one in this thread. In a proof, if I put

letI := λ (a b : E), classical.prop_decidable (eq a b),

everything is OK, but with

letI := classical.dec_eq E,

there is a problem. Does this mean there is a problem somewhere or I should just use classical.prop_decidable and be happy?

[David Wärn]

Yaël Dillies said:

Yes @pajonk, I think we can agree that a 1x1 matrix is not really a matrix

I believe that $0 \times 1$ and $1 \times 0$ matrices exist, and that they are different. :rolling_on_the_floor_laughing:

Fun fact: according to Lean, the type of $0 \times 1$ matrices equals the type of $0 \times 2$ matrices.

import data.matrix.basic

example {R m n : Type} : matrix empty m R = matrix empty n R :=
congr_arg (λ f : empty → Type, Π i, f i) (subsingleton.elim _ _)

[Eric Wieser]

Can you make a #mwe @Riccardo Brasca?

[Riccardo Brasca]

I think I have understood the problem: I recently added docs#polynomial.aeval_root_derivative_of_splits. This lemma uses, in the statement, docs#multiset.erase, that has [decidable_eq α] as an assumption.
The point is that docs#polynomial.aeval_root_derivative_of_splits does not have any [decidable_eq] in the assumptions, since at the beginning of the file there is open_locale classical, so I think Lean just uses λ (a b : L), classical.prop_decidable (eq a b). Now, if I use that lemma somewhere else where the same instance is filled using classical.dec_eq L I get a problem. Indeed

import logic.basic

example (L : Type*) : (λ (a b : L), classical.prop_decidable (eq a b)) = classical.dec_eq L := rfl

does not work. I don't know if this is the intended behavior or not. Maybe the correct solution is just to add [decidable_eq L] in docs#polynomial.aeval_root_derivative_of_splits even if there is open_locale classical?

[Riccardo Brasca]

So in practice I've solved my problem and I think I even really understood it :)

[Eric Wieser]

The problem is that docs#classical.dec_eq is a lemma but carries data

[Eric Wieser]

Lean never unfolds lemmas

[Eric Wieser]

Apparently that's necessary: https://leanprover-community.github.io/mathlib_docs/notes.html#classical%20lemma

[Riccardo Brasca]

I think that the confusion, at least for me, comes from the fact that

open_locale classical
lemma foo ...

is less general than

lemma foo1 [decidable_eq T]...

even if in foo1 it seems to be one assumption more than in foo.

[Riccardo Brasca]

Because foo only applies to the decidable_eq produced by classical, while foo1 applies to any decidable_eq instance.

[Riccardo Brasca]

This is surely a stupid thing, but I've understood it before

[Eric Wieser]

Yes, that's certainly true, but it doesnt'explain why classical.prop_decidable and classical.dec_eq aren't equivalent by rfl despite having the same implementation

[Eric Wieser]

I opened #10292 to see if the library note is still true

[Riccardo Brasca]

Sure, that is a deeper question. At the moment I am just looking to understand how to do classical mathematics, and I am more and more convinced that open_locale classical is not always the right way.

[Yaël Dillies]

David Wärn said:

Fun fact: according to Lean, the type of $0 \times 1$ matrices equals the type of $0 \times 2$ matrices.

I assume this doesn't work for $0 \times 1$ vs $1 \times 0$ nor $1 \times 0$$ vs $2\times 0$?

[Floris van Doorn]

David Wärn said:

Fun fact: according to Lean, the type of $0 \times 1$ matrices equals the type of $0 \times 2$ matrices.

import data.matrix.basic

example {R m n : Type} : matrix empty m R = matrix empty n R :=
congr_arg (λ f : empty → Type, Π i, f i) (subsingleton.elim _ _)

For those who are confused by this example (which included me), first consider this example:

lemma empty_pi {α β : empty → Type} : (Π i, α i) = (Π i, β i) :=
congr_arg (λ f : empty → Type, Π i : empty, f i) (subsingleton.elim α β)

This proof makes sense: α and β are both "functions" out of the empty type, so they're equal, so the Pi-types of them must also be equal.
Now the arrow-case is a direct consequence of this (recall that X → Y is just notation for Π _ : X, Y):

lemma empty_arrow {α β : Type} : (empty → α) = (empty → β) :=
empty_pi

and that's how the above proof works.

[Kevin Buzzard]

ha ha that's a funny proof David. Can you prove matrix m empty = matrix n empty? I'm not so sure this is provable.

[Kevin Buzzard]

Riccardo Brasca said:

This is surely a stupid thing, but I've understood it before

Here's another weird "choosing stuff" thing. These computer scientists took the axiom of choice too far. You know when in a proof we say "OK we know this set can't be empty so let's just choose an element at random; I don't care which one it is but I know it has these properties and those will be enough to finish the proof". The computer scientists want to know which element we pick, but we don't care, we would happily choose a different element next year when we are lecturing the same proof, so the computer scientists made this classical.choice thing where they choose exactly the same element every time. Before I appreciated this, I just thought that this choice axiom did nothing more than cases h with x hx when the goal was a Type, but then when I realised it was always the same x as opposed to a random one I think I felt a little giddy.

[Riccardo Brasca]

Same here!

[Kyle Miller]

That's one reason to sometimes avoid classical.choice in definitions: since it's actually picking out some unknown-to-you but very specific element, there's nothing that requires you to prove the choice it made didn't matter. (What if by some unlucky coincidences you manage to prove a "false" theorem because all the definitions chose the same elements with classical.choice?)

I was trying to think of the cases that feel safe to use it (from an avoiding-unluckly-coincidences perspective), and the only thing that comes to mind is when you want to extract the element of a singleton type (that includes the classical decidable instances).

There seems to be an awkward way to make it so you have to show choices didn't matter, but it's pretty awkward. If each definition that uses choice in a non-unique way exposes an arbitrariness type (for the auxiliary data that we imagine the choice function uses to make its choices), then you're forced to prove that the choice didn't matter. But then you have to manage these arbitrariness types and thread them correctly through all your definitions...

/-- Select an element of  `α` using the data from `x`. -/
noncomputable def my_choice {κ α : Type*} (x : κ) (h : nonempty α) : α :=
sigma.snd (@classical.choice (Σ (y : κ), α) ⟨⟨x, h.some⟩⟩)

The point is that this is now unprovable:

lemma unprovable {κ κ' α : Type*} (x : κ) (x' : κ') (h : nonempty α) :
  my_choice x h = my_choice x' h := sorry

But that's no good if everyone just chooses a random number:

lemma provable {α : Type*} (h : nonempty α) :
  my_choice 37 h = my_choice 37 h := rfl

[Chris Hughes]

Kevin Buzzard said:

Riccardo Brasca said:

This is surely a stupid thing, but I've understood it before

Here's another weird "choosing stuff" thing. These computer scientists took the axiom of choice too far. You know when in a proof we say "OK we know this set can't be empty so let's just choose an element at random; I don't care which one it is but I know it has these properties and those will be enough to finish the proof". The computer scientists want to know which element we pick, but we don't care, we would happily choose a different element next year when we are lecturing the same proof, so the computer scientists made this classical.choice thing where they choose exactly the same element every time. Before I appreciated this, I just thought that this choice axiom did nothing more than cases h with x hx when the goal was a Type, but then when I realised it was always the same x as opposed to a random one I think I felt a little giddy.

In some sense isn't this the whole point of choice. I was always confused by choice because in order to prove nonempty α you have to provide a witness anyway so why not just return the witness provided. Then I realised that the power lay in the fact that it always returns the same element regardless of the witness. I realised this when proving Lagrange's theorem. To prove the isomorphism of sets $H × G / H ≃ G$ you need choice. Given $g \in G$ you send it to the pair $(a^{-1}g, aH)$ where $a$ is an element of the same coset as $g$. You use $g$ to prove nonemptiness of the coset containing $g$ but you have to make sure you always choose the same element of the coset regardless of what element of the coset you start with.

I quite the following alternative version of choice when introducing the concept. They won't have to understand the difference between nonempty and inhabited or anything like that to understand it. It is ∀ {α : Sort u}, ∃ f : α → α, ∀ x y, f x = f y. I can't remember how strong it is compared with the other versions. I think it's pretty weak but I think it still covers a lot of uses of choice. I thought about this once but I can't remember.

[Mario Carneiro]

There is another theorem called docs#classical.axiom_of_choice (rarely used in mathlib because classical.choice is easier) which is closer to the version found in the textbooks. The reason classical.choice being a function is important is that it lets you use it in lambdas to get statements like classical.axiom_of_choice; it is actually strictly stronger though since axiom_of_choice still keeps everything behind an existential so it is not noncomputable in the lean sense and you can't use it to define noncomputable things

[Chris Hughes]

I guess the point is that the function should be random but not the element.

[Mario Carneiro]

the function should be a function

[Mario Carneiro]

this is a rare case where the function-ness is the important part

[Mario Carneiro]

Reading the proof of Diaconescu's theorem (src#classical.em) is great for understanding how powerful this property is