On Thu, 2007-03-22 at 17:15 +0100, Stefano Zacchiroli wrote:
> On Fri, Mar 23, 2007 at 03:08:53AM +1100, skaller wrote:
> > 'why' should 'recommends' ergo,
> > they're sister products.
>
> Not at all, Why works well with tons of other provers.
Indeed. It's a very cool product I think: it gives 'average'
programmers (like me) easy access to theorem provers, and
support for proof assistants by unifying the front end
up to obligation specification.
> Why it should
> recommend ergo and not, say, Coq?
ergo and why have the same language input, in fact if
you're using ergo you don't actually seem to need why at all,
so actually you have a point .. :)
BTW: my use is this:
Felix has typeclasses with semantics now, for example:
//////////////////////////////
...
// equality
typeclass Eq[t] {
virtual fun eq: t * t -> bool;
virtual fun ne (x:t,y:t):bool => not (eq (x,y));
axiom reflex(x:t): eq(x,x);
axiom sym(x:t, y:t): eq(x,y) = eq(y,x);
axiom trans(x:t, y:t, z:t): implies(eq(x,y) and eq(y,z), eq(x,z));
}
type long = "long";
open Eq[long];
fun add: long * long -> long = "$1+$2";
fun zero: unit -> long = "0L";
axiom sym(x:long, y:long): x + y == y + x;
axiom add0(x:long): x + zero() == x;
lemma radd0(x:long): zero() + x == x;
////////////////////////////
and the Felix compiler translates the axioms into why axioms,
and the lemmas into goals, which can then be processed
by ergo or another prover via why. I've also checked
using simplify, both validate the lemma above.
Yes, well, it is a rather simple lemma .. but large oaks
from small acorns grow .. :)
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net