Zulip Chat Archive

Stream: new members

Topic: Inf troubles

Pim Otte (Aug 07 2022 at 10:33):

Couple of questions about the sample below:

Why doesn't apply work as-is? I get "failed to unify", but the shape seems perfectly fine.
For the @-variant: It fails to synthesize the complete_semilattice_Inf ℕ, as I understand it, N should be one, but I'm not sure how to get that, or how to find it. Any pointers?:)

import data.mv_polynomial.basic

noncomputable theory
open_locale big_operators

example : (Inf ({n :  | n  5} : set ))  5 :=
    apply Inf_le,
    -- apply @Inf_le ℕ _ ({n : ℕ | n ≥ 5} : set ℕ) 5,

Eric Rodriguez (Aug 07 2022 at 10:39):

docs#cInf_le is what you need to use for nat

Eric Rodriguez (Aug 07 2022 at 10:39):

nat does not form a docs#complete_semilattice_inf (equivalent to a docs#complete_lattice, which requires a top element)

Eric Rodriguez (Aug 07 2022 at 10:40):

"c" stands for conditional, and this is because Inf {} = 0, not a hypothetical "top" element as should be required

Pim Otte (Aug 07 2022 at 10:43):

I see, thanks a lot!

Anatole Dedecker (Aug 07 2022 at 16:46):

Maybe this is solved in Lean4, but would there be a way to tell when the failure of unification is cause by lack of instances and fall back to the « failed to synthesize type class instance » error message ? Although I guess it would be pretty hard because in this case the error comes before searching for a complete lattice instance, it fails because the theorem is about inf coming from complete lattice and you want to apply it to the one coming from conditionally complete lattice, right ?

Last updated: Dec 20 2023 at 11:08 UTC