DecidableEq diamond on Fin

Stream: lean4

[Yaël Dillies]

I have discovered that Mathlib's docs#Fin.instLinearOrder induces a diamond for DecidableEq (Fin n):

import Mathlib.Order.Fin.Basic

example (n : ℕ) : instDecidableEqFin n = instDecidableEq_mathlib := rfl -- fails

[Yaël Dillies]

This is due to the LinearOrder (Fin n) instance being defined through docs#LinearOrder.liftWithOrd, which itself uses docs#decidable_of_iff

[Yaël Dillies]

... and this is the obvious thing to be doing: We want to prove Decidable (x ≤ y) from Decidable (↑x ≤ ↑y) by "rewriting" using decidable_of_iff. In particular, I don't think that we should change docs#Fin.instLinearOrder .

[Yaël Dillies]

Hence, even though the problem is created by Mathlib, it eventually boils down to two core constructs, namely docs#instDecidableEqFin and docs#decidable_of_iff, being defined in incompatible ways.

[Yaël Dillies]

Would people be happy with a PR redefining instDecidableEqFin using decidable_of_iff?

[Yaël Dillies]

... and here is the Mathlib-free MWE that the above Mathlib-full MWE boils down to:

example (n : Nat) : instDecidableEqFin n = fun x y ↦ decidable_of_iff _ Fin.val_inj := rfl -- fails

[Kim Morrison]

I suspect there is going to be a bootstrapping issue here: instDecidableEqFin is in Init.Prelude, and I think is needed immediately.

[Yaël Dillies]

I did notice that, but decidable_of_iff doesn't really depend on anything either, right?

[Kim Morrison]

I guess so! Happy to take a look if you want to make a draft PR to this effect.

[Yaël Dillies]

I am trying to write the PR as we speak, but I am discovering that I don't even know how to get the Lean server started on the lean4 repo! I get the following error (on Windows, if relevant):

Error while checking Lean version: info: downloading component 'lean' error: could not download nonexistent lean version `lean4-stage0` info: caused by: could not download file from 'https://github.com/leanprover/lean4/releases/expanded_assets/lean4-stage0' to 'C:⋃ info: caused by: http request returned an unsuccessful status code: 404 Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })

[Matthew Ballard]

elan toolchain link lean4-stage0 build/release/stage0 assuming you have already built things

[Yaël Dillies]

Matthew Ballard said:

assuming you have already built things

What "things"?

[Eric Wieser]

Yaël Dillies said:

In particular, I don't think that we should change docs#Fin.instLinearOrder .

I don't really agree with this; I think changing the instance would be fine (but so is your approach)

[Matthew Ballard]

stage0 and stage1 -- I'll find the link

[Matthew Ballard]

https://lean-lang.org/lean4/doc/make/index.html#generic-build-instructions

[Kim Morrison]

Yaël Dillies said:

Matthew Ballard said:

assuming you have already built things

What "things"?

mkdir -p build/release
cd build/release
cmake ../..
cd ../..
make -j32 -C build/release

(only the last line necessary on subsequent runs)

[Julian Berman]

-j32

:dollar_bills:

[Yaël Dillies]

Hmm,

Matthew Ballard said:

https://lean-lang.org/lean4/doc/make/index.html#generic-build-instructions

Doing this I'm stuck on installing libuv

[Yaël Dillies]

Kim Morrison said:

mkdir -p build/release
cd build/release
cmake ../..
cd ../..
make -j32 -C build/release

Doing this too

[Markus Himmel]

Yaël Dillies said:

Doing this I'm stuck on installing libuv

Stuck in what way?

[Yaël Dillies]

I don't know what instructions to follow

[Markus Himmel]

Which operating system are you using?

[Yaël Dillies]

I'm on gitpod, so Ubuntu

[Henrik Böving]

Yaël Dillies said:

I'm on gitpod, so Ubuntu

The instructions here give the right packages to install: https://lean-lang.org/lean4/doc/make/ubuntu.html