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


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_casesline 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.introin 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


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?

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

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

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

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

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