fails to reduce?

Stream: lean4

[Joseph O]

I have this function

@[reducible] def mapNth : (n : Fin' αs.length) → (f : (αs.get' n) → β) → HList αs → HList (αs.replaceAt n β)
  | ⟨0, _⟩, f, a::as => (f a)::as
  | ⟨n+1, h⟩, f, a::as => a::(as.mapNth ⟨n, Nat.lt_of_succ_lt_succ h⟩ f)

and i tried doing this:

def foo : HList [Int, String, Nat] := [-4, "cool", 28]

#eval foo.mapNth 0 (·*-1)

but i get the error

expression
  mapNth 0 (fun a => a * -1) foo
has type
  HList (List.replaceAt [Int, String, ℕ] 0 (List.get' [Int, String, ℕ] 0))
but instance
  Lean.MetaEval (HList (List.replaceAt [Int, String, ℕ] 0 (List.get' [Int, String, ℕ] 0)))
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

What i dont understand is that mapNth is marked @[reducible], so it should work. This was a solution, but I dont really like it:

def the (α : Type u) (a : α) := a

#eval the (HList [Int, String, Nat]) (foo.mapNth 0 (·*-1))

i could just make a wrapper function to utilize this, but is there a reason its not working?

[Joseph O]

Also, im using version leanprover/lean4:nightly-2022-03-13

[Mario Carneiro]

You need an implementation of MetaEval, which usually means that you need a way to print the resulting object

[Mario Carneiro]

this is not a #mwe so it's hard to say more

[Joseph O]

Mario Carneiro said:

You need an implementation of MetaEval, which usually means that you need a way to print the resulting object

i already have a repr instance, why do i need metaeval?

[Joseph O]

instance [Repr α] (αs : List Type) [HListRepr (HList αs)] : HListRepr (HList (α :: αs)) where
  repr
  | HList.cons x xs =>
    match xs with
    | HList.nil => reprPrec x 0
    | HList.cons x' xs' => reprPrec x 0 ++ ", " ++ HListRepr.repr xs

[Leonardo de Moura]

What i dont understand is that mapNth is marked @[reducible], so it should work. This was a solution, but I dont really like it:

Note that the type is HList (List.replaceAt [Int, String, ℕ] 0 (List.get' [Int, String, ℕ] 0)). So, marking mapNth as reducible will not help.
As I mentioned before, typeclass resolution only unfolds definitions marked as reducible. It also uses an index for retrieving relevant instances, and this index unfolds only reducible definitions during retrieval. It is not feasible to change that because everything would become much more expensive.

[Leonardo de Moura]

Since #eval is only used for testing, I pushed another modification that should improve the behavior of the system in this kind of example. Given #eval t, Lean infers the type A of the term t. If it fails to find the instance, it normalizes A and tries again.
This change should be available in tomorrow's nightly build.

[Leonardo de Moura]

In your example, it will first fail to find an instance for HList (List.replaceAt [Int, String, ℕ] 0 (List.get' [Int, String, ℕ] 0)). Then, it will normalize and obtain HList [Int, String, ℕ], and when it tries to synthesize again, it will find the solution.

[Joseph O]

Leonardo de Moura said:

Since #eval is only used for testing, I pushed another modification that should improve the behavior of the system in this kind of example. Given #eval t, Lean infers the type A of the term t. If it fails to find the instance, it normalizes A and tries again.
This change should be available in tomorrow's nightly build.

Only problem is newer releases break mathlib

[Arthur Paulino]

@Edward Ayers has this PR open to update to nightly 03-20. What if we fast-forward it to 03-21 instead?

[Arthur Paulino]

@Joseph O in the meantime, if you want to keep moving forward in your studies, you can make a fork of Mathlib4 and update the toolchain in a branch of yours. Then add your fork of Mathlib4 (using your branch) as a dependency

[Edward Ayers]

Hi yes please edit away (I am editing now)

[Edward Ayers]

Sorry I didn't quite understand the protocol for the nightly fixes to mathlib4

[Edward Ayers]

I guess the preference with those is to merge asap

[Joseph O]

how can i tell my mathlib4 dependency to update?

[Arthur Paulino]

I'm not sure lake supports something like this yet but you can try closing VS Code, deleting the lean_packages directory and opening VS Code again

[Sebastian Ullrich]

Updating the hash in lakefile.lean and invoking Refresh File Dependencies in VS Code should be sufficient

[Joseph O]

What do you mean by updating the hash

[Arthur Paulino]

In your lakefile.lean you have this:

src := Source.git "https://github.com/leanprover-community/mathlib4.git" <REV>

The hash Sebastian is talking about is what you put in <REV>. You can add a specific commit hash there

[Arthur Paulino]

nightly 03-21 is breaking Mathlib4 in many places though. So it won't be too trivial to make the update

[Joseph O]

Arthur Paulino said:

In your lakefile.lean you have this:

src := Source.git "https://github.com/leanprover-community/mathlib4.git" <REV>

The hash Sebastian is talking about is what you put in <REV>. You can add a specific commit hash there

like this?

dependencies := #[
    {
      name := `mathlib,
      src := Source.git "https://github.com/leanprover-community/mathlib4.git" "260cceb2bd29e5f2f67bd55335d3cb8a5397416f"
    }

[Arthur Paulino]

Yeah, but that's the commit hash of Mathlib4 master branch (as of now), which is not updated with nightly 03-21 yet

[Joseph O]

Oh. Are you sure? image.png

[Arthur Paulino]

Yes. That bump was to nightly 03-20. I'm working on a new bump right now

[Arthur Paulino]

mathlib4#244

[Arthur Paulino]

Many changes were made because we don't have instance : OfNat String.Pos n := ⟨⟨n⟩⟩ in core though. @Leonardo de Moura may I PR it?

[Mauricio Collares]

Judging by https://github.com/leanprover/lake/pull/60, that might have been intentional

[Sebastian Ullrich]

Yes, let's not immediately break down the abstraction we just erected. At least not without thorough motivation.

[Gabriel Ebner]

Also many of the ⟨...⟩ fixes (incl. the proposed OfNat instance) are incorrect and will produce interesting results. Quiz: what does the following evaluate to?

#eval "ℝeal".get ⟨1⟩
#eval "ℝeal".extract 0 ⟨1⟩

[Arthur Paulino]

Indeed, I'm going to undo my careless proposed changes regarding String.Pos on mathlib4#244