# Zulip Chat Archive

## 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