3 ms·

What about coq vs z3 ? It seems they are the two most actively developed theorem provers/checkers

ahelwer 7y ago
Z3 is very different from Coq and Lean. Coq and Lean are interactive theorem provers, while Z3 is a satisfiability modulo theories (SMT) solver which can do things like checking whether a logical formula is satisfiable or finding a solution for a system of constraints.
- The_rationalist 7y ago
  Thanks! And what about agda and Idris?
  - aweinstock 7y ago
    Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.
aweinstock 7y ago
For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of Euclid's theorem on there being infinitely many primes). Here's a transcript of using the z3 python bindings to ask for a proof: $ python >>> import z3 >>> x, y = z3.Ints('x y') >>> s = z3.Solver() >>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0))))) >>> s.check() unknown z3 returns unknown (if it had returned "unsat", it would have been possible to extract a resolution-refutation proof), and there's not much that can be done with the unknown. Here's a Coq interactive session that proves most of the cases (with one subproof left unsolved, it was taking me too long relative to the rest of the proof). $ coqtop Require Import NArith. Require Import Omega. Lemma x_le_fact : forall x, x <= fact x. induction x;. - simpl; omega. - simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *) Admitted. Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0. intros x; exists (fact x). split. - unfold ">=". apply x_le_fact. - induction x. + simpl; reflexivity. + (* goal here is `fact (S x) mod S x = 0` *) unfold fact; fold fact. (* goal here is `(S x * fact x) mod S x = 0` *) rewrite (Nat.mul_comm (S x) (fact x)). (* goal here is `(fact x * S x) mod S x = 0` *) apply (Nat.mod_mul (fact x) (S x)). discriminate. Qed. Unlike z3, you need to manually tell Coq what the steps are, but it gives you feedback on which steps are correct, and what assumptions are available and what subgoals still remain at each step (I've included some of those as comments, running the proof through the interpreter shows more detail).

Z3 is very different from Coq and Lean. Coq and Lean are interactive theorem provers, while Z3 is a satisfiability modulo theories (SMT) solver which can do things like checking whether a logical formula is satisfiable or finding a solution for a system of constraints.

The_rationalist 7y ago
Thanks! And what about agda and Idris?
- aweinstock 7y ago
  Agda and Idris are the same sort of tool (total dependently typed languages/proof assistants/interactive theorem provers) as Lean and Coq.

aweinstock 7y ago

For a concrete example of how z3 differs from Coq, consider trying to prove that "for all integers x, there exists an integer y greater than x such that x divides y" (a subgoal of Euclid's theorem on there being infinitely many primes). Here's a transcript of using the z3 python bindings to ask for a proof: $ python >>> import z3 >>> x, y = z3.Ints('x y') >>> s = z3.Solver() >>> s.add(z3.Not(z3.ForAll([x], z3.Exists([y], z3.And(y >= x, y % x == 0))))) >>> s.check() unknown z3 returns unknown (if it had returned "unsat", it would have been possible to extract a resolution-refutation proof), and there's not much that can be done with the unknown. Here's a Coq interactive session that proves most of the cases (with one subproof left unsolved, it was taking me too long relative to the rest of the proof). $ coqtop Require Import NArith. Require Import Omega. Lemma x_le_fact : forall x, x <= fact x. induction x;. - simpl; omega. - simpl; admit. (* Proving `x <= fact x -> S x <= fact x + x * fact x` left unsolved here *) Admitted. Goal forall (x : nat), exists (y : nat), y >= x /\ Nat.modulo y x = 0. intros x; exists (fact x). split. - unfold ">=". apply x_le_fact. - induction x. + simpl; reflexivity. + (* goal here is `fact (S x) mod S x = 0` *) unfold fact; fold fact. (* goal here is `(S x * fact x) mod S x = 0` *) rewrite (Nat.mul_comm (S x) (fact x)). (* goal here is `(fact x * S x) mod S x = 0` *) apply (Nat.mod_mul (fact x) (S x)). discriminate. Qed. Unlike z3, you need to manually tell Coq what the steps are, but it gives you feedback on which steps are correct, and what assumptions are available and what subgoals still remain at each step (I've included some of those as comments, running the proof through the interpreter shows more detail).