Proof by contradiction

Stream: new members

[Trevor Fancher]

Sometimes the by_contradiction tactic doesn't work that way I would expect. For example,

theorem cofinite_not_principal : ∀ S : set ℕ, cofinite ℕ ≠ 𝓟 S :=
begin
  intro S,
  by_contradiction,
end

fails with the message

tactic by_contradiction failed, target is not a proposition

(even if I remove the intro S line). One way I've come up with to deal with these situations is to do the following

theorem cofinite_not_principal : ∀ S : set ℕ, cofinite ℕ ≠ 𝓟 S :=
begin
  intro S,
  have t : true := trivial,
  contrapose! t,
  rw not_true,
  -- Now I'm in the state that I would expect by_contradiction to put me in after the "intro S" line.
end

I'm still new to the game of formalizing proofs, but it seems by_contradiction should do this for me.

Am I just missing some another technique/tactic/way of using by_contradiction?

p.s. I would also expect contrapose! to turn ¬true to false.

p.p.s. To get a MWE just add the following above the theorem

MWE header

import order.filter.basic
open_locale filter
open filter set

def cofinite (α : Type) : filter α :=
{ sets := { S : set α | (Sᶜ).finite },
univ_sets := begin
rw [mem_set_of_eq, compl_univ],
exact finite_empty,
end,
sets_of_superset := begin
intros X Y hX hXY,
-- rw mem_set_of_eq at hX ⊢,
apply finite.subset hX,
rwa compl_subset_compl,
end,
inter_sets := begin
intros X Y hX hY,
rw [mem_set_of_eq, compl_inter],
apply finite.union hX hY,
end }

[Riccardo Brasca]

If your goal is a ≠ b you should start with intro h, and the goal will be false.

[Riccardo Brasca]

With h : a = b. There is no need of using a proof by contradiction here, since a ≠ b is defined as a = b → false .

[Riccardo Brasca]

(We all made this mistake I think, so you are in a good position :grinning_face_with_smiling_eyes: )

[Ruben Van de Velde]

intro h works, but why doesn't by_contra? Even more oddly, rw ne.def, by_contra h, works

[Trevor Fancher]

Ok. Thanks for enlightening me. I would never think to call intro when proving a ≠ b. Well, except now that I've been enlightened :)

[Riccardo Brasca]

It's a decidablity issue, adding open_locale classical should also work.

[Trevor Fancher]

I can confirm that

open_locale classical
theorem cofinite_not_principal : ∀ S : set ℕ, cofinite ℕ ≠ 𝓟 S :=
begin
  intro S,
  by_contradiction,
end

does exactly what I expect. Is there a downside to that open_locale classical line?

[Riccardo Brasca]

If you want to do "standard" mathematics no. But if you are interested in constructive logic and/or computability then yes, but I will let someone else more experienced than me clarify this.

[Trevor Fancher]

Fair enough. Thanks :)

[Riccardo Brasca]

And beware that if at some point you want to PR this in mathlib the constructivist mafia will force you to use intro h here.

[Riccardo Brasca]

BTW, the issue here is probably very simple: without excluded middle you cannor prove ¬¬p → p, so ¬(a ≠ b) does not imply a = b.

[Trevor Fancher]

I'm fine with doing intro h and I would guess most people would be (other than for disoverability). I have no idea if it's possible or a good idea for by_contradiction to detect this situation and then just do intro h, but it seems reasonable. Because the state after intro S, intro h in the above theorem is exactly what I, in my limited understanding, would mean when I say "lets now prove this by contradiction".

[Riccardo Brasca]

I think that a good lesson to learn here is to realize that you never asked yourself what ¬h actually means. Of course we are very happy with the standard vague idea, and we can do a lot of beautiful math with it, but in Lean even very basic things must be defined (we even have a definition of =). ¬h is defined as h → false, so if the goal is an implication it is natural to start with intro.

[Trevor Fancher]

I agree. It is nice to know how ¬h is defined now. by_contradiction not handling this is overall a relatively minor pain point. But, from my couple weeks with lean now, it does seem like there are a lot of these minor pain points that seem like they would be easy to fix.

[Trevor Fancher]

Of course, seeming easy to fix is quite different than actually being easy :)

[Riccardo Brasca]

This is a feature, not a problem. It's a feature you are not interested if you want to do mathematics, and it becomes annoying in that case, but it is needed to do other things. If you want to forget about all of this, just start all files with

open_locale classical
noncomputable theory

and you are doing classical mathematics.

[Trevor Fancher]

Would a decent compromise being for by_contradiction to detect this situation and, rather than fail with a mysterious message (it was mysterious to me), to print out a few of the suggestions you just made? That would have saved me and probably other people some time.

[Riccardo Brasca]

My suggestion is already in the documentation.

[Eric Wieser]

Trevor, what version of lean are you using?

[Trevor Fancher]

I maintain that the error message "target is not a proposition" is not as actionable as it could be. But your point that I should read the documentation is well taken.

[Ruben Van de Velde]

This is the thing that doesn't make sense to me:

theorem cofinite_not_principal : ∀ S : set ℕ, cofinite ℕ ≠ 𝓟 S :=
begin
  intro S,
  by_contra h, -- fails
  sorry,
end

theorem cofinite_not_principal' : ∀ S : set ℕ, ¬(cofinite ℕ = 𝓟 S) :=
begin
  intro S,
  by_contra h, -- works
  sorry,
end

[Trevor Fancher]

@Eric Wieser leanprover-community/lean:3.24.0. I'm working the Formalising Mathematics exercises and thats the version leanproject pulled.

[Kyle Miller]

I'd thought by_contra automatically used classical decidability instances since by_cases now does, but it seems like it doesn't.

Also, I found a way to get by_contra to infinite loop somehow:

example (α : Type*) (x y : α) : x ≠ y :=
begin
  by_contra,
  -- never gets here
end

[Eric Wieser]

src#tactic.by_contradiction: it does

[Kyle Miller]

(By the way, the tactic#classical tactic is a way to do open_locale classical from within a tactic proof.)

[Eric Wieser]

This is clearly just a bug: by_contradiction is already programmed to do intro when presented with a not, it just doesn't know how to do it for an ne

[Kyle Miller]

@Eric Wieser It seems that I'm accidentally using an old version of Lean when I was poking through the source -- by_contra has been able to use classical decidable instances for 11 months now. https://github.com/leanprover-community/lean/commit/af2f0be9958b0bc390698ffad434c2305ab40e0f

[Eric Wieser]

So there are two bugs here:

• by_contra is somehow not finding the classical instance needed to introduce h : ¬(x ≠ y)
• the heuristic intended to just do intro on goals of the form ¬P (giving the more useful h : x = y) does not look through semireducible defs

[Trevor Fancher]

It certainly felt like a bug. I'm glad it's been surfaced and now I'll let the experts handle it :)

[Riccardo Brasca]

Wow, wonderful!

[Riccardo Brasca]

I mean, wonderful that we realize we have a problem.

[Eric Wieser]

The first bullet is easy to fix with:

meta def by_contradiction2 (H : name) : tactic expr :=
do tgt ← target,
  (match_not tgt $> ()) <|>
  (mk_mapp `decidable.by_contradiction [some tgt, none] >>= eapply >> skip) <|>
  (mk_mapp `classical.by_contradiction [some tgt] >>= eapply >> skip) <|>
  fail "tactic by_contradiction failed, target is not a proposition",
  intro H

[Ruben Van de Velde]

"target is not a proposition" is still a weird error message, at least in this case

[Eric Wieser]

https://github.com/leanprover-community/lean/pull/622

[Yaël Dillies]

About not true being replaced by false, true is a type with one element, trivial, and false is a type with no element. So you can prove not true iff false by doing \la h, h trivial one way and \la h, h.elim rhe other way. But you see that this is much less natural than you would have expected, which indicates that this is not really the way we do maths in Lean.

[Kyle Miller]

I've never really understood why ne is behind a definition:

@[reducible] def ne {α : Sort u} (a b : α) := ¬(a = b)
infix ` ≠ `:50 := ne

Couldn't it have been this, saving some of these headaches?

notation a ` ≠ `:50 b := ¬ a = b

[Eric Wieser]

Then docs#ne.symm wouldn't work with dot notation

[Eric Wieser]

I'd argue the headache is that the tactic forgot to look through reducible definitions

[Kyle Miller]

Seems fine to me, so long as you're ok with it being in the not namespace:

local notation a ` ≠ `:50 b := ¬ a = b

def not.symm {α : Type*} {x y : α} (h : x ≠ y) : y ≠ x :=
λ h', h h'.symm

example (α : Type*) (x y : α) (h : y ≠ x) : x ≠ y :=
begin
  exact h.symm,
end

[Kyle Miller]

I've run into ne not being literally not-equals a number of times. There's always a simple workaround, but it's a bit of annoying friction.

[Kyle Miller]

This reminds me that there's no docs#not.def. The difference between not and implies-false is another small annoyance (¬p → false seems like it should simp to p)

[Eric Wieser]

Why would there need to be a not.def?

[Eric Wieser]

Instead of rw not.def you can use rw not

[Kyle Miller]

It's to rewrite it backwards

[Kyle Miller]

It would let you normalize all the implies-falses in an expression into nots, which have a lot more simp lemmas about them.

[Eric Wieser]

Hmm, there's something weird there.. I'll make a new thread

[Kyle Miller]

lemma not.def (p : Prop) : ¬p ↔ (p → false) := iff.rfl

example (p : Prop) (h : p) : ¬p → false :=
begin
  simp [←not.def],
  exact h
end

[Eric Wieser]

My point was that not should have an equation lemma so that you can just do simp [←not]. It is missing.

[Kyle Miller]

Does simp actually work that way though for definitions?

namespace foo

def not (p : Prop) := p → false
local prefix `¬`:40 := not

example (p : Prop) (h : p) : ¬p → false :=
begin
  simp [←not],
  -- p : Prop,
  -- h : p
  -- ⊢ (p → false) → false
end

end foo

(rw [←not] does the expected thing, however.)

[Eric Wieser]

Ah, perhaps I was thinking of rw

[Eric Wieser]

That looks like a bug to me, simp has clearly done the opposite of what we asked it to

[Eric Wieser]

Filed as https://github.com/leanprover-community/lean/issues/623, I'm not familiar enough with the simplifier to debug that one

[Arthur Paulino]

I have hf: fintype.card α' = 0 and hn: nonempty α'. How do I use those to prove false?

(library_search couldn't help me)

[Eric Rodriguez]

docs#fintype.card_pos_iff :)

[Arthur Paulino]

Thanks!!

[Johan Commelin]

docs#fintype.card_ne_zero

[Johan Commelin]

@Arthur Paulino Was that hn : nonempty α already there at the beginning of the proof?

[Johan Commelin]

I'm asking, because if you created it later, you need to reset the instance cache using the resetI, tactic.
Maybe resetI, library_search would have been able to find the fintype.card_ne_zero lemma.

[Arthur Paulino]

Nope, I had to "fabricate" it. Dunno the exact term. Create? Insert?

[Arthur Paulino]

Ah, state then prove

[Yaël Dillies]

Synthesize!

[Arthur Paulino]

I did use tactic.unfreeze_local_instances,