As far as theorem provers go Coq seems to be the most widely known among working programmers.
Lean deserves wide recognition. First, it's fast enough for highly interactive theorem development. Second it can also be used as a programming language. And lastly its syntax is pleasant to work with which is important to the experience.
If you have only heard about interactive theorem provers and don't yet have any opinions I'd give Lean a try first. The interactive tutorials are nice and the aforementioned features make it pleasant to work with.
These are interesting pros for lean. I just wanted to point out that Coq is also a programming language, and there are some packages of hackage of various data structures proven correct in Coq and then compiled from the original coq sources.
Strongly agree. I only found Lean after a couple of weeks of struggling to pick up coq. In my opinion, this tutorial alone makes lean a better choice for beginners.
Out of interest, what about this tutorial do you find better than (which?) Coq tutorials?
I think Lean might be the better technology, but I don't think this tutorial is better than Software Foundations. I can't see beginners not being turned off by boring discussions of hierarchies of universes before the first real proofs to get you hooked.
This tutorial starts by explaining how things work, and only later shows you magic. That's exactly what I like about it, actually. Almost every coq tutorial I found (I tried software foundations, cpdt, and several shorter online tutorials) fails to explain what you're doing before you do it.
Obligatory mention to `coq` and `Software foundations`(SF).
`coq` is an amazing piece of software. SF makes you start prooving thing right from chapter one. Learn mathematics by doing. After going through the chapters of Logic Foundations I'm able to see the patterns in most mathematicals proof I come by.
Must read book if you want to acquire mathematical superpowers.
Coq tells you when you are wrong, but it doesn't provide you the solution either. So you have to work it up for yourself. The satisfaction of finding a proof and knowing it is right is hard to match( this is known as the video-game-effect). You'll even be able to spot slopy proof in text books.
One should also mention Isabelle/HOL [1] and Concrete Semantics
[2]. As of May 2018, Isabelle/HOL has the best proof automation, in case you want to get things done.
True. It is worth pointing out that Isabelle/HOL does not have dependent types in its underlying logic making framework building a (much?) harder work.
I've got very little experience with theorem provers, but I have spent some time working through this book, and I can recommend it. If you're interested, the Emacs Lean mode works great.
Was there a reason for the move away from HoTT? I seem to recall looking this up a while ago but didn't find a solid answer. Was there a fork version 2 that continues development with HoTT?
Though, given then above linked discussion, I expect that never to become officially supported. But who knows, I don't think Lean 2 started life intending to handle HoTT either.
That is also true, but its proof is different. Proofs have types; the "and.intro hq hp" part has type "q /\ p". If you change it to "and.intro hp hp", you can prove "p /\ p". That is, the following works:
theorem and_commutative (p q : Prop) : p ∧ q → p ∧ p :=
assume hpq : p ∧ q,
have hp : p, from and.left hpq,
have hq : q, from and.right hpq,
show p ∧ p, from and.intro hp hp
(and then you should rename it from "and_commutative" to something else, and you can remove the "hq" line)
"intros [HP HQ]" separates the two conjuncts of the hypothesis into separate hypotheses (P, and Q); "split" breaks the goal (Q ∧ P) into two subgoals (Q, and P), and the two applications prove the two subgoals.
It could also be written:
Theorem and_commutative_2 (P Q : Prop) : P ∧ Q → Q ∧ P.
Proof. tauto. Qed.
...as the proof tactic "tauto" is capable of proving this (simple) theorem immediately.
Cool, thanks for this. I've yet to play with Lean, but it looks very interesting! (I'm hoping that my time invested in Coq will transfer reasonably well...)
You're welcome! I'm in a similar boat, coming to this tutorial from a Coq background (and some Isabelle/HOL). I'm pleasantly surprised how similar many things are. But I'm also a bit disappointed because I was under the impression that Lean was relying on automation via Z3 a lot more. Not quite done with the tutorial yet, so there might still be some material to this effect coming up, but I'm afraid not.
Look up the words Dynamic Invariant Generation. Uses examples or test data. There's also machine learning techniques for pulling the specs out of combos of input and output. Human still has to check them for correctness. I have seen folks use automated proof or test generation to reality check them, though.
Lean deserves wide recognition. First, it's fast enough for highly interactive theorem development. Second it can also be used as a programming language. And lastly its syntax is pleasant to work with which is important to the experience.
If you have only heard about interactive theorem provers and don't yet have any opinions I'd give Lean a try first. The interactive tutorials are nice and the aforementioned features make it pleasant to work with.