How to convey the idea of a proof

Stream: new members

[Daniel Fabian]

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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Bryan Gin-ge Chen]

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

[Daniel Fabian]

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]

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

[Daniel Fabian]

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

[Johan Commelin]

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

[Daniel Fabian]

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

ah yes, I like calc of that thing

[Bhavik Mehta]

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

[Daniel Fabian]

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]

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

[Reid Barton]

Well, you can use calc with <->

[Reid Barton]

but then it's a different kind of calc

[Daniel Fabian]

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

[Reid Barton]

Right

[Daniel Fabian]

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

[Patrick Massot]

Implication is not possible, AFAIK

[Johan Commelin]

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

[Reid Barton]

Actually implication in calc does work

[Johan Commelin]

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]

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]

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 :=
calc
  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]

Does this help?

[Mario Carneiro]

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]

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

example {α : Type} (f g : α → α) : α → α :=
calc α → α : f
   ... → α : g

type mismatch at application
  implies.trans
term
  α
has type
  Type : Type 1
but is expected to have type
  Prop : Type