Zulip Chat Archive

Stream: new members

Topic: Lean vs Dafny: Why can't I just put a bunch of assertions...


view this post on Zulip Huỳnh Trần Khanh (Feb 01 2021 at 14:53):

In Dafny induction is easy: just use recursion. And most of the time the inbuilt SMT solver proves the lemma automatically. If for some reason the SMT solver can't find a proof, I can still add more assert statements to guide the solver. It seems that in Lean I have to do everything explicitly, sure there is simp, omega and ring but I have to explicitly invoke those solvers. It may seem weird to ask this question but is this an intentional design choice of Lean? And why was that choice made?

view this post on Zulip Huỳnh Trần Khanh (Feb 01 2021 at 14:54):

And also there is no SMT solver integration in Lean right?

view this post on Zulip Johan Commelin (Feb 01 2021 at 14:59):

I don't know Dafny, but what kind of lemmas can you prove in Dafny? Can you state theorems like the sum 1++n=n(n+1)/21 + \dots + n = n(n+1)/2?

view this post on Zulip Huỳnh Trần Khanh (Feb 01 2021 at 14:59):

Yes.

view this post on Zulip Huỳnh Trần Khanh (Feb 01 2021 at 15:00):

There is a pretty well written tutorial here https://rise4fun.com/Dafny/tutorial

view this post on Zulip Huỳnh Trần Khanh (Feb 01 2021 at 15:01):

Dafny is more geared towards program verification though but you can still do some math stuff.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:01):

What kind of math stuff can you not do with it?

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 15:02):

I might be wrong but you might be able to emulate the Dafny induction in Lean by writing your own primitives of induction and wiring up some SMT solver AFAIK

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:03):

We can still answer the questions. You are free to write a custom induction tactic that tries a bunch of other tactics to close every goal.

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:03):

And wiring up SMT solver is definitely planned, and there have been experiments, but the real thing will wait for a more mature Lean 4.

view this post on Zulip Huỳnh Trần Khanh (Feb 01 2021 at 15:10):

@Johan Commelin Theoretically, none. But certain things may be more painful to prove because it lacks a mathematical library like mathlib perhaps.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:11):

Ok, I see... I don't know enough to compare these systems. But my guess is that if we try to call automatic solves on every induction proof, many proofs will become very slow.

view this post on Zulip Ryan Lahfa (Feb 01 2021 at 15:13):

That sounds really a tool for program verification, contracts, etc.

view this post on Zulip Mario Carneiro (Feb 01 2021 at 15:27):

Yes, this is the basic difference between ATP (automatic theorem proving) vs ITP (interactive theorem proving). ATP based provers are all about stating intermediate lemmas and letting the SMT backend fill the gaps, while ITPs are more about saying how the proof goes with tactics proving the individual steps (or even directly applying lemmas). The ATP approach is a lot more easy to use on simple problems, it can be almost completely hands off most of the time, but it tends to fail in really hard to predict ways when you start to scale up because you are at the mercy of the black box solver, which might fail because you wrote your hypotheses in the wrong order or something. This is bad for maintainability, and as Johan mentioned it's also really slow if your whole library is written this way


Last updated: May 14 2021 at 00:42 UTC