cases of decidable

Stream: new members

[Richard Copley]

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]

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

[Mario Carneiro]

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

[Richard Copley]

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]

The hypothesis h?

[Richard Copley]

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

[Mario Carneiro]

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]

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

[Richard Copley]

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

[Martin Dvořák]

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]

Is by_cases what you would suggest, then?

[Richard Copley]

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]

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

[Mario Carneiro]

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]

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

[Richard Copley]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Richard Copley]

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]

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

[Mario Carneiro]

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]

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)