## Stream: new members

### Topic: cases of decidable

#### Richard Copley (Feb 07 2023 at 20:20):

Having defined a decidable hypothesis, what's good style for using it in a proof by cases? I'd like the proof to fail if, after edits, it's no longer true that the hypothesis is decidable, which rules out by_cases. Here's my current attempt (see all_good':

import data.nat.basic

constant n : ℕ
def lesser (x : ℕ) : Prop := x < n

noncomputable def decidable_lesser (x : ℕ) : decidable (lesser x) :=
(if h : x < n then decidable.is_true h else decidable.is_false h)

noncomputable instance : decidable_pred lesser := decidable_lesser

def good (x : ℕ) := true
lemma when_lesser {x : ℕ} (h : lesser x) : good x := trivial
lemma unless_lesser {x : ℕ} (h : ¬lesser x) : good x := trivial

theorem all_good' (x : ℕ) [d : decidable (lesser x)] : good x :=
begin
-- Note : must provide a name "k" to avoid the error "failed to revert 'd',
-- it is a frozen local instance"
cases k : d,
exact unless_lesser h,
exact when_lesser h,
end


#### Mario Carneiro (Feb 07 2023 at 20:22):

why do you care that the hypothesis is decidable for the lemma? It is a proof of a proposition

#### Mario Carneiro (Feb 07 2023 at 20:23):

(That's not a rhetorical question. There are reasons to care, and depending on which one is yours the solution is different.)

#### Richard Copley (Feb 07 2023 at 20:26):

It's more that I'm new to Lean and I want to understand what is happening. Also ... there's no proof provided to the lemma theorem all_good', right? So I'm not sure I understand the question.

#### Richard Copley (Feb 07 2023 at 20:27):

The hypothesis h?

#### Richard Copley (Feb 07 2023 at 20:28):

Lemme edit all_good' to be a theorem to avoid confusion [done]

#### Mario Carneiro (Feb 07 2023 at 20:29):

I'm saying that because all_good' is a theorem, there are no observable effects of having proved it using classical logic instead of the decidable instance

#### Mario Carneiro (Feb 07 2023 at 20:30):

(FYI lemma and theorem are synonyms in lean, there is no difference between them other than style)

#### Richard Copley (Feb 07 2023 at 20:31):

(sure! but now we can say "the theorem" and "the lemmas")

#### Martin Dvořák (Feb 07 2023 at 20:34):

Mario Carneiro said:

(FYI lemma and theorem are synonyms in lean, there is no difference between them other than style)

Sometimes I wish we had even more freedom. I'd like to have the following synonyms:
theorem
lemma
observation
corollary

#### Richard Copley (Feb 07 2023 at 20:39):

Is by_cases what you would suggest, then?

#### Richard Copley (Feb 07 2023 at 20:54):

Hmm. The observable effect is that the proposition is now inhabited, which is what I'd want to avoid if (hypothetically) the predicate were genuinely undecidable and (also hypothetically) decidable math is what I'm interested in, for the piece of work in question

#### Mario Carneiro (Feb 07 2023 at 21:03):

what do you mean by "decidable math is what I'm interested in"

#### Mario Carneiro (Feb 07 2023 at 21:03):

there are a lot of ways to gloss "decidable math" and most of them don't directly correspond to having an instance of decidable

#### Richard Copley (Feb 07 2023 at 21:06):

If the objective is to come up with a proof that does not use excluded middle, double-negation elimination and so on.

#### Richard Copley (Feb 07 2023 at 21:08):

The non-hypothetical reason is that I want to understand the fundamentals of the way Lean works, a little at a time.

#### Mario Carneiro (Feb 07 2023 at 21:11):

Probably in that case you shouldn't use tactics at all, use if instead

#### Mario Carneiro (Feb 07 2023 at 21:14):

theorem all_good' (x : ℕ) : good x :=
if h : lesser x then
unless_lesser h
else
when_lesser h


this won't compile unless it is possible to infer decidable (lesser x). However, it is possible to supply such an instance using classical logic if you use it directly (e.g. by using open_locale classical which makes docs#classical.dec a local instance)

#### Richard Copley (Feb 07 2023 at 21:16):

I notice just now that the by_cases tactic is used a little in "init/data/nat/lemmas.lean", so probably not something worth me being too precious about

#### Mario Carneiro (Feb 07 2023 at 21:17):

by_cases does not use classical logic unless it has to, but it won't error if the instance is missing

#### Richard Copley (Feb 07 2023 at 21:19):

BTW, curiously cases (d : decidable) seems to take the cases in the opposite order to by_cases. In my example when_lesser takes (lesser x) and unless_lesser takes ¬(lesser x)

#### Richard Copley (Feb 07 2023 at 21:19):

Thank you so much for taking the time, this has been helpful

#### Mario Carneiro (Feb 07 2023 at 21:19):

usually this is the more useful behavior since it works in both classical and constructive contexts. If you are defining a function to be #eval'd, you will get an error as desired if the classical instance is used, because it will make the definition noncomputable

#### Mario Carneiro (Feb 07 2023 at 21:32):

Buster said:

BTW, curiously cases (d : decidable) seems to take the cases in the opposite order to by_cases. In my example when_lesser takes (lesser x) and unless_lesser takes ¬(lesser x)

That's because cases uses the natural order of the constructors (false then true, because false is 0 and true is 1), while by_cases uses the same order used by if (then-case then else-case)

Last updated: Dec 20 2023 at 11:08 UTC