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


Last updated: Dec 20 2023 at 11:08 UTC