search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

simp and -t syntax #39

Closed PatrickMassot closed 6 years ago

PatrickMassot commented 6 years ago

On line 1245 of https://github.com/leanprover/theorem_proving_in_lean/blob/master/tactics.rst, I read "The simp tactic does not recognize the -t syntax, so to use an identity in the other direction you need to use eq.symm explicitly." I guess this refers to rw [<-equation] syntax, and not rw [-equation]. In addition simp does have a -t syntax meaning: "without lemma t". So I think this sentence is a bit confusing.

PatrickMassot commented 6 years ago

I was looking for something else in the change log when I realized that this issue is relevant only to the nightly version of Lean, not the latest release. What is the strategy here? Do you have released vs nightly versions of TPIL? Or do you start updating TPIL when a new version of Lean is released?

avigad commented 6 years ago

Indeed, we try to keep TPIL up to date with the releases. Use the change log for more recent changes.

PatrickMassot commented 6 years ago

Thank you for your answer. Maybe you could keep the master branch in sync with Lean releases but have a dev branch updated more often? I don't know whether Lean has a formal release policy but it seems to me that a lot happened since Lean 3.3.0. I see two reasons to start this new branch:

I know I'm asking for more work (at least on short term), so let me point out how great I think TPIL is. I'm a regular mathematician with no training in computer science, and I never used a proof assistant before (I very briefly tried Coq last summer, without much success). To me the greatness of Lean relies on:

I know this is an inhomogeneous list (Lean would disapprove) but dropping any item would make Lean unusable by mathematicians. I really love that TPIL does not focus on software certification and does not assume prior knowledge of Haskell or ML (those were the main reasons why I could never read any Coq documentation).

Note also that I'm ready to help with documentation, see e.g. https://github.com/leanprover/mathlib/pull/73, but I don't know much...

avigad commented 6 years ago

@PatrickMassot Thanks very much for the kind words. Updating TPIL involves not just fixing all the code snippets but also reading through all the text and making sure it is correct and coherent. It only makes sense to keep the main version synchronized with the release, but if it will be help to you and others I will make an intermediate pass with the current version and publish it at my own repository. I'll add this task to my to do list. With teaching, upcoming travel, a paper deadline, chairing the ITP conference, etc., I won't be able to do this at the end of April or early May, but I won't forget. (I need to work on the other Lean documentation as well.)

By the way, I am concerned that people contributing to the mathlib project seem to be thinking of Lean as a more finished product than it is. (I have expressed these concerns to Mario.) It is still very much a work in progress. I am happy to hear that you are enjoying the system, but it is still has a long way to go before it is a stable and useful tool, and Leo is still making fundamental changes. In the long run, these will vastly improve the system, and are needed to make the system viable. But in the short run, they will lead to frustration. It makes sense to experiment with Lean now and explore ways of writing definitions and proofs, but please keep in mind that if you build big projects and libraries, you may find yourself spending inordinate amounts of time fixing things when the system changes, as well as coping with bugs and workarounds and wishing for features that just aren't there. Please make sure your expectations are realistic, and plan accordingly...

PatrickMassot commented 6 years ago

Indeed it would be helpful to have an intermediate pass, but there is no hurry. Your documentation efforts really help, and having more tactic writing documentation in Programming in Lean would also be awesome (assuming this is was you refer to in "I need to work on the other Lean documentation as well").

Sebastian Ullrich mentioned https://robpol86.github.io/sphinxcontrib-versioning/ it seems we could have a release version and a current version hosted on the same webpage, with a single link to click to go from one to the other.

I don't think people contributing to mathlib think of Lean as a finished project. First Leo is rather clear in his FAQ and answers to issues or PR. Next, we certainly hope that some things will improve, especially on the automation side of the story. I don't know about people coming from a computer science background, but the handful of traditional mathematicians experimenting with Lean are really experimenting, not building huge long terms projects. I certainly don't have enough time for this, I only use Lean is my spare time, although I hope that proof assistants will become daytime tools for mathematicians in the future.

avigad commented 6 years ago

Thanks! I will try the versioning system. I am pleased by the enthusiasm from the mathematical community, and I appreciate your patience and willingness to experiment.

cipher1024 commented 6 years ago

Just to throw in my two cents, I'm a CS guy and I develop a few large packages in Lean for software verification. Like Patrick, I'm aware that the project is unstable but I'm hoping to come up with interesting examples of how to use Lean and what features are helpful or not helpful and what proving styles need better support. So far, I'm really surprised by how easy it was to develop my own tactic monad. I really like the overall direction of the project and I keep coming back for more :) Being a Haskell fan, this system really struck a chord with me.

In short, I see the constant changes as a reasonable price to pay to be able get ideas in.

Kha commented 6 years ago

@avigad Let me know if I can be of any help here btw.

PatrickMassot commented 6 years ago

@Kha What about releasing Lean 3.4.0? Maybe after making sure this pow stuff isn't blocking anything.

avigad commented 6 years ago

@Kha Thanks. I am happy to do it. Last month was really busy, but things are starting to improve, and I'll have plenty of time in May and June.

Do you think it is important to have a Javascript version of Lean that works with the prerelease documentation? If so, how hard is it to build one?

How would you avoid e.g. correcting the same typos in the main (release) branch and the prerelease branch? Would you destructively update the latter on the former?

Kha commented 6 years ago

Do you think it is important to have a Javascript version of Lean that works with the prerelease documentation? If so, how hard is it to build one?

It would make sense if we want to make sure the "try it!" links keep working. We should probably move to deploying the editor automatically via Travis. Then multiple, continuously updated versions should not be a burden at all.

How would you avoid e.g. correcting the same typos in the main (release) branch and the prerelease branch?

Good question. I think primary development should be based on the master (prerelease) branch. Then we can selectively backport changes to e.g. the 3.3.0 branch via git cherry-pick. It's just a matter of time (and thus divergence) until that breaks down because of merge conflicts (at least until the next stable is released), so we may want to limit it to important fixes like correcting code.

avigad commented 6 years ago

I just addressed the initial issue about simp and TPIL is up to date with Lean 3.4.1. There is still more to do, but I think we can consider this issue closed.

PatrickMassot commented 6 years ago

Thank you! While reviewing the change, I noticed https://github.com/leanprover/theorem_proving_in_lean/blame/master/tactics.rst#L450 is partly outdated: now you can use sorry also in tactic mode.

avigad commented 6 years ago

Thanks. I changed admit to sorry.