fails_quickly times out

Stream: new members

[Christopher Hoskin]

I'm stuck on PR #8673, failing the lint:

Run ./scripts/mk_all.sh
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
:0:0: error: deep recursion was detected at 'replace' (potential solution: increase stack space in your system)
Error: Process completed with exit code 1.

I think it's objecting to this instance https://github.com/leanprover-community/mathlib/pull/8673/files#diff-955f5d05cac3345a253a4f9d7d0a9d97914339b75b6a52e9a7501b4bccc7386bR420

However, I can't see what needs to be done to make it go green?

Thanks,

Christopher

[Kevin Buzzard]

Does the linter fail locally? Then you can change the instance to a def and find out if you're right

[Christopher Hoskin]

Yes, it fails locally. If I change it to a def (and delete any subsequent statements depending on the instance) then the linter passes.

[Christopher Hoskin]

But that doesn't help me know what to do about it...

[Eric Wieser]

That instance forms a loop with docs#distrib_lattice.to_lattice

[Eric Wieser]

So therefore cannot safely be an instance, no matter the priority

[Eric Wieser]

(this is not the case in lean 4 I think)

[Christopher Hoskin]

Thanks. So how would I prove something like:

lemma test [covariant_class α α (*) (≤)] (x y z: α) : (y ⊓ z) ⊔ x = (y ⊔ x) ⊓ (z ⊔ x)

without using class inference? I tried

  apply sup_inf_right (lattice_ordered_comm_group_to_distrib_lattice α) x y z

but that doesn't work.

[Christopher Hoskin]

I thought perhaps

instance : has_coe (covariant_class α α (*) (≤)) (distrib_lattice α) := sorry

would help, but it doesn't. Sorry, I seem to be stabbing around in the dark here.

[Eric Wieser]

You should just change it from instance to def

[Christopher Hoskin]

Eric Wieser said:

You should just change it from instance to def

Right, but then I can't see what to do here where I need to make use of the fact that α is (mathematically) a distributive lattice?

[Eric Wieser]

What's in the context (the hypotheses in the goal window) at that point?

[Christopher Hoskin]

Eric Wieser said:

What's in the context (the hypotheses in the goal window) at that point?

lattice_ordered_group.lean:455:12
Tactic state
widget
filter:
no filter
1 goal
α: Type u
_inst_1: lattice α
_inst_2: comm_group α
_inst_3: covariant_class α α has_mul.mul has_le.le
abc: α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) = (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * ((b ⊔ a) ⊓ c / (b ⊓ a ⊓ c))
Messages (1)
lattice_ordered_group.lean:455:2
rewrite tactic failed, did not find instance of the pattern in the target expression
  (?m_3 ⊔ ?m_4) ⊓ (?m_5 ⊔ ?m_4)
state:
α : Type u,
_inst_1 : lattice α,
_inst_2 : comm_group α,
_inst_3 : covariant_class α α has_mul.mul has_le.le,
a b c : α
⊢ (b ⊔ c ⊔ (a ⊔ c)) / ((b ⊔ c) ⊓ (a ⊔ c)) * ((b ⊓ c ⊔ a ⊓ c) / (b ⊓ c ⊓ (a ⊓ c))) =
    (b ⊔ a ⊔ c) / (b ⊓ a ⊔ c) * ((b ⊔ a) ⊓ c / (b ⊓ a ⊓ c))

[Eric Wieser]

I think you should either:

• replace lattice α with distrib_lattice α in that lemma
• add a letI : distrib_lattice α := lattice_ordered_comm_group_to_distrib_lattice _ inside that proof

[Christopher Hoskin]

The PR has gone green with letI. Thank you very much.