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

Stream: new members

[Huỳnh Trần Khanh]

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?

[Huỳnh Trần Khanh]

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

[Johan Commelin]

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

[Huỳnh Trần Khanh]

Yes.

[Huỳnh Trần Khanh]

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

[Huỳnh Trần Khanh]

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

[Johan Commelin]

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

[Ryan Lahfa]

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

[Patrick Massot]

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.

[Patrick Massot]

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.

[Huỳnh Trần Khanh]

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

[Johan Commelin]

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.

[Ryan Lahfa]

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

[Mario Carneiro]

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