I've only ever learnt Agda, and I feel like I should learn another popular proof assistant, but I can never understand the proofs that are made in other proof assistants. I suppose the point is not to understand but to trust that the compiler has checked it? The fact that Agda has barely any tactics means that at the end of the proof, you're left with a very readable program.
For example, the proof that 2 is prime from the post:
theorem prime_two : prime 2 := by
simp
intros k x
simp [divides] at x
have ⟨q,hq⟩ := x
(cases q <;> cases k <;> grind)
I can understand the Agda proof by looking up what the requirements of the field gt1 and div are, then I can understand what the available arguments represent and what we're supposed to return as the return value of the function. But in the Lean proof, I have no clue what it's doing; what's the first simp for, what's grind actually doing? I can't translate the proof into mathematical terms, which I personally find annoying.
Yeah, this is an example of what you might call “proof language paradigms” which I am sure has been written about somewhere although I don’t know of it. But basically with the proof languages we’ve developed so far there’s a tradeoff between how easy a proof is to write and how easy a proof is to read. The more declarative your proof is the more it looks like a real informal proof that you can read & follow, but also it seems much more difficult to understand why the prover is getting stuck while you are writing the proof.
TLA+ has a proof sub-language that is the most extreme example of declarative proofs I am aware of; you don’t get very much help when figuring out why discharging an obligation failed. However, the proofs are quite readable (as long as you collapse some of the longer nested child proofs). The TLA+ proof language has no support for tactics whatsoever.
Contrast this with Lean where proofs comprise a series of operations that directly manipulate the current assumption & goal states, often in an automated way using tactics. It is very easy to see why a proof obligation cannot be discharged while writing it, but it is impossible to read the proof without stepping through it in a Lean development environment.
ettolrach | an hour ago
I've only ever learnt Agda, and I feel like I should learn another popular proof assistant, but I can never understand the proofs that are made in other proof assistants. I suppose the point is not to understand but to trust that the compiler has checked it? The fact that Agda has barely any tactics means that at the end of the proof, you're left with a very readable program.
For example, the proof that 2 is prime from the post:
versus
I can understand the Agda proof by looking up what the requirements of the field
gt1anddivare, then I can understand what the available arguments represent and what we're supposed to return as the return value of the function. But in the Lean proof, I have no clue what it's doing; what's the firstsimpfor, what'sgrindactually doing? I can't translate the proof into mathematical terms, which I personally find annoying.ahelwer | an hour ago
Yeah, this is an example of what you might call “proof language paradigms” which I am sure has been written about somewhere although I don’t know of it. But basically with the proof languages we’ve developed so far there’s a tradeoff between how easy a proof is to write and how easy a proof is to read. The more declarative your proof is the more it looks like a real informal proof that you can read & follow, but also it seems much more difficult to understand why the prover is getting stuck while you are writing the proof.
TLA+ has a proof sub-language that is the most extreme example of declarative proofs I am aware of; you don’t get very much help when figuring out why discharging an obligation failed. However, the proofs are quite readable (as long as you collapse some of the longer nested child proofs). The TLA+ proof language has no support for tactics whatsoever.
Contrast this with Lean where proofs comprise a series of operations that directly manipulate the current assumption & goal states, often in an automated way using tactics. It is very easy to see why a proof obligation cannot be discharged while writing it, but it is impossible to read the proof without stepping through it in a Lean development environment.