*To*: Stefano Zacchiroli <zack@debian.org>*Cc*: debian-ocaml-maint@lists.debian.org*Subject*: Re: why and ergo*From*: skaller <skaller@users.sourceforge.net>*Date*: Fri, 23 Mar 2007 03:50:32 +1100*Message-id*: <1174582232.22719.24.camel@rosella.wigram>*In-reply-to*: <20070322161554.GA12635@takhisis.invalid>*References*: <1174525621.27055.40.camel@rosella.wigram> <4602A178.9020500@ens-lyon.org> <1174579733.22625.5.camel@rosella.wigram> <20070322161554.GA12635@takhisis.invalid>

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

**References**:**why and ergo***From:*skaller <skaller@users.sourceforge.net>

**Re: why and ergo***From:*Samuel Mimram <samuel.mimram@ens-lyon.org>

**Re: why and ergo***From:*skaller <skaller@users.sourceforge.net>

**Re: why and ergo***From:*Stefano Zacchiroli <zack@debian.org>

- Prev by Date:
**Re: why and ergo** - Next by Date:
**Re: why and ergo** - Previous by thread:
**Re: why and ergo** - Next by thread:
**Re: why and ergo** - Index(es):