Missing 'noncomputable'

Stream: new members

[Robert Maxton]

Still working on re-implementing the natural numbers for my edification. My near-clone of mathlib's decidable_le complains

missing 'noncomputable' modifier, definition 'peano.nat.decidable_le' is not compiled

[Robert Maxton]

(I realize I'm making a habit of not giving sufficient #mwe's, sorry -_-. In my defense, this time I think it would involve copying a lot of my code over, since the whole point is that all the proofs have to actually be valid to a constructivist? Or can I in fact just fill in some theorems with 'sorry's and put that in?)

[Robert Maxton]

... actually, judging from the other error messages, should this be a problem local to the proof/algorithm?

[Robert Maxton]

since it doesn't say "depends on <some other proof>"

[Yaël Dillies]

This is very hard to debug. It might just be that you haven't finished writing your definition.

[Robert Maxton]

that's... unfortunate. Um. Here's the local bit: if this doesn't look obviously wrong, I guess I'll just give up for now and come back after I finish more of the file?

[Robert Maxton]

  lemma decidable_le : ∀ a b: nat, decidable (a ≤ b)
  | nat.zero      b  := is_true zero_le
  | (S a)  nat.zero  := is_false (@succ_not_le_zero a)
  | (S a)  (S b)     :=
    match decidable_le a b with
    | is_true h := is_true (succ_le_succ.mp h)
    | is_false h := is_false (by rwa succ_le_succ at h)
    end

[Robert Maxton]

thanks anyway

[Yaël Dillies]

Doesn't look obviously wrong :shrug:

[Robert Maxton]

mk~

[Robert Maxton]

I'll come back and bug people later I guess lol

[Robert Maxton]

and see if I can somehow pull an MWE out of this

[Kevin Buzzard]

Yes you can sorry other proofs and definitions in a mwe

[Robert Maxton]

Well sure, but that's not the question; the question is, if the bug is specifically "I'm getting noncomputable/cannot be compiled bugs, is it still legitimate to leave sorry's lying around?"

[Mario Carneiro]

lemmas don't have code generation, so they often cause this kind of problem. Don't use lemma for data

[Robert Maxton]

... oh.

[Robert Maxton]

well.

[Robert Maxton]

that's good to know.

[Robert Maxton]

also bizarre, but okay

[Mario Carneiro]

I believe the suggestion to use noncomputable lemma is due to @Kyle Miller 's recent change

[Robert Maxton]

that fixed it. thanks!

[Mario Carneiro]

but def should just work here

[Robert Maxton]

that fixed it. thanks!

[Robert Maxton]

that fixed it. thanks!

[Henrik Böving]

Robert Maxton said:

also bizarre, but okay

It's not really bizarre no, lemmas are proofs and proofs are irrelevant so they can just be ignored for code generation. Furthermore lemmas are usually declared using tactics and the stuff that tactics spits out is not meant to be turned into executable code if you wanted it to, the job of tactics is to generate a term of the desired type,not to do that in a pretty or efficient way.

[Mario Carneiro]

tactics usually try to be efficient, although they sometimes do no-op steps on purpose

[Henrik Böving]

Eh bad wording, I meant their job is not to generate a term of the type that can be computed in an efficient way

[Kyle Miller]

Robert Maxton said:

Well sure, but that's not the question; the question is, if the bug is specifically "I'm getting noncomputable/cannot be compiled bugs, is it still legitimate to leave sorry's lying around?"

Pretty much anything that reproduces the behavior you're observing is legitimate for a mwe.

[Kyle Miller]

Robert Maxton said:

also bizarre, but okay

The error message could admittedly be better by giving a reason:

missing 'noncomputable' modifier, definition 'peano.nat.decidable_le' is not compiled since it is a theorem