by_contradiction does not require noncomputable

Stream: new members

[Tumbleweed]

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]

src#tactic.by_contradiction should answer your question

[Eric Wieser]

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]

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

[Eric Wieser]

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]

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]

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

[Henrik Böving]

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 inProp.