6 ms·

Theorem Proving in Lean

156 points by benwr 8y ago

aban 8y ago
An Introduction to Lean [0] is another nice (albeit incomplete) tutorial. There’s a fairly active community over on Zulip [1] if you like to drop by for a chat or get some help. [0]: https://leanprover.github.io/introduction_to_lean/ https://leanprover.github.io/introduction_to_lean/ [1]: https://leanprover.zulipchat.com https://leanprover.zulipchat.com
agentultra 8y ago
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.
- benwr 8y ago
  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.
  - tom_mellior 8y ago
    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.
    - benwr 8y ago
      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.
      - tom_mellior 8y ago
        Fair enough. That's not my preferred approach to tutorials, but tastes differ. Thanks.
- tathougies 8y ago
  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.
  - agentultra 8y ago
    I have read a fair bit about use of hs-to-coq and coq-haskell; Coq is a nice tool for sure!
- elcapitan 8y ago
  What's the upside compared to coq?
4rgento 8y ago
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. [0]https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/
qwerty456127 8y ago
Is there something like this that can use a real data set to validate all the statements against instead of a set of hand-written formal assumptions?
- nickpsecurity 8y ago
  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.
- alimw 8y ago
  Do you maybe want a database integrated with a good logic programming language? Datomic/Datalog springs to mind.
robinhoode 8y ago
This seems really cool! 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.
- benwr 8y ago
  This problem went away for me when I turned off my ad blocker.
tmpmov 8y ago
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?
- im_down_w_otp 8y ago
  This was a discussion I remember coming across not long ago when I had the same question: https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIzM https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIz... There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3 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.
logicchains 8y ago
Interesting note: a new version, Lean 4, is currently under development, which will presumably replace Lean 3 once complete: https://github.com/leanprover/lean/blob/master/doc/lean4.md https://github.com/leanprover/lean/blob/master/doc/lean4.md.
amelius 8y ago
Hmm, in the example, I tried to change show p ∧ q into show p ∧ p (which should also be true). But it gives a type error. I guess I better start reading the tutorials ...
- tom_mellior 8y ago
  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)
  - gmfawcett 8y ago
    Just for the sake of comparison, the same proof in Coq might be written: Theorem and_commutative (P Q : Prop) : P ∧ Q → Q ∧ P. Proof. intros [HP HQ]. split. - apply HQ. - apply HP. Qed. "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.
    - tom_mellior 8y ago
      There are tons of other ways of writing the same thing in Lean too, of course. Here is one: theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := begin intros, simp * end https://leanprover.github.io/live/3.4.1/#code=theorem%20and_commutative%20(p%20q%20:%20Prop)%20:%20p%20%E2%88%A7%20q%20%E2%86%92%20q%20%E2%88%A7%20p%20:=%0Abegin%20intros,%20simp%20*%20end https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...
YorkshireSeason 8y ago
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. [1] https://isabelle.in.tum.de/ https://isabelle.in.tum.de/
- unboxed_type 8y ago
  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.
  - YorkshireSeason 8y ago
    I'm not sure what you mean by "framework building" in this context.
- YorkshireSeason 8y ago
  Whoops, forgot to link to _Concrete Semantics_. [2] http://www.concrete-semantics.org http://www.concrete-semantics.org
sevensor 8y ago
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.

156 points by benwr 8y ago

aban 8y ago

An Introduction to Lean [0] is another nice (albeit incomplete) tutorial. There’s a fairly active community over on Zulip [1] if you like to drop by for a chat or get some help. [0]: https://leanprover.github.io/introduction_to_lean/ https://leanprover.github.io/introduction_to_lean/ [1]: https://leanprover.zulipchat.com https://leanprover.zulipchat.com

agentultra 8y ago

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.

benwr 8y ago
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.
- tom_mellior 8y ago
  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.
  - benwr 8y ago
    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.
    - tom_mellior 8y ago
      Fair enough. That's not my preferred approach to tutorials, but tastes differ. Thanks.
tathougies 8y ago
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.
- agentultra 8y ago
  I have read a fair bit about use of hs-to-coq and coq-haskell; Coq is a nice tool for sure!
elcapitan 8y ago
What's the upside compared to coq?

4rgento 8y ago

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. [0]https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/

qwerty456127 8y ago

Is there something like this that can use a real data set to validate all the statements against instead of a set of hand-written formal assumptions?

nickpsecurity 8y ago
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.
alimw 8y ago
Do you maybe want a database integrated with a good logic programming language? Datomic/Datalog springs to mind.

robinhoode 8y ago

This seems really cool! 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.

benwr 8y ago
This problem went away for me when I turned off my ad blocker.

tmpmov 8y ago

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?

im_down_w_otp 8y ago
This was a discussion I remember coming across not long ago when I had the same question: https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIzM https://groups.google.com/forum/#!topic/lean-user/VA71gT5nIz... There's a somewhat active integration of HoTT into Lean 3 ongoing here: https://github.com/gebner/hott3 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.

logicchains 8y ago

Interesting note: a new version, Lean 4, is currently under development, which will presumably replace Lean 3 once complete: https://github.com/leanprover/lean/blob/master/doc/lean4.md https://github.com/leanprover/lean/blob/master/doc/lean4.md.

amelius 8y ago

Hmm, in the example, I tried to change show p ∧ q into show p ∧ p (which should also be true). But it gives a type error. I guess I better start reading the tutorials ...

tom_mellior 8y ago
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)
- gmfawcett 8y ago
  Just for the sake of comparison, the same proof in Coq might be written: Theorem and_commutative (P Q : Prop) : P ∧ Q → Q ∧ P. Proof. intros [HP HQ]. split. - apply HQ. - apply HP. Qed. "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.
  - tom_mellior 8y ago
    There are tons of other ways of writing the same thing in Lean too, of course. Here is one: theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := begin intros, simp * end https://leanprover.github.io/live/3.4.1/#code=theorem%20and_commutative%20(p%20q%20:%20Prop)%20:%20p%20%E2%88%A7%20q%20%E2%86%92%20q%20%E2%88%A7%20p%20:=%0Abegin%20intros,%20simp%20*%20end https://leanprover.github.io/live/3.4.1/#code=theorem%20and_...

YorkshireSeason 8y ago

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. [1] https://isabelle.in.tum.de/ https://isabelle.in.tum.de/

unboxed_type 8y ago
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.
- YorkshireSeason 8y ago
  I'm not sure what you mean by "framework building" in this context.
YorkshireSeason 8y ago
Whoops, forgot to link to _Concrete Semantics_. [2] http://www.concrete-semantics.org http://www.concrete-semantics.org

sevensor 8y ago

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.