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

Stream: new members

[Lars Ericson]

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]

docs#not_and_distrib or something like that...

[Adam Topaz]

So you can rw not_and_distrib at h

[Adam Topaz]

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

[Adam Topaz]

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

[Bryan Gin-ge Chen]

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]

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]

by_contra and by_cases are tactics.

[Adam Topaz]

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

[Adam Topaz]

(Although that page contains some tactics from mathlib)

[Lars Ericson]

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]

by_cases h1 : p \to q

[Adam Topaz]

You can also take a look at the dedup tactic :)

[Adam Topaz]

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

[Lars Ericson]

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]

The hand h2 are terms, and p \to q is their type. You have two terms of the same type.

[Lars Ericson]

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]

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]

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]

Oh good point, thank you!

[Adam Topaz]

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]

@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]

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

[Adam Topaz]

In particular, the by_casesline doesn't seem to buy you anything in this proof.

[Eric Wieser]

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]

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]

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]

Instead of by_contra h4, why not just apply h1?

[Kevin Buzzard]

You're trying to prove r after all, and the conclusion of h1 is r.

[Lars Ericson]

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]

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]

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]

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]

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]

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]

I think of show as being analogous to change in tactic mode. I might be wrong though...

[Bryan Gin-ge Chen]

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]

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]

(p → q) is true if p is false (hp), right?

[Lars Ericson]

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]

No, again, h is a hypothesis about the specific q in your tactic state

[Lars Ericson]

But I'm not seeing forall.introin the docs.

[Ruben Van de Velde]

Try apply h

[Reid Barton]

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

[Reid Barton]

You need to apply h and prove its antecedent p -> q--in tactic mode you can do these in either order

[Lars Ericson]

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]

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

[Ruben Van de Velde]

You could prove p because your assumptions were contradictory, they still are when proving ¬q

[Ruben Van de Velde]

(Alternatively, note that you could also prove p ∧ ¬q that way.)

[Adam Topaz]

Here are a few more hints

open classical

variables {p q : Prop}

example : ¬(p → q) → p ∧ ¬q :=
begin
intro h,
by_cases hp : p,
{ split,
  assumption,
  intro hq,
  apply h,
  sorry },
{ split,
  { exfalso,
    apply h,
    sorry },
  { intro hq,
    apply h,
    sorry }},
end

[Reid Barton]

Given hp : ¬p what can you say about p → q?

[Ruben Van de Velde]

@Adam Topaz

You don't need the second split either :)

[Adam Topaz]

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

[Adam Topaz]

:rofl:

open classical

variables {p q : Prop}

example : ¬(p → q) → p ∧ ¬q :=
λ h, or.rec (λ hp, ⟨hp,λ hq, h $ λ h, hq⟩) (λ hnp, false.elim $ h $ λ hp, false.elim $ hnp hp) (em p)

[Lars Ericson]

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]

@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]

No, it's just applying the assumption hp from the context to prove goal p

[Adam Topaz]

After that, lean moves on to the next goal

[Lars Ericson]

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

[Kevin Buzzard]

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]

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]

@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]

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]

Wouldn't dec_trivial also work?

[Yakov Pechersky]

Because bool is a fintype

[Adam Topaz]

bool != Prop

[Lars Ericson]

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]

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

[Lars Ericson]

@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]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

Classical logic means em or by_cases

[Kevin Buzzard]

It's the by_cases which is out of scope for this one, and this is a famously tricky one.

[Adam Topaz]

@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]

@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]

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]

@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]

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]

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

[Marc Huisinga]

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

[Lars Ericson]

With q=p, this is the Law of the Excluded Middle, so it is out of scope.

[Marc Huisinga]

@Lars Ericson can you prove ¬p in your goal, on paper?

[Bryan Gin-ge Chen]

(end_of_chapter_3 is definitely provable constructively.)

[Lars Ericson]

@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]

can you somehow prove (p → false), i.e. make it available?

[Lars Ericson]

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]

have h : p → false, and then prove it.

[Marc Huisinga]

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]

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]

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]

the first goal requires you to prove h4 : ¬p, whereas the second goal has h4 in its assumptions

[Lars Ericson]

Thanks I get it, I can do an apply here.

[Marc Huisinga]

remember that ¬p = p → false

[Lars Ericson]

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]

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]

You can look up lemma names using library_search.

[Marc Huisinga]

instead of apply, try intro

[Lars Ericson]

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]

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]

Bonus points: make a term-mode proof!

[Yakov Pechersky]

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

[Marc Huisinga]

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]

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

[Kevin Buzzard]

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

[Yakov Pechersky]

I mean, for the two goals of p

[Kevin Buzzard]

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]

Ah, I see, never mind

[Ruben Van de Velde]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

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

[Lars Ericson]

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

[Adam Topaz]

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

[Lars Ericson]

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]

Here's a higher quality mp4
output.mp4

[Adam Topaz]

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]

I use peek (Patrick told me about it).

[Adam Topaz]

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