4 proof styles

Stream: new members

[Utensil Song]

I, very new to Lean and this Zulip Chat Community, would like to share my experience with Lean prover on trying to prove a trivial proposition in four proof styles supported by Lean. It's gonna feel verbose(for describing the intuition I established during the interactions with Lean), for that, I apologize in advance.

The proposition is from 3.3.3. Negation and Falsity, Theorem Proving in Lean (which is where I'm at in the walkthrough of TPIL:

For any two propositions p and q, assuming p → q and ¬q, Then ¬p.

TPIL expresses the proposition like this:

constants p q: Prop
example (hpq : p → q) (hnq : ¬q) : ¬p := sorry

As a beginner in Lean, I find it particularly important to be able to move things around and transform between different appearances of the same thing in one's mind, since the expressive Lean gives us too much liberty at how to express the same idea. Just move them around in the code editor (for me that's VSCode with Lean extension installed) and check the result against Lean. From these muscle memories (of success or errors), a mental model grows out naturally.

Since example is just a nameless theorem/lemma, we can rewrite the above to the following by naming it play:

lemma play (hpq : p → q) (hnq : ¬q) : ¬p := sorry

Benefit from Curry–Howard correspondence, theorem/lemma shares the same basic grammar structure as def, i.e. def name : type := value, so the above is no different from:

-- Play with `hpq` and `hnq` directly
def play₁ (hpq : p → q) (hnq : ¬q) : ¬p := play hpq hnq

Also, "parameters" are just syntax sugar in Lean, so the above is also the same as:

-- Need Lambda to introduce binding names with the type
def play₂ : (p → q) → (¬q) → ¬p :=  λ hpq, λ hnq, play hpq hnq

Structural Proof

OK, now we can move types, parameters around, let's go back to the original proposition, TPIL demonstrates a structural proof for it:

example (hpq : p → q) (hnq : ¬q) : ¬p :=
assume hp : p,
show false, from hnq (hpq hp)

I failed to wrap my head around it until I read it carefully again and noticed ¬p is equivalent to p → false, so the idea is to assume p and prove false. This is accomplished by applying p → q and then q → false(¬q).

Tactic Mode proof

Next thing I try is to convert it to a Tactic Mode proof(which is best supported by the VS Code extension but hard to read without it), starting with:

example (hpq : p → q) (hnq : ¬q) : ¬p :=
begin
sorry
end

The goal (when the cursor is after begin) is

p q : Prop,
hpq : p → q,
hnq : ¬q
⊢ ¬p

By realizing intro will convert a goal like ⊢ a → b to ha : a ⊢ b and again ¬p is equivalent to p → false, inputting intro hp, we have the following goal(when the cursor is after the comma):

p q : Prop,
hpq : p → q,
hnq : ¬q,
hp : p
⊢ false

apply is the opposite of intro (in a way), it can turn a goal likeb into a by a hypothesis a → b. Basically, it's just a function application(applying a function of the type a → b), while intro is actually a lambda that creates such a function. That's why I accepted the commas (instead of semicolons or nothing) at the end of each line of a proof, it's the same as the one in λ a : ℕ, a + 1.

So assuming we have a → b, when we want to leave b as our goal, we use intro, when we want to leave a as our goal, we use apply. A pretty straight forward, left-hand-or-right-hand choice.

So we work our way backwards: apply q → false to get q, apply p → q to get p, then we have the proof as:

example (hpq : p → q) (hnq : ¬q) : ¬p :=
begin
intro hp,
apply hnq,
apply hpq,
sorry
end

and the goal (before sorry) as:

p q : Prop,
hpq : p → q,
hnq : ¬q,
hp : p
⊢ p

And this goal is exactly our initial assumption hp : p so we finish the proof by exact hp.

A Tactic Mode proof is really relying on the interactive hints of the current goals. While the writing process is enjoyable, the written code is hard to read. By narrowing my mind to the current goal during writing, I can't tell what's going on if I step back and look at the whole proof:

example (hpq : p → q) (hnq : ¬q) : ¬p :=
begin
intro hp,
apply hnq,
apply hpq,
exact hp
end

Term Mode proof

To truly understand the whole Tactic Mode proof, we must completely forget tactics and focus on the commas and replace all intro with a λ, replace all applys as function calls while the exact is the ultimate parameter so we see a Term Mode proof:

example (hpq : p → q) (hnq : q → false) : p → false :=
λ hp, hnq (hpq hp)

Writing a Term Mode proof can use a similar degree of help in VS Code, by prompting types instead of prompting goals:

When we write λ hp, and type a random identifier such as p, Lean will complain about "type mismatch" and we'll know the right type and simply call a function with the expected type (recall that p → q is a hypothesis and also a function that eats something with type p and emits something with type q). Now the game switched from fulfilling goals to filling parameters of functions, type theory in action is fun!

Calc Mode proof

Finally, to my favourite Calc mode. I like it very much since it resembles the experience of pen and paper calculation/proof. Not completely, since we can't do something to both the left-hand side and right-hand side.

To use the Calc Mode proof, we need something like an equation. ¬p is not one but p → false is:

example (hpq : p → q) (hnq : q → false) : p → false := sorry

I'm a bit nervous when I typed calc and see nothing back from Lean. But then I try to forget the computer and start writing on the imaginary paper:

example (hpq : p → q) (hnq : q → false) : p → false :=
calc p → q       : sorry
...    → false   : sorry

Now my brain is doing all the thinking and I only have to find the computer excuse names back to replace the sorrys. It's surprisingly easy:

example (hpq : p → q) (hnq : q → false) : p → false :=
calc p → q       : hpq
...    → false   : hnq

The excuse names(hypothesis) themselves are pretty dumb and you only feel like applying rewrite rules when your cursor is on a hypothesis and Lean shows you its type. To entertain myself a bit, I rewrite the above to:

example (p_to_q : p → q) (q_to_false : q → false) : p → false :=
calc p → q       : p_to_q
...    → false   : q_to_false

Back to Structural Proof

When I first see the structural proof, I thought it means to prove ¬p, simply assume p and it leads to a contradiction, but it's not the logic of that proof, so with a little search, I wrote:

example (hpq : p → q) (hnq : ¬q) : ¬p :=
by_contradiction
(assume hnnp : ¬¬p,
have hp : p, from sorry,
have hq : q, from sorry,
show false, from sorry)

Writing a structural proof is a bit like writing a Calc Mode proof, we do it by first assume, then write down the intermediate steps using haves and end it with a final show of the final target. Then we work out things after , from, just like how we work out what's after the colons in a Calc Mode proof:

open classical

example (hpq : p → q) (hnq : ¬q) : ¬p :=
by_contradiction
(assume hnnp : ¬¬p,
have hp : p, from by_contradiction hnnp,
have hq : q, from hpq hp,
show false, from hnq hq)

Conclusion

It's really a trivial proposition and only very elementary keywords are involved in the proofs, but I'm so excited about being able to write all four styles of proofs and finding out how I feel about each of them. Open questions are:

• Am I missing something or there's little pedagogical material on writing non-trivial proofs using all four styles?
• Are there automatic tools to convert the four styles to each other? ( Is it always possible?)
• Is there on-going efforts to resemble more of the pen-and-paper experience(e.g. manipulate both sides of an equation)?

[Reid Barton]

Have you thought about writing a blog or something? I really like your style of explaining and exploring.

[Jalex Stark]

I agree, this would be a nice blog post.

Every proof compiles down to terms, and in fact after this

lemma contrapositive (hpq : p → q) (hnq : ¬q) : ¬p :=
begin
intro hp,
apply hnq,
apply hpq,
exact hp
end

you can type #print contrapositive to see what term is generated.

[Jalex Stark]

you might enjoy writing up a solution to this codewars kata
https://www.codewars.com/kata/5eb0ce255179590016d613ce

[Kevin Buzzard]

@Utensil Song you'd be welcome to write a guest Xena project blog post based on your post

[Utensil Song]

@Reid Barton Thank you! I wasn't sure if it's worth blogging but so excited to share it. I'm so glad you guys like it and will try to enrich it a bit and write a blog based on it.

[Utensil Song]

Jalex Stark said:

I agree, this would be a nice blog post.

Every proof compiles down to terms, and in fact after this

lemma contrapositive (hpq : p → q) (hnq : ¬q) : ¬p :=
begin
intro hp,
apply hnq,
apply hpq,
exact hp
end

you can type #print contrapositive to see what term is generated.

Thank you! It turns out that underlyingly they are not using the same terms, unlike in my mental model after writing this post:

lemma contrapositive_structural (hpq : p → q) (hnq : ¬q) : ¬p :=
assume hp : p,
show false, from hnq (hpq hp)

#print contrapositive_structural
-- theorem chap_03.contrapositive_structural : ∀ (p q : Prop), (p → q) → ¬q → ¬p :=
-- λ (p q : Prop) (hpq : p → q) (hnq : ¬q) (hp : p), show false, from hnq (hpq hp)

lemma contrapositive_tactic (hpq : p → q) (hnq : ¬q) : ¬p :=
begin
intro hp,
apply hnq,
apply hpq,
exact hp
end

#print contrapositive_tactic
-- theorem chap_03.contrapositive_tactic : ∀ (p q : Prop), (p → q) → ¬q → ¬p :=
-- λ (p q : Prop) (hpq : p → q) (hnq : ¬q), id (λ (hp : p), hnq (hpq hp))

lemma contrapositive_term (hpq : p → q) (hnq : q → false) : p → false :=
λ hp, hnq (hpq hp)

#print contrapositive_term
-- theorem chap_03.contrapositive_term : ∀ (p q : Prop), (p → q) → (q → false) → p → false :=
-- λ (p q : Prop) (hpq : p → q) (hnq : q → false) (hp : p), hnq (hpq hp)

lemma contrapositive_calc (hpq : p → q) (hnq : q → false) : p → false :=
calc p → q       : hpq
...    → false   : hnq

#print contrapositive_calc
-- theorem chap_03.contrapositive_calc : ∀ (p q : Prop), (p → q) → (q → false) → p → false :=
-- λ (p q : Prop) (hpq : p → q) (hnq : q → false), implies.trans hpq hnq

[Utensil Song]

Jalex Stark you might enjoy writing up a solution to this codewars kata
https://www.codewars.com/kata/5eb0ce255179590016d613ce

Fun! Like a tango:

theorem not_not_not_tactic
  (P : Prop) :
  ¬ ¬ ¬ P → ¬ P :=
begin
intro hnnnp,
intro hp,
apply hnnnp,
intro hnp,
apply hnp,
apply hp
end

[Jalex Stark]

Yeah :)

[Jalex Stark]

If you solve enough kata on codewars, you'll be able to submit your own

[Jalex Stark]

I submitted that one a few weeks ago, after having solved ~15 problems

[Utensil Song]

On the other hand, working out the other three styles are not that easy:

theorem not_not_not_term
  (P : Prop) :
  ¬ ¬ ¬ P → ¬ P :=
λ hnnnp hp, hnnnp (λ hnp, hnp hp)

theorem not_not_not_calc
  (P : Prop) :
  ¬ ¬ ¬ P → ¬ P :=
calc ¬ ¬ ¬ P → ¬ P : iff.elim_left (not_not_not_iff P)

theorem not_not_not_structural
  (P : Prop) :
  ¬ ¬ ¬ P → ¬ P :=
assume hnnnp : ¬¬¬P,
assume hp : P,
have hnnp : ¬¬P, from (assume hnp: ¬P, hnp hp), -- from not_not_intro hp,
show false, from hnnnp hnnp

I don't know if not_not_not_calc can be reduced to more atomic steps.

[Jalex Stark]

yeah your "calc" proof is really just "I found this in the library"

[Utensil Song]

Kevin Buzzard said:

Utensil Song you'd be welcome to write a guest Xena project blog post based on your post

Thank you! But I couldn't figure out how to post a guest Xena project blog after reading https://xenaproject.wordpress.com/ , http://wwwf.imperial.ac.uk/~buzzard/xena/UROP2020.html and https://github.com/kbuzzard/xena . Does it mean I simply create a new Github repo, add a .lean and a .md then it's published (I guess not)?

[Jalex Stark]

my guess is that kevin meant that you could give him the text of a blog, he would lightly edit and then post it for you

[Jalex Stark]

this is what most bloggers mean by guest post, I think

[Utensil Song]

Oh I see, thanks!

[Utensil Song]

Jalex Stark said:

yeah your "calc" proof is really just "I found this in the library"

So far I can only reduce it to:

theorem not_not' (P : Prop) : ¬ (¬ P) → P :=
begin
  cases (classical.em P) with hp hnp,
  {
    intro hnnp,
    exact hp,
  },
  {
    intro hnnp,
    exfalso,
    apply hnnp,
    exact hnp
  }
end

theorem not_not_not_calc
  (P : Prop) :
  ¬ ¬ ¬ P → ¬ P :=
calc ¬ ¬ ¬ P  → ¬ P : not_not' (¬ P)

[Jalex Stark]

my best guess is that you would have more fun moving on from here and doing more math (or thinking more about the presentation, if you're trying to make a blog post)

[Jalex Stark]

you extracted almost as much pedagogical material as there is in those two examples

[Utensil Song]

My current goal is to formalize Real Spinorial Groups ( https://www.amazon.com/Real-Spinorial-Groups-Mathematical-SpringerBriefs-ebook/dp/B07QPPTK7B ) in Lean . There's a long way to go from here.

[Jalex Stark]

cool! I remember someone saying something about lie groups recently, if you use the search functionality you may find it

[Utensil Song]

The motivation of this post is mostly that I wonder the pros and cons of these four styles and how to best combine their strength after I read quite a few proofs in Mathlib and Zulip .

[Jalex Stark]

I think the easiest way to make progress on that question is to write a bunch of a proofs :slight_smile:

[Utensil Song]

Yes, I noticed that topic and the not-yet-PRed progress on manifold.

[Utensil Song]

Utensil Song said:

Kevin Buzzard said:

Utensil Song you'd be welcome to write a guest Xena project blog post based on your post

Thank you! But I couldn't figure out how to post a guest Xena project blog after reading https://xenaproject.wordpress.com/ , http://wwwf.imperial.ac.uk/~buzzard/xena/UROP2020.html and https://github.com/kbuzzard/xena . Does it mean I simply create a new Github repo, add a .lean and a .md then it's published (I guess not)?

Just joined the Discord.

[Utensil Song]

Just an update:

moving on from these trivial proposition as @Jalex Stark suggested makes me noticed many new elements of interacting with Lean. I would like to do a due survey of different tutorials already available before I actually turn this into a blog post. Specifically I want to make sure I know my target audience and the expectation (the tone in my original post is very unstable, and detail levels are varying, that's part of the reason). My personal motivation of such an enriched blog would be describing the subtle reactions/feeling/expectation/struggling when one first start interacting with Lean (I might lose the touch very quickly when I learn more about Lean).

When self studying I find it very helpful to read multiple literature simultaneously to have a multi-dimensional perspective (since one such literature has to choose a linear path to organize the materials and facilitate the recognition process). What I've learned so far is a mixture of The Hitchhiker’s Guide to Logical Verification (noticed from https://lean-forward.github.io/ , skimmed in one night, the very reason I started learning Lean), TPIL (doing walkthrough and experimenting) and Logic and Proof(Had to read it in full to deal with exercises from Ch. 3 of TPIL with a clear understanding of the machinery involved) and this Zulip chat. But I haven't tried the games (N, R, Group) and the tutorial as well as mathematics_in_lean.

[Jalex Stark]

I think the thing you already wrote is pretty much ready to be a blog post, and I think the main reason it's exciting is that it gives insight into the very beginning of the process of learning Lean

[Jalex Stark]

you should definitely keep learning Lean, and definitely keep writing about it if you want

[Jalex Stark]

but the writing you already produced is valuable and "updating it" with more of a literature search might be a mistake

[Utensil Song]

Jalex Stark said:

but the writing you already produced is valuable and "updating it" with more of a literature search might be a mistake

Yeah I get that and will try not to pollute it with the update

[Utensil Song]

Anyway, I put the source of the original post at https://github.com/utensil/lean-playground/blob/master/posts/four_proof_styles.md for the time being.