Data.Fintype.Vector mathlib4#1716

Stream: mathlib4

[Johan Commelin]

On

instance Vector.fintype [Fintype α] {n : ℕ} : Fintype (Vector α n) :=
  Fintype.ofEquiv _ (Equiv.vectorEquivFin _ _).symm

I get

IR check failed at 'Fintype.ofBijective._at.Vector.fintype._spec_2._rarg', error: unknown declaration 'Pi.fintype'

[Johan Commelin]

Making it noncomputable of course fixes the issue. But I imagine that's not what we want.

[Johan Commelin]

Pi.fintype definitely does exist, as #check confirms.

[Johan Commelin]

Aha. Pi.fintype is noncomputable!

[Eric Wieser]

docs#pi.fintype, docs4#Pi.fintype

[Eric Wieser]

It was computable in mathlib3

[Eric Wieser]

What changed?

[Johan Commelin]

The Lean version?

[Ruben Van de Velde]

I've regularly had lean4 claim things needed to be noncomputable when they weren't in lean3. I haven't looked into why

[Eric Wieser]

Ah, this is because docs4#Multiset.recOn is noncomputable

[Eric Wieser]

Like all other recursors

[Eric Wieser]

Perhaps the thing to do is to write a recOn' with pattern matching

[Eric Wieser]

Actually, this comes down to computability of docs4#Multiset.rec which in turn goes down to List.rec

[Johan Commelin]

All is fixed. Ready for review

[Johan Commelin]

Modulo removing the noncomputable once List.rec is fixed, of course.

[Eric Wieser]

I wonder why csimp doesn't work on List.rec...

[Kyle Miller]

@Eric Wieser I'm not sure, but in case you want to work on making these fintypes computable, here's a computable Multiset.rec:

def rec_aux (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
    (C_cons_heq :
      ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b))) :
    (l : List α) → C (Quotient.mk (isSetoid α) l)
| [] => C_0
| a::l => C_cons a ⟦l⟧ (rec_aux C_0 C_cons C_cons_heq l)

theorem rec_aux_eq :
    rec_aux C_0 C_cons C_cons_heq = @List.rec α (fun l => C ⟦l⟧) C_0 fun a l b => C_cons a ⟦l⟧ b :=
by
  ext l
  induction l with
  | nil => rfl
  | cons a l ih => simp [rec_aux, ih]

/-- Dependent recursor on multisets.
TODO: should be @[recursor 6], but then the definition of `Multiset.pi` fails with a stack
overflow in `whnf`.
-/
protected
def rec (C_0 : C 0) (C_cons : ∀ a m, C m → C (a ::ₘ m))
    (C_cons_heq :
      ∀ a a' m b, HEq (C_cons a (a' ::ₘ m) (C_cons a' m b)) (C_cons a' (a ::ₘ m) (C_cons a m b)))
    (m : Multiset α) : C m :=
  Quotient.hrecOn m (rec_aux C_0 C_cons C_cons_heq) fun l l' h => by
    rw [rec_aux_eq]
    exact h.rec_heq
      (fun hl _ ↦ by congr 1; exact Quot.sound hl)
      (C_cons_heq _ _ ⟦_⟧ _)

[Eric Wieser]

I'd argue it would be easier to just write a computable list.rec and swap that in everywhere; I think all the derived types end up comptuable automatically

[Kyle Miller]

I think using recursors for computation is "wrong" though, since Lean eagerly evaluates arguments. I'm pretty sure it's not that List.rec is noncomputable, but rather that the Lean compiler is by design pushing the user away from using it for computations.

[Eric Wieser]

#eval (List.rec 0 (fun x xs ih => 0) ([] : List Nat) : Nat)

gives (emphasis mine)

code generator does not support recursor 'List.rec' yet, consider using 'match ... with' and/or structural recursion

which suggests this is not by design but by it not being prioritized

[Notification Bot]

2 messages were moved from this topic to #lean4 > csimp on recursors by Eric Wieser.

[Reid Barton]

It's still arguably suboptimal to use List.rec because (as Kyle alluded to) you have to evaluate the empty list case even when the list is not empty

[Reid Barton]

Of course it doesn't matter if you only care about "does Lean complain about noncomputable"

[Eric Wieser]

mathlib4#1720 makes a very large number of things computable by adding those csimp lemmas

[Eric Wieser]

Reid Barton said:

It's still arguably suboptimal to use List.rec because (as Kyle alluded to) you have to evaluate the empty list case even when the list is not empty

I would guess that in almost all cases the empty list case is entirely trivial anyway, so evaluation costs very little

[Reid Barton]

It should also be noted (as usual) that this "computability" is not the same as being able to reduce things

[Eric Wieser]

Presumably both List.rec and Nat.rec already reduce correctly

[Kevin Buzzard]

On the other hand this "computability" will make porting easier, with fewer confusing errors.

[Eric Wieser]

Notably there are some Decidable instances that describe some algorithms on lists. It's pretty silly to say "oh, this algorithm is just as noncomputable as using choice would be".

[Chris Hughes]

https://github.com/leanprover-community/mathlib4/pull/1728

[Chris Hughes]

I made this on a fork because I wasn't planning on PRing it, but maybe I should PR from a branch of leanprover-community for CI

[Chris Hughes]

CI seems to have kicked in now so I'll leave it

[Johan Commelin]

@Chris Hughes Can you also fix Data.Fintype.Vector please?

[Reid Barton]

does Lean 4 still give an error when you mark something noncomputable that's computable?

[Reid Barton]

Eric Wieser said:

Notably there are some Decidable instances that describe some algorithms on lists. It's pretty silly to say "oh, this algorithm is just as noncomputable as using choice would be".

AFAIK we don't ever evaluate Decidable instances (that's not how dec_trivial works)

[Johan Commelin]

This rg noncomputable | rg orting gives

Mathlib/Data/Multiset/Basic.lean:noncomputable -- Porting note: added
Mathlib/Data/Multiset/Basic.lean:noncomputable -- Porting note: added
Mathlib/Data/Multiset/Basic.lean:noncomputable -- Porting note: added
Mathlib/Data/Multiset/Basic.lean:noncomputable -- Porting note: added
Mathlib/Data/Multiset/Sections.lean:-- Porting note: `Sections` depends on `recOn` which is noncomputable.
Mathlib/Data/Multiset/Pi.lean:--Porting note: Added noncomputable
Mathlib/Data/Finset/Pi.lean:--Porting note: marked noncomputable
Mathlib/Data/Fin/Basic.lean:--Porting note: marked noncomputable
Mathlib/Data/Fin/Tuple/Basic.lean:-- Porting note: I made this noncomputable because Lean seemed to think it should be
Mathlib/Data/Vector/Basic.lean:-- porting notes: requires noncomputable
Mathlib/Data/Vector/Basic.lean:-- porting notes: requires noncomputable
Mathlib/Data/Vector/Basic.lean:-- porting notes: requires noncomputable
Mathlib/Data/PNat/Basic.lean:-- Porting note: added `noncomputable` because of
Mathlib/Data/Fintype/Pi.lean:--Porting note: added noncomputable
Mathlib/Data/Fintype/Pi.lean:--Porting note: added noncomputable
Mathlib/Data/Set/Basic.lean:-- Porting note: remove `noncomputable` later
Mathlib/Algebra/Group/Units.lean:-- Porting note: `to_additive` doesn't carry over `noncomputable` so we make an explicit defn
Mathlib/Algebra/FreeMonoid/Basic.lean:-- Porting note: added noncomputable
Mathlib/Order/RelClasses.lean:-- Porting note: WellFounded.fix is noncomputable, at 2022-10-29 lean
Mathlib/Order/RelClasses.lean:-- Porting note: WellFounded.fix is noncomputable, at 2022-10-29 lean
Mathlib/Order/RelClasses.lean:-- Porting note: WellFounded.fix is noncomputable, at 2022-10-29 lean
Mathlib/Control/Fix.lean:-- porting note: added noncomputable, because WellFounded.fix is noncomputable (for now?)
Mathlib/Control/Fix.lean:-- porting note: added noncomputable, because WellFounded.fix is noncomputable (for now?)
Mathlib/Control/Fix.lean:-- porting note: added noncomputable, because WellFounded.fix is noncomputable (for now?)

[Johan Commelin]

I'm on a train, so this was on an ancient master (from 12 hrs ago, or so)

[Eric Wieser]

I think I have most of those removed my PR

[Eric Wieser]

I think it's just the WellFounded.fix things that remain noncomputable

[Eric Wieser]

Reid Barton said:

AFAIK we don't ever evaluate Decidable instances (that's not how dec_trivial works)

Oh, that's a very good point. I guess it's still nice for metaprograms, but the application is admittedly niche.

[Mario Carneiro]

Eric Wieser said:

I think it's just the WellFounded.fix things that remain noncomputable

I recall early in the ad-hoc phase I did something similar to your List.recC for WellFounded.fix - you can just add a csimp lemma and then anything using WellFounded.fix will be computable

[Eric Wieser]

Oh, I wasn't aware it was possible to write one