# Zulip Chat Archive

## Stream: new members

### Topic: by_contradiction does not require noncomputable

#### Tumbleweed (May 25 2022 at 19:15):

I've noticed in a few of my proofs that use complete_lattice, that I need to add noncomputable to the declaration. When I dug deep I found that it was relying on classical LEM

However, I've used the by_contradiction tactic in a few places where I don't think the goal can be matched against an instance for decidable. Is my assumption wrong that proof by contradiction, in general, requires LEM?

Why am I not required to preface my declaration with noncomputable?

#### Eric Wieser (May 25 2022 at 19:20):

src#tactic.by_contradiction should answer your question

#### Eric Wieser (May 25 2022 at 19:21):

In particular, these two lines:

```
(mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip) <|>
(mk_mapp `classical.by_contradiction [some tgt] >>= eapply >> skip) <|>
```

#### Eric Wieser (May 25 2022 at 19:21):

Which says "try docs#decidable.by_contradiction first, and if that fails try docs#classical.by_contradiction"

#### Eric Wieser (May 25 2022 at 19:22):

Oh, hang on:

I've noticed in a few of my proofs that use complete_lattice, that I need to add noncomputable to the declaration.

Proofs (aka `lemma`

) don't need `noncomputable`

, only definitions (aka `def`

) do

#### Eric Wieser (May 25 2022 at 19:22):

`by_contradiction`

is only ever usable in a proof, so will never cause you to need `noncomputable`

; because nothing is being computed in the first place.

#### Tumbleweed (May 25 2022 at 19:26):

Awesome I think the difference between def/lemma answers things, thanks :)

#### Henrik Böving (May 25 2022 at 19:30):

Note that this is because `lemma`

/`theorem`

is basically a definition that always has a type that lives in `Prop`

and since Lean has proof irrelevance there is never a need to calculate the value of an element of a type in`Prop`

.

Last updated: Dec 20 2023 at 11:08 UTC