4 ms·

> Is this true though? What program properties can Isabelle easily automate the proofs of that Coq cannot? Almost all? Granted, I haven't used Coq very much,

> Is this true though? What program properties can Isabelle easily automate the proofs of that Coq cannot? Almost all? Granted, I haven't used Coq very much, so correct me if I'm wrong, but isn't it true that in Coq, with the exception of basic proofs like simple arithmetic expressions, in order to prove a theorem you have to at least explicitly know and write the name of the lemmas that are needed to prove it (apart from how they fit together)? In Isabelle/HOL, many times you literally only need to write "try" and Isabelle will find the proof of the theorem for you, including the lemmas that were needed to prove it and how they fit together (assuming these lemmas were already proven before). If it turns out that your theorem is false, it can show you an example of inputs where it fails. This auto-proof functionality I'm describing is mostly thanks to Sledgehammer [0], the auto-counterexample finding is due to Nitpick (and another tool which I can't remember), although there are a few other automation tools that are also very useful. Granted, you still have to have a high-level understanding of how you want to prove your code, but I would argue this eliminates a lot of the work and (wasted?) time you need to accomplish the final goal... [0] http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehammer.html http://isabelle.in.tum.de/website-Isabelle2009-1/sledgehamme...

seanwilson 9y ago
Do you have any example proof scripts of some basic algorithms where the proofs can be almost fully automated in Isabelle?
- wizeman 9y ago
  See [1] for an example (edit: although this may not be the best example nowadays, see below): Quoting: > Consider the conjecture "length(tl xs) <= length xs", which states that the length of a list’s tail (its "cdr") is less than or equal to the length of the entire list. > Thanks to Vampire, Sledgehammer finds the following proof: by (metis append_Nil2 append_eq_conv_conj drop_eq_Nil drop_tl tl.simps(1)) Those are all the lemmas that were needed to prove the theorem. They were selected completely automatically. AFAIU the "metis" procedure tries to fit the lemmas together so that they prove the theorem, and I believe the HOL kernel gives high assurance that if "metis" succeeds, then the theorem was proven correctly (but my understanding may be wrong here). Note that Sledgehammer may even automatically find and return a human-readable proof, which for the example above, it returns something like this: proof – have “tl [] = []” by (metis tl.simps(1)) hence “∃u. xs @ u = xs ∧ tl u = []” by (metis append_Nil2) hence “tl (drop (length xs) xs) = []” by (metis append_eq_conv_conj) hence “drop (length xs) (tl xs) = []” by (metis drop_tl) thus “length (tl xs) <= length xs” by (metis drop_eq_Nil) qed Edit: That said, note that at least nowadays Isabelle/HOL seems to be able prove the above theorem by simplification alone ("by simp"), so this may not be the best example. [1] http://people.irisa.fr/Thomas.Genet/ACF/BiblioIsabelle/isabelleOverview.pdf http://people.irisa.fr/Thomas.Genet/ACF/BiblioIsabelle/isabe...
  - cmrx64 9y ago
    metis is a first-order automated theorem prover. the metis tactic will handle encoding the goal as a first-order problem, using ~just the rules you provide it, invoking actual-metis, and reconstructing a proof (in the kernel logic) from the output proof. so, it is impossible to prove things that are false using the metis tactic (ie, metis is entirely out of the TCB). re: the simplifier, I feel like it's a bad example because coming up with good simp rules and knowing when to add them and when not to when writing new code in Isabelle/HOL is almost an art.
mcguire 9y ago
"Granted, I haven't used Coq very much, so correct me if I'm wrong, but isn't it true that in Coq, with the exception of basic proofs like simple arithmetic expressions, in order to prove a theorem you have to at least explicitly know and write the name of the lemmas that are needed to prove it (apart from how they fit together)?" Coq has automated tactics like "auto" that search for proofs based on a configurable database of "hints". On the other hand, if it doesn't succeed, it leaves the proof state unchanged and gives no hints as to what to do next. But on the other, other hand, if it succeeds, it gives no hints as to how it succeeds. So it's less useful than it might be. Edit: Also, Coq has a dandy baked-in search system for finding lemmas and so-forth that would be useful in a given situation. On the other hand, for a similar flavor, look on Hoogle for functions transforming one list into another list. I need to play with Isabelle.

seanwilson 9y ago

Do you have any example proof scripts of some basic algorithms where the proofs can be almost fully automated in Isabelle?

wizeman 9y ago
See [1] for an example (edit: although this may not be the best example nowadays, see below): Quoting: > Consider the conjecture "length(tl xs) <= length xs", which states that the length of a list’s tail (its "cdr") is less than or equal to the length of the entire list. > Thanks to Vampire, Sledgehammer finds the following proof: by (metis append_Nil2 append_eq_conv_conj drop_eq_Nil drop_tl tl.simps(1)) Those are all the lemmas that were needed to prove the theorem. They were selected completely automatically. AFAIU the "metis" procedure tries to fit the lemmas together so that they prove the theorem, and I believe the HOL kernel gives high assurance that if "metis" succeeds, then the theorem was proven correctly (but my understanding may be wrong here). Note that Sledgehammer may even automatically find and return a human-readable proof, which for the example above, it returns something like this: proof – have “tl [] = []” by (metis tl.simps(1)) hence “∃u. xs @ u = xs ∧ tl u = []” by (metis append_Nil2) hence “tl (drop (length xs) xs) = []” by (metis append_eq_conv_conj) hence “drop (length xs) (tl xs) = []” by (metis drop_tl) thus “length (tl xs) <= length xs” by (metis drop_eq_Nil) qed Edit: That said, note that at least nowadays Isabelle/HOL seems to be able prove the above theorem by simplification alone ("by simp"), so this may not be the best example. [1] http://people.irisa.fr/Thomas.Genet/ACF/BiblioIsabelle/isabelleOverview.pdf http://people.irisa.fr/Thomas.Genet/ACF/BiblioIsabelle/isabe...
- cmrx64 9y ago
  metis is a first-order automated theorem prover. the metis tactic will handle encoding the goal as a first-order problem, using ~just the rules you provide it, invoking actual-metis, and reconstructing a proof (in the kernel logic) from the output proof. so, it is impossible to prove things that are false using the metis tactic (ie, metis is entirely out of the TCB). re: the simplifier, I feel like it's a bad example because coming up with good simp rules and knowing when to add them and when not to when writing new code in Isabelle/HOL is almost an art.

mcguire 9y ago

"Granted, I haven't used Coq very much, so correct me if I'm wrong, but isn't it true that in Coq, with the exception of basic proofs like simple arithmetic expressions, in order to prove a theorem you have to at least explicitly know and write the name of the lemmas that are needed to prove it (apart from how they fit together)?" Coq has automated tactics like "auto" that search for proofs based on a configurable database of "hints". On the other hand, if it doesn't succeed, it leaves the proof state unchanged and gives no hints as to what to do next. But on the other, other hand, if it succeeds, it gives no hints as to how it succeeds. So it's less useful than it might be. Edit: Also, Coq has a dandy baked-in search system for finding lemmas and so-forth that would be useful in a given situation. On the other hand, for a similar flavor, look on Hoogle for functions transforming one list into another list. I need to play with Isabelle.