proof_by_contra

Stream: general

[Johan Commelin]

I would very much like to have the following tactic in mathlib. But presumably this should be merged into by_contra, which is locked in core. And the behaviour of this tactic depends on push_neg, which is only available in mathlib. What is the best way forward?

namespace tactic
namespace interactive

/-- Turns a goal `P` into `¬¬P`, and uses `push_neg` to simplify the inner `¬P`. -/
meta def proof_by_contra : tactic unit :=
`[ by_contra proof_by_contra_hyp,
   try { push_neg at proof_by_contra_hyp },
   revert proof_by_contra_hyp,
   show ¬ _ ]

example (P : Prop) : P :=
begin
  proof_by_contra, -- `¬¬P`
  sorry
end

end interactive
end tactic

[Gabriel Ebner]

But presumably this should be merged into by_contra

It does something different than by_contra, so I don't think they should be merged.

[Johan Commelin]

@Gabriel Ebner I think this would be reasonable behaviour for by_contra if it doesn't get a new id for the hypothesis.

[Johan Commelin]

Or maybe by_contra!.

[Gabriel Ebner]

The push_neg is pretty mathlib-specific though.

[Eric Wieser]

Note that your tactic is a no-op for:

example (P : Prop) : ¬P :=
begin
  proof_by_contra,
  sorry
end

which is probably not what you want

[Johan Commelin]

I think it is what I want.

[Eric Wieser]

Aren't no-op tactics frowned upon?

[Eric Wieser]

eg simp fails by default if it does nothing

[Johan Commelin]

You mean that it should fail instead?

[Eric Wieser]

Yes

[Johan Commelin]

Aha... I don't know how to do that.

[Johan Commelin]

I'm a cargo-tactic-writer

[Eric Wieser]

Probably you shouldn't inherit the intro behavior from by_contra

[Johan Commelin]

I just want support for writing

  have : p > n,
  { proof_by_contra,
    assume : p ≤ n,

[Johan Commelin]

I don't care too much about what proof_by_contra is called, as long as it is more readable than apply lt_of_not_ge.

[Johan Commelin]

Every random stranger understands what proof_by_contra does. But lt_of_not_ge is hieroglyphic.

[Kevin Buzzard]

Just to comment that I'm extensively using by_contra as it stands in a lecture I'm about to give and also in my undergraduate teaching this term. It's a great way of introducing classical logic to mathematicians without going on about constructivism

[Johan Commelin]

by_contra is nice, except for the lack of automatic tidying up using push_neg.

[Kevin Buzzard]

You don't always want to use push_neg next though

[Johan Commelin]

Why not?

[Johan Commelin]

A proof that doesn't name any Prop-assumptions or library lemmas:

theorem euclid (n : ℕ) : ∃ p > n, p.prime :=
begin
  let N := n! + 1,
  let p := nat.min_fac N,
  have : n! > 0    := by library_search,
  have : N > 1     := by library_search,
  have : N ≠ 1     := by library_search,
  have : p.prime   := by library_search,
  have : p > n,
  { proof_by_contra,
    assume : p ≤ n,
    have : p > 0   := by library_search,
    have : p ∣ n!  := by library_search,
    have : p ∣ N   := by library_search,
    have : p ∣ 1   := by library_search,
    have : ¬p ∣ 1  := by library_search,
    contradiction },
  finish,
end

[Johan Commelin]

It's a bit long-winded. But this proof is readable by someone who has never read Lean before. I like that it doesn't contain any library lemmas.

[Kevin Buzzard]

That's pretty nice!

[Yaël Dillies]

Impressive!

[Kevin Buzzard]

Can I use it in my talk?

[Yaël Dillies]

But doesn't it set your CPU on fire?

[Johan Commelin]

Unfortunately you can't use

by library_search using [‹p ∣ n!›]

[Eric Wieser]

What imports does that example need?

[Eric Wieser]

The problem with library_search is that it only works with the right imports, and without them you have no idea what you need to import!

[Johan Commelin]

Preamble:

import data.nat.prime
import tactic

namespace tactic
namespace interactive

/-- Turns a goal `P` into `¬¬P`, and uses `push_neg` to simplify the inner `¬P`. -/
meta def proof_by_contra : tactic unit :=
`[ by_contra proof_by_contra_hyp,
   try { push_neg at proof_by_contra_hyp },
   revert proof_by_contra_hyp,
   show ¬ _ ]

example (P : Prop) : P :=
begin
  proof_by_contra, -- `¬¬P`
  sorry
end

end interactive
end tactic

open_locale nat -- enable `!` as notation for factorial

[Mario Carneiro]

Johan Commelin said:

I just want support for writing

  have : p > n,
  { proof_by_contra,
    assume : p ≤ n,

I don't like that the proposed version of the tactic introduces a negation for no reason. If this is the kind of proof you want to do, why not make it proof_by_contra h? : p ≤ n, i.e. the same style as by_contra?

[Johan Commelin]

Mario, this is all due to the fact that I don't know how to properly write tactics.

[Johan Commelin]

So, if I can write

proof_by_contra,
assume : p ≤ n,

with a different implementation under the hood, then I certainly wont complain.

[Johan Commelin]

proof_by_contra : p ≤ n reads slightly weird. It's missing the assume verb.

[Mario Carneiro]

well then change the name of the tactic

[Mario Carneiro]

e.g. assume_by_contra

[Eric Wieser]

The existing by_contra has no assume in the name, though

[Mario Carneiro]

I think that it can also be merged into by_contra in this form; the only addition here is that we are explicitly type ascribing the hypothesis

[Mario Carneiro]

and we use some simpa call involving push neg stuff to make the type match

[Eric Wieser]

Am I right in thinking the main advantages of @Johan Commelin's spelling:

proof_by_contra,
assume : p ≤ n,

over

by_contra
push_neg at h

is that the former doesn't name the hypothesis and does show the type?

[Johan Commelin]

It also doesn't name push_neg. Which is an operation that should be performed "behind the scenes" whenever possible.

[Mario Carneiro]

they both name the hypothesis

[Mario Carneiro]

the first one names it this

[Johan Commelin]

Eric means that the proof script doesn't name (i.e., mention explicitly) it.

[Mario Carneiro]

Doesn't by_contra have a ! version that calls push_neg?

[Johan Commelin]

by_contra is in core, right?

[Eric Wieser]

I'd certainly be in favor of changing by_contra to accept an optional type annotation

[Eric Wieser]

Yes, it is; I changed it very recently

[Eric Wieser]

tactic#by_contra to give you the breadcrumb to find it

[Mario Carneiro]

I could have sworn we had some souped up version of by_contra in mathlib

[Eric Wieser]

https://github.com/leanprover-community/lean/blob/a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82/library/init/meta/interactive.lean#L1624-L1638 is the parser

[Eric Wieser]

https://github.com/leanprover-community/lean/blob/a0fb1e8c7ac81dfd2e80ad0de08f4e57ee853d82/library/init/meta/tactic.lean#L1481-L1487 is the tactic itself

[Mario Carneiro]

ah, there is tactic#contrapose

[Johan Commelin]

I would be in favour of having assume_by_contra which also calls push_neg on the new hyp.

[Mario Carneiro]

I think it would make sense to have a push_neg powered by_contra

[Mario Carneiro]

would it be too tricky to remove by_contra and just have by_contradiction in core?

[Johan Commelin]

It might break projects that don't use mathlib?

[Mario Carneiro]

fair

[Eric Wieser]

I'm guessing it's not possible to have by_contra in core and by_contra! in mathlib?

[Johan Commelin]

Otoh, such project might not be using a recent Lean anyways.

[Mario Carneiro]

there is always the old standby of by_contra'

[Johan Commelin]

We never got complaints when we ripped algebra out of core.

[Eric Wieser]

Can we use replacement hooks like obviously does, and have the default for by_contra! to just print "sorry, needs mathlib"

[Johan Commelin]

Mario Carneiro said:

there is always the old standby of by_contra'

which is ugly. My goal is to have a way to write really slick proofs.

[Ruben Van de Velde]

by_con?

[Johan Commelin]

I don't think people will immediately understand that either.

[Johan Commelin]

The point is, when you write a proof that will be printed, there cannot be any mouse-over hover-texts, and there will be no goal state or infoview.

[Mario Carneiro]

I think for demo purposes you can set up your own veneer over mathlib tactics, so they aren't intrinsically related

[Johan Commelin]

That's fair. And that's what I'm doing now.

[Mario Carneiro]

like Patrick's "french mode"

[Johan Commelin]

Still, I would like to stay very close to mathlib.

[Johan Commelin]

Ideally, someone should be able to go to the online editor, and type in my proof.

[Eric Wieser]

Johan Commelin said:

Ideally, someone should be able to go to the online editor, and type in my proof.

I had complaints from a reviewer that attempts to copy my proof from a PDF version didn't work... So sharing a URL with .lean files might be more reasonable.

[Johan Commelin]

That's a good idea.

[Johan Commelin]

Especially since ∣ ≠ | which will certainly trip up hand-copying of proofs.

[Johan Commelin]

In that case, can someone tell me how to write a observe : some_prop tactic that does

have : some_prop := by library_search

[Johan Commelin]

I can then put proof_by_contra and observe in a prereq file that I import.

[Mario Carneiro]

import tactic.push_neg
import tactic.suggest
import data.nat.prime

namespace tactic
namespace interactive
setup_tactic_parser

meta def assume_by_contra (h : parse ident?) (t : parse (tk ":" *> texpr)?) : tactic unit := do
  let h := h.get_or_else `this,
  applyc ``classical.by_contradiction,
  h₁ ← tactic.intro h,
  t' ← infer_type h₁,
  (e, pr) ← push_neg.normalize_negations t' <|> refl_conv t',
  match t with
  | none := () <$ replace_hyp h₁ e pr
  | some t := do
    t ← to_expr ``(%%t : Prop),
    unify t e,
    () <$ replace_hyp h₁ t pr
  end

meta def observe (h : parse ident?) (t : parse (tk ":" *> texpr)) : tactic unit := do
  let h := h.get_or_else `this,
  t ← to_expr ``(%%t : Prop),
  assert h t,
  -- `[{library_search}]
  solve1 $ do
    (lemma_thunks, ctx_thunk) ← solve_by_elim.mk_assumption_set ff [] [],
    (() <$ tactic.library_search
      { backtrack_all_goals := tt,
        lemma_thunks := some lemma_thunks,
        ctx_thunk := ctx_thunk,
        md := tactic.transparency.reducible }) <|> fail "observe failed"

example (a b : ℕ) : a < b :=
begin
  assume_by_contra : b ≤ a,
  observe h : a ≤ a,
end

[Mario Carneiro]

it was harder than it should have been because the porcelain tactics forgot to expose the plumbing version, so I had to copy and paste bits of the implementation of push_neg and library_search respectively

[Johan Commelin]

I had done

meta def observe (h : parse ident?) (q₁ : parse (tk ":" *> texpr)?) : tactic unit :=
«have» h q₁ none >>
tactic.focus1 (tactic.library_search { backtrack_all_goals := tt } >>= (λ _, skip))

[Mario Carneiro]

library_search should really have an option to turn off the trace in opt

[Mario Carneiro]

You probably don't want the type arg of observe to be optional

[Johan Commelin]

I guess so :smiley:

[Mario Carneiro]

I'm not really sure what the mk_assumption_set is doing, but library_search was doing that so I copied it

[Mario Carneiro]

ah, you do want that stuff, it adds some default lemmas like rfl, trivial, congr_arg to the simp set

[Johan Commelin]

Thanks for your help, Mario!

[Patrick Massot]

I'm a bit late to the party but I obviously support the idea of having a version of by_contra that uses push_neg (I wrote both push_neg and contrapose). I think we already had this conversation before and the fact that by_contra is in core is the only obstruction (we can't simply add the exclamation mark version in mathlib)

[Patrick Massot]

I very frequently wish I could have this improved by_contra even outside of propaganda talks

[Mario Carneiro]

I think that we should just do by_contra'. We already have several tactics like that, they are basically TODOs for lean 4

[Gabriel Ebner]

(we can't simply add the exclamation mark version in mathlib)

To be pedantic, you can:

reserve notation `by_contra!`

meta def tactic.interactive.«by_contra!» : tactic unit :=
tactic.fail "todo"

example : true := by by_contra!

PRs are of course also welcome, but Lean 4 is on the horizon.

[Kevin Buzzard]

Just to add that "have p>n, by contra, assume p<=n" is pretty much exactly what a mathematician would write on a blackboard -- that's what Johan's idea has going for it

[Kevin Buzzard]

I really like observe too

[Yury G. Kudryashov]

I would love to have a by_cases! too, or even something that does

have := em p,
push_neg at this,
rcases this with (...|...),

[Yury G. Kudryashov]

This is useful, e.g., when I want to say: either ∀ x, f x ≤ g x, or ∃ x, g x < f x.

[Mario Carneiro]

Never See a Negation Again (TM)

[Kevin Buzzard]

Classical mathematicians don't take them seriously :-)

[Yaël Dillies]

I personally became quite fluent in using has_le.le.eq_or_lt, ne.lt_or_lt, lt_trichotomy to optimize my case disjunctions, and I've been shortening quite a few existing proofs that doing by_cases then rewriting to what they actually wanted to end up with.

[Johan Commelin]

@Mario Carneiro do you want to PR your assume_by_contra as by_contra'? Or would you mind if I do that?

[Mario Carneiro]

go ahead

[Johan Commelin]

I feel like the following doesn't really belong in tactic.norm_num. Which file should it move to?

/-- Reflexivity conversion: given `e` returns `(e, ⊢ e = e)` -/
meta def refl_conv (e : expr) : tactic (expr × expr) :=
do p ← mk_eq_refl e, return (e, p)

/-- Turns a conversion tactic into one that always succeeds, where failure is interpreted as a
proof by reflexivity. -/
meta def or_refl_conv (tac : expr → tactic (expr × expr))
  (e : expr) : tactic (expr × expr) := tac e <|> refl_conv e

/-- Transitivity conversion: given two conversions (which take an
expression `e` and returns `(e', ⊢ e = e')`), produces another
conversion that combines them with transitivity, treating failures
as reflexivity conversions. -/
meta def trans_conv (t₁ t₂ : expr → tactic (expr × expr)) (e : expr) :
  tactic (expr × expr) :=
(do (e₁, p₁) ← t₁ e,
  (do (e₂, p₂) ← t₂ e₁,
    p ← mk_eq_trans p₁ p₂, return (e₂, p)) <|>
  return (e₁, p₁)) <|> t₂ e

[Anne Baanen]

If nowhere else fits, I guess tactic/basic.lean?

[Johan Commelin]

That's just a long list of imports.

[Johan Commelin]

@Mario Carneiro Can we soup up by_contra' h : t, so that t is equal to \not goal modulo push_neg?

[Johan Commelin]

In other words, t doesn't have to be equal to the result of push_neg(\not goal). But push_neg(t) should be.

[Johan Commelin]

@Mario Carneiro Does this look right?

meta def by_contra' (h : parse ident?) (t : parse (tk ":" *> texpr)?) : tactic unit := do
  let h := h.get_or_else `this,
  applyc ``classical.by_contradiction,
  h₁ ← tactic.intro h,
  t' ← infer_type h₁,
  (e', pr') ← push_neg.normalize_negations t' <|> refl_conv t',
  match t with
  | none := () <$ replace_hyp h₁ e' pr'
  | some t := do
    t ← to_expr ``(%%t : Prop),
    (e, pr) ← push_neg.normalize_negations t <|> refl_conv t,
    unify e e',
    () <$ replace_hyp h₁ e `(@eq.trans Prop %%t' %%e %%t %%pr' (eq.symm %%pr))
  end

[Mario Carneiro]

you can use mk_eq_trans toward the end there

[Mario Carneiro]

see trans_conv above for inspiration

[Johan Commelin]

Like so?

    p_aux ← mk_eq_symm pr,
    p ← mk_eq_trans pr' p_aux,
    () <$ replace_hyp h₁ e p

[Mario Carneiro]

the cool kids write mk_eq_symm pr >>= mk_eq_trans pr' >>= replace_hyp h₁ e :D

[Johan Commelin]

gotcha

[Johan Commelin]

@Mario Carneiro do you agree if I move those refl_conv things to tactic/core.lean?

[Mario Carneiro]

yes, go ahead. You are right that they are misplaced

[Johan Commelin]

#9619