Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 21 2020 at 18:17):

docs#not_and_distrib or something like that...

view this post on Zulip Adam Topaz (Nov 21 2020 at 18:17):

So you can rw not_and_distrib at h

view this post on Zulip Adam Topaz (Nov 21 2020 at 18:18):

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

view this post on Zulip Adam Topaz (Nov 21 2020 at 18:18):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 21 2020 at 19:40):

by_contra and by_cases are tactics.

view this post on Zulip Adam Topaz (Nov 21 2020 at 19:41):

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

view this post on Zulip Adam Topaz (Nov 21 2020 at 19:42):

(Although that page contains some tactics from mathlib)

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 21 2020 at 19:44):

by_cases h1 : p \to q

view this post on Zulip Adam Topaz (Nov 21 2020 at 19:46):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Lars Ericson (Nov 21 2020 at 19:52):

Oh good point, thank you!

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 21 2020 at 20:00):

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

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 20:39):

Instead of by_contra h4, why not just apply h1?

view this post on Zulip Kevin Buzzard (Nov 21 2020 at 20:39):

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

view this post on Zulip 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

view this post on Zulip 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 232^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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ruben Van de Velde (Nov 21 2020 at 21:10):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Nov 21 2020 at 21:14):

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

view this post on Zulip Lars Ericson (Nov 21 2020 at 21:15):

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

view this post on Zulip Ruben Van de Velde (Nov 21 2020 at 21:15):

Try apply h

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ruben Van de Velde (Nov 21 2020 at 21:28):

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

view this post on Zulip Adam Topaz (Nov 21 2020 at 21:29):

Here are a few more hints

view this post on Zulip Reid Barton (Nov 21 2020 at 21:30):

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

view this post on Zulip Ruben Van de Velde (Nov 21 2020 at 21:36):

@Adam Topaz

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Nov 21 2020 at 21:42):

:rofl:

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Nov 21 2020 at 21:56):

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

view this post on Zulip Adam Topaz (Nov 21 2020 at 21:57):

After that, lean moves on to the next goal

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:11):

Wouldn't dec_trivial also work?

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:11):

Because bool is a fintype

view this post on Zulip Adam Topaz (Nov 22 2020 at 16:14):

bool != Prop

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:32):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:36):

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

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:37):

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

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:37):

Classical logic means em or by_cases

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 18:07):

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

view this post on Zulip Marc Huisinga (Nov 22 2020 at 18:08):

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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Nov 22 2020 at 18:09):

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

view this post on Zulip Bryan Gin-ge Chen (Nov 22 2020 at 18:10):

(end_of_chapter_3 is definitely provable constructively.)

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Nov 22 2020 at 18:12):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 18:16):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Lars Ericson (Nov 22 2020 at 18:25):

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

view this post on Zulip Marc Huisinga (Nov 22 2020 at 18:27):

remember that ¬p = p → false

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 18:33):

You can look up lemma names using library_search.

view this post on Zulip Marc Huisinga (Nov 22 2020 at 18:34):

instead of apply, try intro

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 22 2020 at 18:52):

Bonus points: make a term-mode proof!

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 18:52):

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

view this post on Zulip 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

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 19:02):

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

view this post on Zulip 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.

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 19:03):

I mean, for the two goals of p

view this post on Zulip 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).

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 19:05):

Ah, I see, never mind

view this post on Zulip 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

view this post on Zulip Marc Huisinga (Nov 22 2020 at 19:10):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 :)

view this post on Zulip 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

view this post on Zulip Adam Topaz (Nov 22 2020 at 20:35):

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

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Nov 22 2020 at 21:37):

Here's a higher quality mp4
output.mp4

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 21:50):

I use peek (Patrick told me about it).

view this post on Zulip 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