Zulip Chat Archive

Stream: new members

Topic: proof of false, but false is not the goal


view this post on Zulip Golol (Oct 21 2020 at 20:18):

Uhm.. so I did a rewrite and suddenly had h : \not z = z in my tactic state. It wasn't hard to get a proof of false from this. But I am not in a proof by contradiction right now. I thought in that case I should have false as the goal.
This is (part of) my Tactic state at one point:

hneq: ¬z = z
heq: z = z
contr: false
 ¬∥x - z = 0

The whole thing is part of a pretty large proof but here is an isolated version of the situation. Weird things start happening at
rw (@sub_left_inj ℂ _ z x z).1 at hneq.

constants f Δ :  -> 
constant z : 
constant hf2 :  (x : ), Δ x * (x - z) = f x - f z

lemma hcalc :  (x : ) (hneq : x  z), x - z∥⁻¹ * f x - f z - (x - z) * (Δ z) = ∥Δ x - Δ z
  := begin
  intro x,
  intro hneq,
  rw hf2,
  rw mul_comm (x - z) (Δ z),
  rw sub_mul (Δ x) (Δ z) (has_sub.sub x z),
  rw normed_field.norm_mul (Δ x - Δ z) (x - z),
  rw mul_comm (x - z∥⁻¹) (∥Δ x - Δ z * x - z),
  rw mul_assoc (∥Δ x - Δ z) (x - z) (x - z∥⁻¹),
  have hneq2 : x - z  0,
    unfold ne,
    unfold ne at hneq,
    rw (@sub_left_inj  _ z x z).1 at hneq,
    have heq, from eq.refl z,
    have contr, from (not_and_self (z=z)).1 (and.intro hneq heq),
    exact false.elim contr,
  rw (@sub_left_inj  _ z x z).2,
  end

At the end I have

x: 
hneq: ¬x = z
 x = z

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:20):

If you have contradictory hypotheses then you can stop right there -- you've proved your theorem. I don't see what's weird about this.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:20):

Just do cases on contr. There are no cases, so the goal will be closed.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:21):

https://en.wikipedia.org/wiki/Principle_of_explosion

view this post on Zulip Golol (Oct 21 2020 at 20:22):

I guess just don't understand how I entered a proof by contradiction? At rw (@sub_left_inj ℂ _ z x z).1 at hneq, a new goal gets introduced for reasons I don't understand and I can contradict.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:22):

exfalso is a tactic which just turns your goal into false

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:22):

so you could do exfalso, assumption too

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:24):

If you provided a #mwe we would be able to easily investigate.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:25):

import tactic

variables (P Q : Prop)

-- I have nothing up my sleeve. This is a straightforward proof which is
-- valid in constructive logic.
example : (P  Q)  (¬ Q  ¬ P) :=
begin
  intro hPQ,
  intro hnQ,
  intro hP,
  /-
  P Q : Prop
  hPQ : P → Q
  hnQ : ¬Q
  hP : P
  ⊢ false
  -/
  -- goal is `false` but I am not doing a proof by contradiction!
  apply hnQ,
  /-
  P Q : Prop
  hPQ : P → Q
  hnQ : ¬Q
  hP : P
  ⊢ Q
  -/
  -- goal is no longer `false`!
  apply hPQ,
  assumption,
end

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:28):

If you are confused about proving false it's probably because you haven't accepted enough that, in those foundations, the definition of "not P" is "P implies false".

view this post on Zulip Golol (Oct 21 2020 at 20:28):

Patrick Massot said:

If you provided a #mwe we would be able to easily investigate.

The code above works if you copy paste it into an empty file, I'll try to reduce it.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:28):

No it doesn't.

view this post on Zulip Golol (Oct 21 2020 at 20:29):

oh

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:29):

Did you try?

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:29):

Hint: you have written no import line.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:30):

I imported complexes but couldn't get norms to work. I don't know this part of the library. You can check to see if your code runs for other people using just one click nowadays (top right of the code block).

view this post on Zulip Golol (Oct 21 2020 at 20:30):

Sorry, there you go :D

import analysis.complex.basic

universes u v w
noncomputable theory

constants f Δ :  -> 
constant z : 
constant hf2 :  (x : ), Δ x * (x - z) = f x - f z

lemma hcalc :  (x : ) (hneq : x  z), x - z∥⁻¹ * f x - f z - (x - z) * (Δ z) = ∥Δ x - Δ z
  := begin
  intro x,
  intro hneq,
  rw hf2,
  rw mul_comm (x - z) (Δ z),
  rw sub_mul (Δ x) (Δ z) (has_sub.sub x z),
  rw normed_field.norm_mul (Δ x - Δ z) (x - z),
  rw mul_comm (x - z∥⁻¹) (∥Δ x - Δ z * x - z),
  rw mul_assoc (∥Δ x - Δ z) (x - z) (x - z∥⁻¹),
  have hneq2 : x - z  0,
    unfold ne,
    unfold ne at hneq,
    rw (@sub_left_inj  _ z x z).1 at hneq,
    have heq, from eq.refl z,
    have contr, from (not_and_self (z=z)).1 (and.intro hneq heq),
    exact false.elim contr,
  rw (@sub_left_inj  _ z x z).2,
  end

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:31):

Thanks. That's a MWE.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:31):

Did you follow the tutorials project to understand negations in Lean?

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:32):

In particular you can prove your intermediate goal by:

  have hneq2 : x - z  0,
    intro H,
    apply hneq,
    exact eq_of_norm_sub_eq_zero H

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:32):

Or the sober have hneq2 : ∥x - z∥ ≠ 0 := λ H, hneq (eq_of_norm_sub_eq_zero H),

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:33):

But I think the answer to the question is simply that logic is logic, and sometimes you do get hypotheses and/or goals which are false, but I think the OP somehow thinks that this is more meaningful than it actually is. My example was supposed to be simple case of this, where there is definitely no proof by contradiction, and where at some point the hypotheses are contradictory and the goal is false -- it doesn't have any profound logical meaning.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:33):

If this looks like black magic then I strongly advise you to follow the tutorials.

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:35):

Patrick's proof also passes through a temporary state where the goal is false, just like my example.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:35):

Sure, but my point is there is no proof by contradiction here, only proofs of negations and use of negation.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:36):

Golol, after proving this hneq2 I recommend rewriting using mul_inv_cancel.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:38):

Then the next step is a crucial formalization trick: your lemma doesn't need the assumption hneq. So, once you'll be done with this proof, get rid of this assumption, adjusting the proof as required (we can give more hints here if needed). Then each time you'll want to apply this lemma, you won't have to check the assumption!

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:39):

Many of the arguments which mathematicians think are proofs by contradiction are not proofs by contradiction to the constructivists anyway. For example the proof that no rational squared is 2 starts "assume that there's a rational whose square is 2, and proceed by contradiction". But "not P" is the same as "P implies false" in Lean so this is literally a direct proof of the statement. Intermediate goals which are false are fine as long as hypotheses are also contradictory, and this has very little to do with what either you or a constructivist thinks a proof by contradiction is. Any proof involving \not= could well have falses flying around at some point.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:39):

It's not only about constructivism, it really helps in Lean to have clear ideas about this.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:41):

Something else: you shouldn't be using constant here. This is not what this keyword is meant to be used for. It works here but this is somehow an accident.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:44):

Here you are adding to Lean's axiomatic system the existence of two functions and a complex number satisfying a certain relation, and then prove some consequences of this relation. This is certainly not what you mean. What you presumably mean is that for all pairs of functions and complex number satisfying this relation you get the result of hcalc. So you you can either put those objects in the declaration hcalc or use the keyword variables if you fear you'll have to repeat things in a lot of other lemmas.

view this post on Zulip Golol (Oct 21 2020 at 20:45):

Ok so I understand that simply the definition of negation happened here but it happened at a point where I didn't expect it. But there are two things which still confuse me
1) How did I introduce a new subgoal by doing `rw (@sub_left_inj ℂ _ z x z).1 at hneq
2) In the last line my tactic state is

x: 
hneq: ¬x = z
 x = z

From this it seems like it isn't possible to finish the proof. I just want to have it clear in my mind that this can totally happen if you take the wrong steps in your tactic proof, right? Just like a generalize can make your goal impossible.
The constants were just there to make the example work

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:46):

You rewrote (blah).1 which was of the form A -> (X = Y) so a new goal of A appeared.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 20:46):

yes, if you take the wrong steps in your tactic proof you can end up with something unprovable

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:47):

e.g. applying exfalso at any point where your hypotheses are not contradictory will make your goal impossible to prove.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 20:47):

unfortunately, you cannot just keep entering random characters until the formula is proved. you have to make intelligent mathematical decisions. this is inconvenient but unavoidable

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:47):

tactics have consequences. Use them wisely :-)

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:49):

@Kevin Lacker , I don't think it helps to suggest that Golol is entering random characters.

view this post on Zulip Golol (Oct 21 2020 at 20:49):

I will brute force the RH proof term and you can not stop me!

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:50):

I think Kevin is just making the general point that when playing this game, if you make random moves then you might get stuck -- it's not like some games where you can always keep going and dig yourself out of a hole

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:52):

Ok, I investigated the weird new goal.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:53):

The issue comes because you try to force the arguments to sub_left_inj and make the wrong choice here (probably by getting the wrong order of arguments). Lean tries to match with the goal anyway but succeeds only if you can prove this crazy goal.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:55):

Actually, before that rewrite, try typing have := (@sub_left_inj ℂ _ z x z).1,.

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:55):

You'll see the term you're trying to use to rewrite is x - z = z - z → x = z

view this post on Zulip Patrick Massot (Oct 21 2020 at 20:56):

So Lean will accept to rewrite x intoz but then ask you prove the premise x - z = z - z

view this post on Zulip Golol (Oct 21 2020 at 20:56):

Ooooh it is the wrong direction. My usb approach of adding a \left if the default direction doesnt work is faulted... :grinning:

view this post on Zulip Golol (Oct 21 2020 at 20:57):

I see now. Many thanks to everyone for the help!

view this post on Zulip Kevin Lacker (Oct 21 2020 at 20:58):

I am in favor of proving things by entering random characters. :smile: it doesn't really work with tactics, though, you have to add in backtracking. then it works

view this post on Zulip Kevin Buzzard (Oct 21 2020 at 20:58):

Kevin Lacker said:

I am in favor of proving things by entering random characters. :smile:

That's the machine learning approach, right? :-)

view this post on Zulip Patrick Massot (Oct 21 2020 at 21:01):

Below I've written a somewhat optimized version. You should look at it when you're happy with how you worked out the exercises (including removing the useless assumption).

view this post on Zulip Golol (Oct 21 2020 at 21:01):

Unironically, I hope that if in the future we have a large database of formal mathematics, machine learning approaches will yield great proof assistants.

view this post on Zulip Patrick Massot (Oct 21 2020 at 21:03):

Many people are working on this dream.

view this post on Zulip Kevin Lacker (Oct 21 2020 at 21:04):

yeah I feel like if a human specified the intermediate steps like, you have to split on x = z or x != z, it should be able to fill in the rset

view this post on Zulip Patrick Massot (Oct 21 2020 at 21:05):

In this specific case we immediately get to the crucial point that Lean should be much better in calculation, at the level of a computer algebra system (but without the wrong results they sometimes produce...).


Last updated: May 14 2021 at 13:24 UTC