On Tue, 2007-03-20 at 16:55 +1100, skaller wrote:
> With some hacking** I have got this to work!!
..
> Still trying to figure out how to use this:
>
> parameter decide_eq_8 : x:'T4 -> y:'T4 ->
> { } bool { if result then eq_8(x,y) else not eq_8(x,y) }
>
Hmm, actually this seems to work:
//////////////////////////////
(* type INT, at red.flx: line 2, cols 1 to 17 *)
type INT
(* function add, at red.flx: line 5, cols 11 to 30 *)
logic add_10: 'T6, 'T6 -> 'T6
(* function mul, at red.flx: line 6, cols 11 to 30 *)
logic mul_13: 'T6, 'T6 -> 'T6
(* function from_int, at red.flx: line 8, cols 11 to 33 *)
logic from_int_19: int -> 'T6
logic eq: 't, 't -> bool
axiom qsym: forall x:'t. forall y:'t. eq(x,y) = eq(y,x)
axiom qrefl: forall x:'t. eq(x,x) = true
axiom qtrans: forall x:'t1. forall y:'t. forall z:'t.
true=eq(x,y) and true=eq(y,z) -> true=eq(x,z)
(******* AXIOMS ******)
(* axiom id, at red.flx: line 11, cols 3 to 38 *)
axiom id:
forall x_40: 'T6.
true=
eq(add_10(x_40, from_int_19(0)), x_40)
(* axiom sym, at red.flx: line 10, cols 3 to 38 *)
axiom sym:
forall x_33: 'T6.
forall y_36: 'T6.
true=
eq(add_10(x_33, y_36), add_10(y_36, x_33))
goal idr:
forall x_44: 'T6.
true=
eq(add_10(from_int_19(0), x_44), x_44)
/////////////////////////
What's I've done here is just add axiom for eq which
ensure it's an equivalence relation. These would come
from the Eq typeclass automatically (if I define them! :)
The only hassle is that these axioms themselves would be
defined using equality on bool, so there is a circularity
unless Why already knows the axioms of bool equality,
OR I add these axioms manually, OR I allow a second
form of axiom (in Felix!) such as
axiom X: L = R
noting this is using = for logical equality whereas
axiom X: L == R
axiom X: eq(L,R) // eq is the name of infix ==
is simply a bool valued expression. These would translate
into the Why code
axiom X: L = R
and
axiom X: true = eq(L,R)
respectively. The first form is essential anyhow, for cases
where there is no programmer defined equality operator.
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Take Surveys. Earn Cash. Influence the Future of IT
Join SourceForge.net's Techsay panel and you'll get the chance to share your
opinions on IT & business topics through brief surveys-and earn cash
http://www.techsay.com/default.php?page=join.php&p=sourceforge&CID=DEVDEV
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
