Noncomputable definitions in !4#3007

Stream: mathlib4

[Jeremy Tan]

!4#3007 Because FreeAlgebra.lift is noncomputable the instance in this file has to be noncomputable too; because that instance is noncomputable starHom must be too. Should I be worried or not?

[Eric Wieser]

FreeAlgebra.lift shouldn't be non-computable

[Eric Wieser]

So your PR is fine, but something is up with a previous PR

[Jeremy Tan]

!4#2905 to be more precise

[Eric Wieser]

Right, the standard fix is to copy what I did with docs4#Nat.rec_eq_recC

[Eric Wieser]

But that can be a separate PR

[Adam Topaz]

Is this a bug?

[Jeremy Tan]

Adam Topaz said:

Is this a bug?

I'm already having an argument with @Eric Wieser on which lemmas should be restored to make the simp in the last declaration work. !4#3008 restored two simp lemmas; I prodded myself and found that a third lemma should be restored, now Eric claims that the third lemma is indeed no longer needed in L4

[Eric Wieser]

Adam Topaz said:

Is this a bug?

It's a missing feature, lean4#2049

[Adam Topaz]

Ah ok.

[Jeremy Tan]

@Eric Wieser I merged your !4#3008 into my !4#3007 and tried it; by simp [star_algebraMap] still doesn't work

[Eric Wieser]

What goal does it leave behind?

[Jeremy Tan]

r: R
⊢ ↑starRingEquiv.toEquiv (↑(algebraMap R (FreeAlgebra R X)) r) = { unop := ↑(algebraMap R (FreeAlgebra R X)) r }

[Jeremy Tan]

Adding rfl alone closes it, but by rfl itself also works

[Eric Wieser]

Did you restart lean after merging?

[Eric Wieser]

Does rewriting by my lemma work from that point?

[Jeremy Tan]

Yes, I closed VSCode and reopened it, I saw the infoview showing that recompiling was underway

[Jeremy Tan]

(Just restarted the server again, I'm still seeing an unsolved goal)

[Adam Topaz]

BTW, this works:

def liftFun {A : Type _} [Semiring A] [Algebra R A] (f : X → A) :
    Pre R X → A
  | .of t => f t
  | .mul a b => liftFun f a + liftFun f b
  | .add a b => liftFun f a * liftFun f b
  | .of_scalar c => algebraMap _ _ c

[Eric Wieser]

rw [RingEquiv.coe_toEquiv]?

[Adam Topaz]

modulo the error I introduced switching $+$ and $*$.

[Jeremy Tan]

Eric Wieser said:

rw [RingEquiv.coe_toEquiv]?

doesn't work, even with the simp

[Jeremy Tan]

In fact it complains

tactic 'rewrite' failed, did not find instance of the pattern in the target expression

[Eric Wieser]

Do you see why I think it should work?

[Jeremy Tan]

Yes, because you said so

[Eric Wieser]

Take a look at the statement of the lemma and the statement of the goal

[Jeremy Tan]

They don't match at all

[Eric Wieser]

Both have a term of the form FunLike.coe (RingEquiv.toEquiv f)

[Eric Wieser]

You can disable the arrows in printing to make that clearer

[Jeremy Tan]

how to disable arrows?

[Eric Wieser]

set_option pp.coercions false maybe? I'm afraid I don't know, but autocomplete after pp. might

[Eric Wieser]

Or just click on the arrows to find out what they are

[Jeremy Tan]

Well after by simp [star_algebraMap] and with coercions not printed the goal is

FunLike.coe starRingEquiv.toEquiv (FunLike.coe (algebraMap R (FreeAlgebra R X)) r) =
  { unop := FunLike.coe (algebraMap R (FreeAlgebra R X)) r }

[Jeremy Tan]

Yes, there's FunLike.coe (RingEquiv.toEquiv f) on the LHS, but Lean's not getting it

[Eric Wieser]

My guess is that this is lean4#2074

[Eric Wieser]

Does set_option synth.etaExperiment true let the proof go through?

[Eric Wieser]

To be clear, your refl proof is fine in that PR (and an improvement over the old proof); but it would also be worth understanding the failure here

[Jeremy Tan]

No

[Jeremy Tan]

(but I'm getting another weird error in which when I do...)

[Jeremy Tan]

/-- `star` as an `AlgEquiv` -/
set_option synthInstance.etaExperiment true in
noncomputable def starHom : FreeAlgebra R X ≃ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ :=
  { starRingEquiv with commutes' := fun r => by simp [star_algebraMap] }
#align free_algebra.star_hom FreeAlgebra.starHom

[Eric Wieser]

I'll have a look tomorrow

[Jeremy Tan]

(... I get expected 'abbrev', 'add_decl_doc', 'alias', 'axiom', 'binder_predicate', 'builtin_initialize', 'class', 'declare_config_elab', 'declare_simp_like_tactic', 'declare_syntax_cat', 'def', 'elab', 'elab_rules', 'example', 'inductive', 'infix', 'infixl', 'infixr', 'initialize', 'instance', 'irreducible_def', 'lemma', 'macro', 'macro_rules', 'notation', 'notation3', 'opaque', 'postfix', 'prefix', 'register_builtin_option', 'register_label_attr', 'register_option', 'register_simp_attr', 'scoped', 'structure', 'syntax', 'theorem' or 'unif_hint')

[Jeremy Tan]

Putting the set_option one line higher works though

[Eric Wieser]

As in, works completely?

[Jeremy Tan]

no, with the set_option one line higher, the original error still remains, but I don't get an error from the set_option

[Jeremy Tan]

The two different errors are independent

[Jireh Loreaux]

The error you were getting was because of the docstring. Docstring was looking for the def but instead saw set_option

[Xavier Roblot]

Eric Wieser said:

FreeAlgebra.lift shouldn't be non-computable

I am the one that ported FreeAlgebra. Last time I encountered a problem with recOn, the easy fix was to mark the definition as noncomputable, but I can see it is not the best option. Sorry about that.
I'll make a new PR today or tomorrow to remove the noncomputable I added in this file.

[Reid Barton]

There was some PR that automated the creation of compiled recursors, right? What's the status of that?

[Xavier Roblot]

I'll make a new PR today or tomorrow to remove the noncomputable I added in this file.

!4#3011
(Thanks Adam for the correct code!)

[Jeremy Tan]

@Eric Wieser I just merged the now-landed !4#3011 into my PR. Now neither rfl or anything described in this thread works. What do I do?

[Eric Wieser]

I'm having a look now

[Eric Wieser]

It turns out we were missing docs#ring_equiv.to_equiv_eq_coe, which is not a tautology in Lean4 after all (!4#3035)

[Eric Wieser]

I think the problem is that the new definition of lift uses brecOn on recOn

[Eric Wieser]

Eric Wieser said:

Right, the standard fix is to copy what I did with docs4#Nat.rec_eq_recC

So I think we should probably do this after all, instead of @Adam Topaz's suggestion

[Eric Wieser]

I misdiagnosed it; your proof fails because the irreducible attribute (which was previously lost in porting) has been restored

[Jeremy Tan]

OK, what now?

[Eric Wieser]

star_algebraMap should prove it directly

[Eric Wieser]

Or wait for !4#3035 then the original mathlib3 proof will work

[Jeremy Tan]

@Eric Wieser Well I've restored the original proof with the added-back simp theorems and it works now, thank you

[Eric Wieser]

!4#3035 is now passing CI