Zulip Chat Archive

Stream: new members

Topic: How to convey the idea of a proof

Daniel Fabian (Jun 02 2020 at 16:57):

When developing in idea, I often find it equally if not more important for my partners to have an intuition for how the theory works than the technical details how it's proved.

And I was wondering how you go about making proof intelligible. Specifically how would you go about not bogging down the reader with trivialities but provide enough detail that it's possible follow what's actually going on?

E.g. I certainly don't care that you use the left introduction rule for a disjunction or that you used the iff elimination. But it might be interesting that you show this by functional extensionality, that you use x in a universal quantifier because of a diagonalization argument or that we "show the forward direction using continuity".

I see at least a few various options:

  • just not care, since it's machine-checked, we know it's correct, so we may as well not bother if others understand it
  • break the proofs into lemmas that are somehow semi-meaningful and try to string them together in a way that convey the idea if not the details of the proof.
  • format the proof in some clever way.

A few observations:

  • pure term-level proofs are virtually unintelligible. When I see them, it tells me "don't worry about this; it's true, but you won't learn anything studying it".
  • term-level proofs have no proof state visible in the IDE, so that makes them potentially more difficult to follow than tactic proofs.
  • pure tactic chains are amazing to study the steps in an IDE but are completely meaningless without it.

If you want me to give an #mwe, what would you like to see?

Kevin Buzzard (Jun 02 2020 at 17:02):

What I write in a proof depends on (a) how hard the proof is and (b) who (if anyone) I expect to read the proof. I have made mathlib PRs on basic material like Noetherian rings where I'm setting up a basic API and proving trivialities, and then I try and write super-concise proofs in term mode because these proofs are not written to be read, they're written so that we have an API. On the other hand when I'm writing teaching material for undergraduates I write super-lengthy tactic mode proofs with perhaps more lines of comments than lines of code.

One rule of thumb I tend to use is that if it's mathematically trivial and you're not attempting to teach beginners how the proof works, then why not kill it in as few characters as possible, because nobody cares about the proof.

Bryan Gin-ge Chen (Jun 02 2020 at 17:03):

I don't disagree with your point, but thanks to @Gabriel Ebner , Lean 3.15.0 will display some proof state for term proofs.

Daniel Fabian (Jun 02 2020 at 17:04):

that's amazing to hear @Bryan Gin-ge Chen .

Kevin Buzzard (Jun 02 2020 at 17:04):

Mathlib has some kind of "no comments" policy, for some reason. But if you want to make a proof comprehensible, especially a term mode one, just write lots of comments.

Bryan Gin-ge Chen (Jun 02 2020 at 17:05):

I don't believe there's a no comments policy.

Bryan Gin-ge Chen (Jun 02 2020 at 17:06):

I would certainly be happy to merge comment-only PRs (provided they were correct and enlightening).

Daniel Fabian (Jun 02 2020 at 17:06):

In my concrete case, I've designed a data structure that uses the fact that under certain conditions union and cartesian product commute.

I've captured the conditions in a LaTeX proof and I figured it'd be a fine exercise to translate to Lean.

The results are not trivial, but not hard either. And once you have the intuition, it's really easy to get it. So I was just trying to figure out how to make things understandable.

Johan Commelin (Jun 02 2020 at 17:07):

@Daniel Fabian Tactics like obtain and suffices can also be used to explain the structure of a proof

Daniel Fabian (Jun 02 2020 at 17:07):

(to my co-workers or any potential dev who wants to maintain the datastructure in future)

Johan Commelin (Jun 02 2020 at 17:07):

Also calc, when you fiddle a bit with the layout, can be pretty readable

Daniel Fabian (Jun 02 2020 at 17:08):

@Johan Commelin currently, I tend to put some show / suffices with an explicit type signature at some key points. And then use tactics or terms for things that are boring, like unwrapping definition 2 times or reordering terms.

Daniel Fabian (Jun 02 2020 at 17:09):

ah yes, I like calc of that thing

Bhavik Mehta (Jun 02 2020 at 17:09):

One option which can help sometimes and not many people use is 'french' quotes

Daniel Fabian (Jun 02 2020 at 17:10):

One thing I miss, is a version of calc that doesn't want things to be equal, but allow you to write modified equalities. E.g. a = b ... a - b = 0.

Daniel Fabian (Jun 02 2020 at 17:10):

I'd love that as a chain of calc things, somehow.

Reid Barton (Jun 02 2020 at 17:11):

Well, you can use calc with <->

Reid Barton (Jun 02 2020 at 17:11):

but then it's a different kind of calc

Daniel Fabian (Jun 02 2020 at 17:12):

Oh, you use implication or equivalence as your relation for calc?

Reid Barton (Jun 02 2020 at 17:12):


Daniel Fabian (Jun 02 2020 at 17:12):

I didn't realise this was possible, thanks, learnt something new.

Patrick Massot (Jun 02 2020 at 17:16):

Implication is not possible, AFAIK

Johan Commelin (Jun 02 2020 at 17:22):

@Daniel Fabian But < and are. (And you can even mix them (and =).

Reid Barton (Jun 02 2020 at 17:24):

Actually implication in calc does work

Johan Commelin (Jun 02 2020 at 17:24):

With obtain I meant the pattern

  obtain \<x, hx\> : \exists x, is_cool x,
  { hammer, tauto },
  -- Now you have (x : X) and (hx : is_cool x) in your context

Patrick Massot (Jun 02 2020 at 17:29):

Oh nice, I misremembered then. This is silly because I think I convinced myself it didn't work a very very long time ago.

Patrick Massot (Jun 02 2020 at 17:34):

I remember what doesn't work:

example (p q r s t : Prop) (h : p  q) (h' : q  r) (h'' : r  s) (h3 : s  t): p  t :=
  p  q : h
...  r : h'
...  s : h''
...  t : h3

If I remember correctly, we can't add the transitivity rule that is missing.

Reid Barton (Jun 02 2020 at 17:36):

Does this help?

Mario Carneiro (Jun 02 2020 at 17:40):

After writing that I realized that this is exactly the reason why it is done: it gives a place for implies.trans to live

Mario Carneiro (Jun 02 2020 at 17:43):

although because implies is less general than nondependent_pi, you get this error:

example {α : Type} (f g : α  α) : α  α :=
calc α  α : f
   ...  α : g
type mismatch at application
has type
  Type : Type 1
but is expected to have type
  Prop : Type

Last updated: Dec 20 2023 at 11:08 UTC