# Zulip Chat Archive

## Stream: new members

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

#### 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
```

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

#### Kevin Buzzard (Oct 21 2020 at 20:20):

Just do cases on `contr`

. There are no cases, so the goal will be closed.

#### Kevin Buzzard (Oct 21 2020 at 20:21):

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

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

#### Kevin Buzzard (Oct 21 2020 at 20:22):

`exfalso`

is a tactic which just turns your goal into `false`

#### Kevin Buzzard (Oct 21 2020 at 20:22):

so you could do `exfalso, assumption`

too

#### Patrick Massot (Oct 21 2020 at 20:24):

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

#### 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
```

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

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

#### Patrick Massot (Oct 21 2020 at 20:28):

No it doesn't.

#### Golol (Oct 21 2020 at 20:29):

oh

#### Patrick Massot (Oct 21 2020 at 20:29):

Did you try?

#### Patrick Massot (Oct 21 2020 at 20:29):

Hint: you have written no `import`

line.

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

#### 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
```

#### Patrick Massot (Oct 21 2020 at 20:31):

Thanks. That's a MWE.

#### Patrick Massot (Oct 21 2020 at 20:31):

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

#### 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
```

#### 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),`

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

#### Patrick Massot (Oct 21 2020 at 20:33):

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

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

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

#### Patrick Massot (Oct 21 2020 at 20:36):

Golol, after proving this `hneq2`

I recommend rewriting using `mul_inv_cancel`

.

#### 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!

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

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

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

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

#### 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

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

#### 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

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

#### 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

#### Kevin Buzzard (Oct 21 2020 at 20:47):

tactics have consequences. Use them wisely :-)

#### Patrick Massot (Oct 21 2020 at 20:49):

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

#### Golol (Oct 21 2020 at 20:49):

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

#### 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

#### Patrick Massot (Oct 21 2020 at 20:52):

Ok, I investigated the weird new goal.

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

#### Patrick Massot (Oct 21 2020 at 20:55):

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

.

#### 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`

#### Patrick Massot (Oct 21 2020 at 20:56):

So Lean will accept to rewrite `x`

into`z`

but then ask you prove the premise `x - z = z - z`

#### 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:

#### Golol (Oct 21 2020 at 20:57):

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

#### 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

#### 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? :-)

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

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

#### Patrick Massot (Oct 21 2020 at 21:03):

Many people are working on this dream.

#### 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

#### 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