# Zulip Chat Archive

## Stream: new members

### Topic: How do I convert ¬(a ∧ b) to ¬a ∨ ¬b in tactic mode?

#### Lars Ericson (Nov 21 2020 at 18:13):

I am working through exercises in chapter 3. One of these is

```
example : ¬(p ∧ q) → ¬p ∨ ¬q :=
begin
intro h,
end
```

After the `intro h`

my goal state is

```
p q : Prop,
h : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
```

I "know" from elementary propositional logic that `¬(p ∧ q)↔(¬p ∨ ¬q)`

. I'm getting stuck here on how to prove it. The obvious tactical move is to pick `left`

or `right`

. If I do

```
left,
intro h1,
```

then my goal state is

```
p q : Prop,
h : ¬(p ∧ q),
h1 : p
⊢ false
```

To make this work I would need to convert `h1`

to `p ∧ q`

but I don't have `q`

.

What tactics are available for this proof that I'm not using? It doesn't seem like I'm looking for `em`

because I don't have a `p ∨ ¬p`

situation.

#### Adam Topaz (Nov 21 2020 at 18:17):

docs#not_and_distrib or something like that...

#### Adam Topaz (Nov 21 2020 at 18:17):

So you can `rw not_and_distrib at h`

#### Adam Topaz (Nov 21 2020 at 18:18):

Oh sorry... You're doing the exercise!

#### Adam Topaz (Nov 21 2020 at 18:18):

(so you shouldn't cheat and use the lemma)

#### Bryan Gin-ge Chen (Nov 21 2020 at 18:26):

The obvious tactical move is to pick left or right.

Unfortunately, this is not the right move in this case. As mentioned in the text before the exercise, you'll need to use classical logic, so try `by_cases`

or `by_contra`

.

#### Lars Ericson (Nov 21 2020 at 19:36):

Is there an equivalent of `by_cases`

and `by_contra`

that is natural for tactic mode? The examples are term mode. Also is there an up to date Lean 3 quick reference guide? This one doesn't have `by_cases`

and `by_contra`

, it is only for Lean 2.

Or well never mind I guess this is the cheat sheet, but it is not a one-pager: https://leanprover-community.github.io/mathlib_docs/core/init/meta/tactic.html#tactic.by_cases

#### Adam Topaz (Nov 21 2020 at 19:40):

`by_contra`

and `by_cases`

are tactics.

#### Adam Topaz (Nov 21 2020 at 19:41):

https://leanprover-community.github.io/mathlib_docs/tactics.html

#### Adam Topaz (Nov 21 2020 at 19:42):

(Although that page contains some tactics from mathlib)

#### Lars Ericson (Nov 21 2020 at 19:43):

If I do `by_cases p → q,`

, it gives me two goals both labelled `h`

. Is there a way to pick the label? Doing `by_cases p → q h1`

gives `unknown identifier 'h1'`

and doing `by_cases p → q with h1`

causes `invalid 'begin-end' expression, ',' expected`

.

#### Adam Topaz (Nov 21 2020 at 19:44):

`by_cases h1 : p \to q`

#### Adam Topaz (Nov 21 2020 at 19:46):

You can also take a look at the `dedup`

tactic :)

#### Adam Topaz (Nov 21 2020 at 19:46):

But it's better just to start off with an explicit name which is different from h.

#### Lars Ericson (Nov 21 2020 at 19:50):

This does something confusing:

```
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
by_cases h2: (p → q),
end
```

The first goal gets the `h2`

label, which I expected. The second goal gets two labels for an existing premise, which I didn't expect:

```
2 goals
p q : Prop,
h : ¬(p → q),
h2 : p → q
⊢ p ∧ ¬q
p q : Prop,
h h2 : ¬(p → q)
⊢ p ∧ ¬q
```

#### Adam Topaz (Nov 21 2020 at 19:51):

The `h`

and `h2`

are terms, and `p \to q`

is their type. You have two terms of the same type.

#### Lars Ericson (Nov 21 2020 at 19:51):

Never mind I understand now looking at it, it's changing both goals. My prior experience was that tactics only operated on the top goal.

#### Lars Ericson (Nov 21 2020 at 19:52):

So I guess the rule is that tactics operate on one or more applicable elements of the goal set and only complain if there are 0 applicable elements.

#### Adam Topaz (Nov 21 2020 at 19:52):

The `by_cases`

tactic takes a proposition `p`

and splits the goal into two, where the first one has a term of type `p`

and the second has a term of type `\not p`

.

#### Lars Ericson (Nov 21 2020 at 19:52):

Oh good point, thank you!

#### Adam Topaz (Nov 21 2020 at 19:54):

Under the hood, all that's going on is this:

```
open classical
variables (p q : Prop)
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
cases em (p → q) with h2 h2,
sorry,
sorry,
end
```

Here `em`

is "excluded middle"

#### Lars Ericson (Nov 21 2020 at 19:58):

@Adam Topaz I'm looping here, can you give me another hint?

```
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
by_cases h2: (p → q),
exfalso,
exact h h2,
by_contra h3,
by_cases h4: p ∧ ¬q,
exact h3 h4,
end
```

leads to goal state

```
p q : Prop,
h h2 : ¬(p → q),
h3 h4 : ¬(p ∧ ¬q)
⊢ false
```

#### Adam Topaz (Nov 21 2020 at 19:59):

I suggest to write down a proof with pen + paper first, and try to convert that into a lean proof.

#### Adam Topaz (Nov 21 2020 at 20:00):

In particular, the `by_cases`

line doesn't seem to buy you anything in this proof.

#### Eric Wieser (Nov 21 2020 at 20:02):

Your proof is calling `by_cases x`

on an `x`

you already know to be false (it's in your proof state). You should be using it on something that you don't know to be true or false yet (perhaps p or q?)

#### Adam Topaz (Nov 21 2020 at 20:07):

I suggest

```
open classical
variables {p q : Prop}
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
by_cases hp : p,
sorry,
sorry,
end
```

#### Lars Ericson (Nov 21 2020 at 20:39):

I'm stuck on a subgoal. If I have `p`

and `q`

as hypotheses, is there a way to introduce `p → q`

? I'm trying to prove this:

```
open classical
variables {p q r s : Prop}
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
begin
intro h1,
intro h2,
intro h3,
by_contra h4,
end
```

and I am in state

```
p q r : Prop,
h1 : (p → q) → r,
h2 : p,
h3 : q,
h4 : ¬r
⊢ false
```

#### Kevin Buzzard (Nov 21 2020 at 20:39):

Instead of `by_contra h4`

, why not just `apply h1`

?

#### Kevin Buzzard (Nov 21 2020 at 20:39):

You're trying to prove `r`

after all, and the conclusion of `h1`

is `r`

.

#### Lars Ericson (Nov 21 2020 at 20:41):

Thank you @Kevin Buzzard that works

```
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
begin
intro h1,
intro h2,
intro h3,
apply h1,
intro h4,
exact h3,
end
```

#### Kevin Buzzard (Nov 21 2020 at 20:48):

One way to prove all of these things is just to do cases on all the propositional variables and then let the simplifier deal with it. In my mind your goal in that question is something which can be solved by a truth table approach -- there are $2^3$ cases and that's the end of it. Giving a constructive proof is a lot more fun but somehow involves having ideas, whereas the classical method can be turned into an algorithm (`tauto!`

, in this case).

#### Kevin Buzzard (Nov 21 2020 at 20:51):

Here is a constructive term mode proof.

```
variables (p q r : Prop)
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
λ hpqr hp hq, _
```

```
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
λ hpqr hp hq, hpqr _
```

```
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
λ hpqr hp hq, hpqr $ λ hp2, _
```

```
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
λ hpqr hp hq, hpqr $ λ hp2, hq
```

#### Kevin Buzzard (Nov 21 2020 at 20:52):

It's just a translation of your tactic proof into compact term mode, which is a variant of term mode which is, for me, far easier to steer than the "chapter 3 term mode" stuff you were doing with all the `assume`

and `show`

stuff.

#### Kevin Buzzard (Nov 21 2020 at 20:52):

At each stage, I pause at the `_`

and look at the goal in the infoview and figure out what to do next.

#### Bryan Gin-ge Chen (Nov 21 2020 at 20:54):

`assume`

is just a more verbose way of saying `λ`

, and (I think) `show`

is just a way of giving an explicit type ascription like with `:`

except up front instead of after the term.

#### Adam Topaz (Nov 21 2020 at 20:55):

I think of `show`

as being analogous to `change`

in tactic mode. I might be wrong though...

#### Bryan Gin-ge Chen (Nov 21 2020 at 20:59):

It's all a bit confusing. In tactic mode there's also tactic#show which lets you choose which goal you want to work on.

#### Lars Ericson (Nov 21 2020 at 21:07):

With the help of `implies_commutative`

I got a little bit farther and then stuck . I am trying

```
lemma not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := iff.rfl
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
rw not_iff_imp_false (p → q) at h,
have hp1 := implies_commutative h,
by_cases hp : p,
have hp1p := hp1 hp,
split,
exact hp,
rw ← not_iff_imp_false at hp1p,
exact hp1p,
end
```

and I get to goal state

```
p q : Prop,
h : (p → q) → false,
hp1 : p → q → false,
hp : ¬p
⊢ p ∧ ¬q
```

which doesn't look provable unless I can abstract `h`

, instantiate the `q`

with false and then I'm done.

#### Ruben Van de Velde (Nov 21 2020 at 21:10):

(p → q) is true if p is false (`hp`

), right?

#### Lars Ericson (Nov 21 2020 at 21:12):

Yes so I do this

```
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
rw not_iff_imp_false (p → q) at h,
have hp1 := implies_commutative h,
by_cases hp : p,
have hp1p := hp1 hp,
split,
exact hp,
rw ← not_iff_imp_false at hp1p,
exact hp1p,
split,
exfalso,
rw not_iff_imp_false at hp,
have hf := h hp,
end
```

and the goal state before the last `have`

is

```
p q : Prop,
h : (p → q) → false,
hp1 : p → q → false,
hp : p → false
⊢ false
```

so I think I should be able to do (h hp) but it won't unify `p → q`

with `p → false`

, so I think I need to universally quantify `h`

first, and then instantiate it, is that right?

#### Reid Barton (Nov 21 2020 at 21:14):

No, again, `h`

is a hypothesis about the specific `q`

in your tactic state

#### Lars Ericson (Nov 21 2020 at 21:15):

But I'm not seeing `forall.intro`

in the docs.

#### Ruben Van de Velde (Nov 21 2020 at 21:15):

Try `apply h`

#### Reid Barton (Nov 21 2020 at 21:15):

If you ever read something about quantification in traditional presentations of first order logic it probably helps to forget it.

#### Reid Barton (Nov 21 2020 at 21:17):

You need to apply `h`

and prove its antecedent `p -> q`

--in tactic mode you can do these in either order

#### Lars Ericson (Nov 21 2020 at 21:19):

I've succeeded in making a longer partial proof

```
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
rw not_iff_imp_false (p → q) at h,
have hp1 := implies_commutative h,
by_cases hp : p,
have hp1p := hp1 hp,
split,
exact hp,
rw ← not_iff_imp_false at hp1p,
exact hp1p,
split,
exfalso,
rw not_iff_imp_false at hp,
apply h,
intro hp2,
exfalso,
exact hp hp2,
exfalso,
apply hp,
end
```

which dead-ends at this goal:

```
p q : Prop,
h : (p → q) → false,
hp1 : p → q → false,
hp : ¬p
⊢ p
```

#### Lars Ericson (Nov 21 2020 at 21:23):

In other words I'm cycling. I can try going back to lambda expressions and looking at _'s.

#### Ruben Van de Velde (Nov 21 2020 at 21:24):

You could prove `p`

because your assumptions were contradictory, they still are when proving `¬q`

#### Ruben Van de Velde (Nov 21 2020 at 21:28):

(Alternatively, note that you could also prove `p ∧ ¬q`

that way.)

#### Adam Topaz (Nov 21 2020 at 21:29):

Here are a few more hints

#### Reid Barton (Nov 21 2020 at 21:30):

Given `hp : ¬p`

what can you say about `p → q`

?

#### Ruben Van de Velde (Nov 21 2020 at 21:36):

@Adam Topaz

#### Adam Topaz (Nov 21 2020 at 21:37):

(I figured it would be helpful to break everything down completely, for the sake of the example)

#### Adam Topaz (Nov 21 2020 at 21:42):

:rofl:

#### Lars Ericson (Nov 21 2020 at 21:46):

Thanks @Adam Topaz @Reid Barton @Ruben Van de Velde @Kevin Buzzard , I got there a different way, kind of ugly, but it compiles. I will study your versions for new tools like _-following and `assumption`

tactic which I haven't used for anything, plus more term mode. Here is my version:

```
open classical
variables {p q r s : Prop}
theorem implies_commutative : ((p → q) → r) → (p → (q → r)) :=
begin
intro h1,
intro h2,
intro h3,
apply h1,
intro h4,
exact h3,
end
lemma not_iff_imp_false (P : Prop) : ¬ P ↔ P → false := iff.rfl
theorem or_equiv (p q : Prop): (¬p ∨ q) → (p → q) :=
begin
intro h,
intro h1,
cases h,
exfalso,
exact h h1,
exact h,
end
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
rw not_iff_imp_false (p → q) at h,
have hp1 := implies_commutative h,
by_cases hp : p,
have hp1p := hp1 hp,
split,
exact hp,
rw ← not_iff_imp_false at hp1p,
exact hp1p,
split,
exfalso,
rw not_iff_imp_false at hp,
apply h,
intro hp2,
exfalso,
exact hp hp2,
have hq := or.intro_left q hp,
have foo := or_equiv p q hq,
have bar := h foo,
exfalso,
exact bar,
end
```

#### Lars Ericson (Nov 21 2020 at 21:55):

@Adam Topaz I'm looking at your hint and I'm confused about one thing. Starting here:

```
example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
by_cases hp : p,
{ split,
assumption,
...
```

just before the `assumption`

, the goal state is

```
p q : Prop,
h : ¬(p → q),
hp : p
⊢ p
```

Applying `assumption`

turns this into

```
p q : Prop,
h : ¬(p → q),
hp : p
⊢ ¬q
```

I read this as saying that it applied `h : ¬(p → q)`

to `p`

. However `h`

is really of type `h : (p → q)→ false`

, not of type `h:p→ (q→ false)`

. So the application should fail. Why is it working with the `assumption`

to give `q→ false`

?

#### Adam Topaz (Nov 21 2020 at 21:56):

No, it's just applying the assumption `hp`

from the context to prove goal `p`

#### Adam Topaz (Nov 21 2020 at 21:57):

After that, lean moves on to the next goal

#### Lars Ericson (Nov 21 2020 at 22:03):

Thanks I see it just got rid of one goal and what I'm seeing is the remaining goal.

#### Kevin Buzzard (Nov 22 2020 at 13:36):

If you were to use `{}`

s in your code so as to always have one goal, as is recommended by the style guide, you would not have confused yourself in this manner.

#### Adam Topaz (Nov 22 2020 at 14:19):

This was probably my fault, I didn't put `{}`

in the hint above because `assumption`

takes care of the first goal immediately. In real life, I would use `refine < hp, _ >,`

instead of `split`

so that lean only leaves one goal instead of two

#### Lars Ericson (Nov 22 2020 at 15:53):

@Adam Topaz "in real life" (Lean sources) it seems that terse term mode is the rule and tactic mode is rarely if ever used for internals.

@Kevin Buzzard I had a moment of enlightenment just now about what "truth table approach" means. If there are variables `p1,p2,p3...`

it means

```
by_cases h1: p1,
by_cases h2: p2,
by_cases h3: p3,
```

as in

```
theorem nand_left (p q : Prop) : ¬(p ∧ q) → ¬p ∨ ¬q :=
begin
intro h,
rw not_iff_imp_false at h,
by_cases h1 : p,
by_cases h2 : q,
exfalso,
exact h (and.intro h1 h2),
exact (or.intro_right (¬p) h2),
exact (or.intro_left (¬q) h1),
end
```

#### Kevin Buzzard (Nov 22 2020 at 15:56):

Right. In classical logic there's an algorithm for proving all the true first order propositional calculus theorems, which is "write out the truth table". When you get bored writing it out manually (by doing cases on the variables and using `simp`

) you can just start using tactics like `tauto!`

which do it all for you. Constructively it's a different story, that's what all this intro, split, apply stuff is

#### Yakov Pechersky (Nov 22 2020 at 16:11):

Wouldn't dec_trivial also work?

#### Yakov Pechersky (Nov 22 2020 at 16:11):

Because bool is a fintype

#### Adam Topaz (Nov 22 2020 at 16:14):

`bool != Prop`

#### Lars Ericson (Nov 22 2020 at 16:26):

I finally finished every exercise in chapter 3. Chapter 4 beckons. I am curious if there is a more tactic-style way to do `iff.elim`

rather than this term style application:

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
have h2 := iff.elim_left h,
have h3 := iff.elim_right h,
by_cases h4 : p,
{ have h5 := h2 h4,
exact h5 h4, },
{ have h5 := h3 h4,
exact h4 h5, }
end
```

#### Yakov Pechersky (Nov 22 2020 at 16:32):

How about an "apply h.mp" after the first intro h?

#### Lars Ericson (Nov 22 2020 at 16:35):

@Yakov Pechersky the instructions on the last exercise are "Prove ¬(p ↔ ¬p) without using classical logic". I think `h.mp`

would be out of scope.

#### Lars Ericson (Nov 22 2020 at 16:36):

I'm just curious if there is a more "tactonic" way to split up an equivalence into left and right hand directions than `iff.elim`

.

#### Yakov Pechersky (Nov 22 2020 at 16:36):

Why is that a classical approach if you use the iff.mp?

#### Yakov Pechersky (Nov 22 2020 at 16:37):

That's exactly the iff in the left to right direction implication

#### Yakov Pechersky (Nov 22 2020 at 16:37):

Classical logic means em or by_cases

#### Kevin Buzzard (Nov 22 2020 at 16:43):

It's the `by_cases`

which is out of scope for this one, and this is a famously tricky one.

#### Adam Topaz (Nov 22 2020 at 16:44):

@Lars Ericson To answer your quuestion about splitting, you can use the following:

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
cases h with h2 h3,
-- have h2 := iff.elim_left h,
-- have h3 := iff.elim_right h,
by_cases h4 : p,
{ have h5 := h2 h4,
exact h5 h4, },
{ have h5 := h3 h4,
exact h4 h5, }
end
```

#### Lars Ericson (Nov 22 2020 at 17:37):

@Kevin Buzzard when I look at this without using `by_cases`

, the first thing I want to do is convert `p → q`

to `¬p ∨ q`

, because the natural start to the proof:

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
cases h with h2 h3,
end
```

leaves me in a goal state with two implications and no premise, and neither implication can be applied as a premise to the other:

```
p : Prop,
h2 : p → ¬p,
h3 : ¬p → p
⊢ false
```

However, to access the definition of implication, I need to prove it, and the only way I could do it was with `by_cases`

, which is out of scope:

```
theorem definition_imply (p q : Prop): (p → q) → (¬p ∨ q) :=
begin
intro h,
by_cases hp : p,
have hq := h hp,
right,
assumption,
left,
assumption,
end
```

What other tricks are available to allow me to rewrite the implication without using classical logic?

#### Kevin Buzzard (Nov 22 2020 at 18:02):

You can't rewrite an implication, I don't know what you mean. The question is hard. I can give you a hint which usually gives it away.

#### Lars Ericson (Nov 22 2020 at 18:05):

@Kevin Buzzard, by rewrite an implication, I simply mean replace `p → q`

with `¬p ∨ q`

, There is no automatic translation that I know of in the system. It has to be proved in some way. My proof above of `definition_imply`

uses `by_cases`

so it is out of scope. Does Lean have another rewrite rule which is not classical which will replace `p → q`

with `¬p ∨ q`

? That's all the hint I need to move a little further.

#### Kevin Buzzard (Nov 22 2020 at 18:06):

Is this thing you want to use provable constructively? If so then just prove it (`have h : (p -> q) \iff (\not p \or q)`

) and then rewrite it.

#### Kevin Buzzard (Nov 22 2020 at 18:07):

(I should say that I neither know nor care whether this is provable constructively)

#### Marc Huisinga (Nov 22 2020 at 18:08):

it isn't, as mentioned in exercise 3.7.2 :)

#### Lars Ericson (Nov 22 2020 at 18:08):

With `q=p`

, this is the Law of the Excluded Middle, so it is out of scope.

#### Marc Huisinga (Nov 22 2020 at 18:09):

@Lars Ericson can you prove `¬p`

in your goal, on paper?

#### Bryan Gin-ge Chen (Nov 22 2020 at 18:10):

(`end_of_chapter_3`

is definitely provable constructively.)

#### Lars Ericson (Nov 22 2020 at 18:11):

@Marc Huisinga I don't think so. My goal state is `false`

and my hypotheses are two implications that don't "fit" each other, and without being able to introduction symmetric assumptions with `by_cases`

, I am stuck. That is, start from

```
h2 : p → (p→ false),
h3 : (p→ false)→ p
```

I don't have any of the premises `p`

or `p→ false`

available, so I can't move, I don't have any rules to apply.

#### Marc Huisinga (Nov 22 2020 at 18:12):

can you somehow prove `(p → false)`

, i.e. make it available?

#### Lars Ericson (Nov 22 2020 at 18:13):

I don't know how to introduce `p → false`

as an assumption without using `by_cases`

. It doesn't prove itself, as it is not generally true. If it was `p → true`

I'd be in better shape.

#### Kevin Buzzard (Nov 22 2020 at 18:16):

`have h : p → false,`

and then prove it.

#### Marc Huisinga (Nov 22 2020 at 18:16):

with `have h4 : p → false, { ... },`

you can make it a goal to prove it, where `...`

is your proof of `p → false`

. after completing `...`

, you can use `h4`

in your proof

#### Lars Ericson (Nov 22 2020 at 18:20):

Oh OK I didn't know I could throw any hypothesis in with `have`

, I thought I always had to construct it. `by_cases`

is a kind of double `have`

and I assumed the reason it was double was because that was sound. Actually I can mimic `by_cases`

with two `have`

statements that insert unproven propositions. I am being constructive by just not inserting the second one?

#### Lars Ericson (Nov 22 2020 at 18:23):

Also, the action of doing `h4 : p → false`

doesn't actually impact my current goal. It just creates a second goal. I'm still stuck with the first goal. If my start is:

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
cases h with h2 h3,
{ have h4: ¬p,
},
sorry
end
```

then after the `have h4: ¬p`

my goal state is

```
2 goals
p : Prop,
h2 : p → ¬p,
h3 : ¬p → p
⊢ ¬p
p : Prop,
h2 : p → ¬p,
h3 : ¬p → p,
h4 : ¬p
⊢ false
```

#### Marc Huisinga (Nov 22 2020 at 18:24):

the first goal requires you to prove `h4 : ¬p`

, whereas the second goal has `h4`

in its assumptions

#### Lars Ericson (Nov 22 2020 at 18:25):

Thanks I get it, I can do an `apply`

here.

#### Marc Huisinga (Nov 22 2020 at 18:27):

remember that `¬p = p → false`

#### Lars Ericson (Nov 22 2020 at 18:31):

With `apply`

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
cases h with h2 h3,
{ have h4: ¬p,
apply h2,
apply h3,
},
sorry
end
```

The `apply`

s cycle me between a top goal state of either `p`

or `¬p`

. It's a loop

```
2 goals
p : Prop,
h2 : p → ¬p,
h3 : ¬p → p
⊢ p
p : Prop,
h2 : p → ¬p,
h3 : ¬p → p,
h4 : ¬p
⊢ false
```

#### Lars Ericson (Nov 22 2020 at 18:33):

According to Wikipedia, I should have access to an axiom of form `¬(¬(p ∨¬p))`

. This might be helpful. What's it's name in Lean?

#### Kevin Buzzard (Nov 22 2020 at 18:33):

You can look up lemma names using `library_search`

.

#### Marc Huisinga (Nov 22 2020 at 18:34):

instead of apply, try intro

#### Lars Ericson (Nov 22 2020 at 18:34):

Or actually it might be the opposite of helpful, it's just telling me I can't do `by_cases`

.

Thanks I will try `intro`

.

#### Lars Ericson (Nov 22 2020 at 18:45):

So finally, finally, end of chapter 3:

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
cases h with h2 h3,
have h4: ¬p,
apply h2,
apply h3,
intro h4,
have h5 := h2 h4,
exact h5 h4,
have h6 := h3 h4,
exact h4 h6,
end
```

#### Adam Topaz (Nov 22 2020 at 18:52):

Bonus points: make a term-mode proof!

#### Yakov Pechersky (Nov 22 2020 at 18:52):

Why wouldn't just "intro h, apply h.mp, intro hp, exact hp" work

#### Marc Huisinga (Nov 22 2020 at 18:56):

Yakov Pechersky said:

Why wouldn't just "intro h, apply h.mp, intro hp, exact hp" work

applying `h.mp`

yields two goals of `p`

, not `p → p`

#### Yakov Pechersky (Nov 22 2020 at 19:02):

OK, then rewrite with h, intro, which gives a hypothesis of "false" which can prove anything

#### Kevin Buzzard (Nov 22 2020 at 19:02):

The rewrite fails. It's p iff (not p), right? You can't rewrite a `false`

goal with that.

#### Yakov Pechersky (Nov 22 2020 at 19:03):

I mean, for the two goals of p

#### Kevin Buzzard (Nov 22 2020 at 19:05):

You rewrite with h and then intro and you get a *goal* of false, and a hypothesis of p. You can do it this way but it's longer (and you have to do it twice).

#### Yakov Pechersky (Nov 22 2020 at 19:05):

Ah, I see, never mind

#### Ruben Van de Velde (Nov 22 2020 at 19:05):

A little shorter:

```
theorem end_of_chapter_3 (p: Prop) : ¬(p ↔ ¬p) :=
begin
intro h,
cases h with h2 h3,
have h4: ¬p,
{ intro hp,
exact h2 hp hp },
have h6 := h3 h4,
exact h4 h6,
end
```

#### Marc Huisinga (Nov 22 2020 at 19:10):

not many steps to a term-mode proof from there :)

#### Adam Topaz (Nov 22 2020 at 19:50):

I've been trying to figure out how to make animated gifs for teaching... Anyway, I made a little animation explaining how to convert the above proof to a term-mode proof, in case it helps.

output.gif

#### Lars Ericson (Nov 22 2020 at 19:54):

Thanks @Adam Topaz this visually and beautifully helps me out of the woods of converting tactics to terms.

#### Adam Topaz (Nov 22 2020 at 19:55):

No problem. I think seeing other people golfing in lean is helpful when you're first starting out :)

#### Lars Ericson (Nov 22 2020 at 20:07):

This GIF as an MP4 would be a great addition to the Xena Channel: https://www.youtube.com/channel/UCtdYf-CsDI215SqaQ3XYx1A

#### Adam Topaz (Nov 22 2020 at 20:35):

I think the emacs might scare off too many people :rofl:

#### Lars Ericson (Nov 22 2020 at 21:32):

I grew up on Emacs but haven't set it up for Lean yet.

The animated GIF is a little hard to scroll through and there's a lot to learn there, so, on Ubuntu,

```
ffmpeg -i output.gif -movflags faststart -pix_fmt yuv420p -vf "scale=trunc(iw/2)*2:trunc(ih/2)*2" video.mp4
```

makes an MP4 which is a lot easier to view.

#### Adam Topaz (Nov 22 2020 at 21:37):

Here's a higher quality mp4

output.mp4

#### Adam Topaz (Nov 22 2020 at 21:38):

BTW, do you know of an easy way of making such gifs on linux? I used a roundabout way by using OBS to make a .mkv file, then I used ffmpeg to convert to a gif. Is there an easier / more direct way?

#### Kevin Buzzard (Nov 22 2020 at 21:50):

I use peek (Patrick told me about it).

#### Adam Topaz (Nov 22 2020 at 21:54):

Nice. peek is even in my distro's official package repo

Last updated: May 13 2021 at 21:12 UTC