Zulip Chat Archive

that is, for expressions made up of max, imax and variables, you can determine if for all values of the variables in nat, one is <= the other or not

Mario Carneiro (Mar 30 2018 at 20:45):

The proof uses case splitting on any imax expressions that come up

Kenny Lau (Mar 30 2018 at 20:45):

oh, I should build a decidable version of finsupp

Mario Carneiro (Mar 30 2018 at 20:46):

I think Johannes had a proposal for that on here, where you use a fintype instead of finite

Kenny Lau (Mar 30 2018 at 20:46):

oh wait, I don't work with finite things

Kenny Lau (Mar 30 2018 at 20:46):

lol

Kenny Lau (Mar 30 2018 at 20:53):

@Mario Carneiro no examples from nat and int?

Kenny Lau (Mar 30 2018 at 20:53):

i.e. everything about them that should be decidable have been proven to be decidable?

Mario Carneiro (Mar 30 2018 at 20:55):

yes, there aren't that many interesting predicate to start with

Kenny Lau (Mar 30 2018 at 20:56):

nice

Andrew Ashworth (Mar 30 2018 at 21:27):

@Kenny Lau out of curiousity what's up with your commutative algebra pr on mathlib

Kenny Lau (Mar 30 2018 at 21:27):

I just started reworking it a few minutes ago, what a coincidence

Kevin Buzzard (Mar 30 2018 at 22:47):

Kenny feel free to PR some of the comm alg stuff in stacks project. Did UMP get PR'd? That's a really important tool I see now.

Kenny Lau (Mar 30 2018 at 22:47):

I can't PR anything until mathlib builds

Kevin Buzzard (Mar 30 2018 at 22:47):

Oh I see.

Kevin Buzzard (Mar 30 2018 at 22:47):

Why don't you roll back?

Kenny Lau (Mar 30 2018 at 22:48):

I mean, the PR will have a cross

Kevin Buzzard (Mar 30 2018 at 22:48):

I know it's a bore. Whenever Lean head and mathlib head don't play well together you're suddenly having to look up commits.

Kevin Buzzard (Mar 30 2018 at 22:48):

I just never upgrade unless I have no red cross and also a thumbs up here

Kevin Buzzard (Mar 30 2018 at 22:49):

I think Sebastian is seriously looking at making this kind of thing easier with leanpkg.

Kenny Lau (Mar 30 2018 at 22:49):

I still don't know why the latest build fails

Hans-Dieter Hiep (Feb 12 2019 at 16:06):

Hi, quick question! What tactic would allow me to show decidable equality of records? I need to show:

⊢ decidable ({o := x_o, m := x_m, τ := x_τ} = {o := y_o, m := y_m, τ := y_τ})

where I know decidable(x_o = y_o), ..., decidable(x_τ = y_τ).

Chris Hughes (Feb 12 2019 at 16:06):

@[derive decidable_eq] when you define the structure.

Hans-Dieter Hiep (Feb 12 2019 at 18:57):

Now, I get an unhelpful error message: failed to find a derive handler for .... What does this mean?

Hans-Dieter Hiep (Feb 12 2019 at 18:59):

It is related to the fact that I have defined an inductive type value. Is that somehow a protected name?

Chris Hughes (Feb 12 2019 at 18:59):

Is the inductive type value a field to your structure?

Chris Hughes (Feb 12 2019 at 18:59):

What does the ... say?

Reid Barton (Feb 12 2019 at 19:01):

Would be easier to say looking at the code and actual error message, but I think ... is the class you want to derive, e.g., decidable_eq

Hans-Dieter Hiep (Feb 12 2019 at 19:01):

failed to find a derive handler for 'choice decidable_eq value.decidable_eq'
Here, choice and decidable_eq are built-in, but value.decidable_eq seems to be related to the generated instance for the type value that I defined earlier.

Hans-Dieter Hiep (Feb 12 2019 at 19:02):

@[derive decidable_eq]
inductive value (β : Type) [objects α β] : type α → Type 1
| object {c : class_name α} (o : β)
    (H : c = class_of α o) : value (ref c)
| null (c : class_name α) : value (ref c)
| term {γ : datatype} : γ → value (data α γ)

Now, I change the name value to valu. Then the error changes!

Hans-Dieter Hiep (Feb 12 2019 at 19:03):

Hmmm, never mind. Unable to reproduce that now. It still is: failed to find a derive handler for 'choice decidable_eq valu.decidable_eq'

Chris Hughes (Feb 12 2019 at 19:03):

Is it confused by something you've defined called decidable_eq? I replicated the error.

namespace foo

def decidable_eq : Type := sorry

@[derive decidable_eq] structure foo :=
(bar : ℕ)

end foo

Reid Barton (Feb 12 2019 at 19:04):

maybe a manually-written instance of decidable_eq got a name like that?

Hans-Dieter Hiep (Feb 12 2019 at 19:05):

Sure, but I have never defined any decidable_eq myself. The value.decidable_eq is not defined by me, but derived.

Chris Hughes (Feb 12 2019 at 19:07):

What namespaces do you have open? Maybe the error is something you've imported.

Hans-Dieter Hiep (Feb 12 2019 at 19:08):

If I remove @[derive decidable_eq] from the value definition, the error changes into something more sensible: mk_dec_eq_instance failed, failed to generate instance for Π (a b : Π (p : param_name m), value β (param_type p)), decidable (a = b) So it must be caused by the derived instance of value.

Chris Hughes (Feb 12 2019 at 19:10):

Of course. I'm confused by choice in the error message. Is this classical.choice?

Hans-Dieter Hiep (Feb 12 2019 at 19:10):

@Chris Hughes Indeed, I have opened the namespace value in which the name decidable_eq was defined by the derivation. Thanks, stupid mistake!

Reid Barton (Feb 12 2019 at 19:13):

aha!
Maybe choice X.foo Y.foo is how Lean represents "I haven't figured out whether you're talking about X.foo or Y.foo yet"?

Hans-Dieter Hiep (Feb 12 2019 at 19:14):

I confirm that. You can see that here:

namespace foo

def value.decidable_eq : Type := sorry
open value

@[derive decidable_eq] structure foo :=
(bar : ℕ)

end foo

Reid Barton (Feb 12 2019 at 19:15):

opening previous inductive types when defining new ones is a totally reasonable thing to do, it's annoying that it causes this derive decidable_eq mechanism to break.

Reid Barton (Feb 12 2019 at 19:15):

Well, it's a totally reasonable thing to want to do, at any rate.

Reid Barton (Feb 12 2019 at 19:16):

Seems like value.decidable_eq should have been protected, then I guess this wouldn't have happened.

Hans-Dieter Hiep (Feb 12 2019 at 19:17):

I agree; if you add protected in the foo snippet above, the derive mechanism works as expected.

Reid Barton (Feb 12 2019 at 19:20):

I'm surprised the lack of protected doesn't break other things though. Seems like having open an inductive/structure type with derived decidable_eq would be pretty common. Maybe Lean is able to resolve the ambiguity in most other situations

Mario Carneiro (Feb 12 2019 at 20:32):

yes, choice is how lean represents an overloaded name in pexprs

Reid Barton (Feb 12 2019 at 20:34):

what better way to represent an overloaded name than by an overloaded name

Last updated: Dec 20 2023 at 11:08 UTC