proof of false, but false is not the goal

Stream: new members

[Golol]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Golol]

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.

[Kevin Buzzard]

exfalso is a tactic which just turns your goal into false

[Kevin Buzzard]

so you could do exfalso, assumption too

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Golol]

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.

[Patrick Massot]

No it doesn't.

[Golol]

oh

[Patrick Massot]

Did you try?

[Patrick Massot]

Hint: you have written no import line.

[Kevin Buzzard]

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

[Golol]

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

[Patrick Massot]

Thanks. That's a MWE.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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!

[Kevin Buzzard]

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.

[Patrick Massot]

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

[Patrick Massot]

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.

[Patrick Massot]

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.

[Golol]

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

[Kevin Buzzard]

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

[Kevin Lacker]

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

[Kevin Buzzard]

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

[Kevin Lacker]

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

[Kevin Buzzard]

tactics have consequences. Use them wisely :-)

[Patrick Massot]

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

[Golol]

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

[Kevin Buzzard]

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

[Patrick Massot]

Ok, I investigated the weird new goal.

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Golol]

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

[Golol]

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

[Kevin Lacker]

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

[Kevin Buzzard]

Kevin Lacker said:

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

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

[Patrick Massot]

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

lemma hcalc : ∀ x : ℂ, ∥x - z∥⁻¹ * ∥f x - f z - (x - z) * (Δ z)∥ = ∥Δ x - Δ z∥ :=
begin
  intro x,
  by_cases hneq : x = z,
  { simp [hneq] },
  have hneq2 : ∥x - z∥ ≠ 0 := λ H, hneq (eq_of_norm_sub_eq_zero H),
  rw [← hf2, show Δ x * (x - z) - (x - z) * Δ z = (x - z) * (Δ x - Δ z), by ring,
      normed_field.norm_mul, ← mul_assoc, inv_mul_cancel hneq2, one_mul],
end

[Golol]

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

[Patrick Massot]

Many people are working on this dream.

[Kevin Lacker]

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

[Patrick Massot]

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