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.
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.
There’s a fairly active community over on Zulip [1] if you like to drop by for a chat or get some help.
`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.
Unfortunately I can't seem to get the live compiler to work properly. I get this message when I check the JS console:
Failed to execute 'postMessage' on 'DedicatedWorkerGlobalScope': DOMException object could not be cloned.
There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3
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.
show p ∧ q
show p ∧ p
I guess I better start reading the tutorials ...
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
Theorem and_commutative (P Q : Prop) : P ∧ Q → Q ∧ P.
Proof.
intros [HP HQ].
split.
- apply HQ.
- apply HP.
Qed.
It could also be written:
Theorem and_commutative_2 (P Q : Prop) : P ∧ Q → Q ∧ P.
Proof. tauto. Qed.