Ask Your Question
0

Need to improve a function in sage which checks trueness of expressions in an example.

asked 2013-01-04 10:55:37 +0100

sage_learner gravatar image

Hello !

Here I have made a function in sage which checks equality between consecutive expressions in an example.

This function takes a set of examples as an argument. I want to improve my function and I really need comments and suggestions for correcting this function.

Two examples which I have used are as follows.

Example 1:

(1 - ((1 + sqrt(a))/(sqrt(a)- 1)))

=

(1 + ((1 + sqrt(a))/(-sqrt(a) + 1)))

=

(1 + ((1 + sqrt(a))* (1 + sqrt(a))/((-sqrt(a) + 1) * (sqrt(a) + 1))))

=

(1 + ((1 + 2* sqrt(a) + a)/(1 - a)))

=

(1 + ((1+a + 2* sqrt(a) )/(1-a)))

=

(((1-a)/(1-a)) + ((1+a + 2* sqrt(a))/(1-a)))

=

(1-a+1+a+ 2*sqrt(a))/(1-a)

=

(2+2*sqrt(a))/(1-a)

Example2:

x^2 + 2*x -3 == 0

<=>

x == (-2 + (2^2 -41(-3))^(1/2))/(21) or x == (-2 - (2^2 -41(-3))^(1/2))/(21)

<=>

x == (-2 + (4+12)^(1/2))/(21) or x == (-2 - (4+12)^(1/2))/(21)

<=>

x == (-2 + (16)^(1/2))/(21) or x == (-2 - (16)^(1/2))/(21)

<=>

x == (-2 + 4)/(21) or x == (-2 - 4)/(21)

<=>

x == (2)/(2) or x == (-6)/(2)

<=>

x == 1 or x == -3

The Problem is , following function checks first example correctly but not second example. In the second example, final answer is x == 1 or x == -3 but even if I provide wrong answer x == -1 or x == -3 it gives true. I have already received explanation about how 'or' behaves. see here

---------------Function begins ---------------

var('j,e,exprList,as1,i,lhs,rhs,r,r1,x')

def ComExpr(a):

r1 = []; 

for j in range(0,len(a)):

forget();

    e = a[ZZ(j)]

    exprList = e[0]

    as1 = e[1]
    print len(a)

r = [];

    for i in range(0,len(exprList)-1):

    forget(); 

        lhs = exprList[ZZ(i)]

        rhs = exprList[ZZ(i+1)]

    assume(as1 and lhs);   

    p1 = rhs.full_simplify()

    forget();

        assume(as1 and rhs); 

    p2 = lhs.full_simplify()

    r.append(bool(p1 and p2))

    r1.append(r)    

return r1

e1 is first example containing two elements one is list of expressions and another is assumption. Same for e2.

e1 = [[(1 - ((1 + sqrt(a))/(sqrt(a)- 1))) == (1 + ((1 + sqrt(a))/(-sqrt(a) + 1))), (1 + ((1 + sqrt(a))/(-sqrt(a) + 1))) == (1 + ((1 + sqrt(a))* (1 + sqrt(a))/((-sqrt(a) + 1) * (sqrt(a) + 1)))), (1 + ((1 + sqrt(a))* (1 + sqrt(a))/((-sqrt(a) + 1) * (sqrt(a) + 1)))) == (1 + ((1 + 2* sqrt(a) + a)/(1 - a))), (1 + ((1 + 2* sqrt(a) + a)/(1 - a))) == (1 + ((1+a + 2* sqrt(a) )/(1-a))), (1 + ((1+a + 2* sqrt(a) )/(1-a))) == (((1-a)/(1-a)) + ((1+a + 2* sqrt(a) )/(1-a))), (((1-a)/(1-a)) + ((1+a + 2* sqrt(a))/(1-a))) == (1-a+1+a+ 2*sqrt(a))/(1-a)], a > 1];

sage: ComExpr([e1]) 1 [[True, True, True, True, True]]

e2=[[x^2 + 2x -3 == 0, x == (-2 + (2^2 -41(-3))^(1/2))/(21) or x == (-2 - (2^2 -41(-3))^(1/2))/(21),x == (-2 ... (more)

edit retag flag offensive close merge delete

Comments

You "really need comments and suggestions" about very cumbersome expressions, and in a precedent post it was "very necessary" for you "to understand this behavior of sage", please what does it mean ?

Bétréma gravatar imageBétréma ( 2013-01-04 13:44:04 +0100 )edit

Sorry for improper English. In the preceding post I wanted to know How 'or' works in sage. But I got answer and now I know that. In this post I said I really need comments and suggestions because I want to edit this function and want to make it more reliable.

sage_learner gravatar imagesage_learner ( 2013-01-05 03:41:57 +0100 )edit

You are probably a high school student who is struggling with quadratic equations and so on, I can tell you that Sage is definitely useless for learning how to handle such computations and for acquiring the necessary skills in this domain. Sorry and good luck with a more traditional approach !

Bétréma gravatar imageBétréma ( 2013-01-05 13:39:14 +0100 )edit

Actually I am using mathematical problems from secondary school or high school level and trying to develop a function in sage which can check whether consecutive expressions are logically true or not, and hence we can check whole example whether it is correct or not.

sage_learner gravatar imagesage_learner ( 2013-01-05 19:24:36 +0100 )edit

1 Answer

Sort by » oldest newest most voted
1

answered 2013-01-06 09:24:55 +0100

Your question is a bit daunting, but let us make some experiments (Sage predefines x to be a global indeterminate):

sage: p=x^2+2*x-3
sage: p.parent()
Symbolic Ring

Who is this guy? His nickname is SR:

sage: SR?
Symbolic Ring, parent object for all symbolic expressions.

One of the main goals of symbolic calculus is to solve equations:

sage: solve(p==0,x), solve(p==1,x)
([x == -3, x == 1], [x == -sqrt(5) - 1, x == sqrt(5) - 1])

Assume is badly documented, but looks useful in this context:

sage: assume(x>0)
sage: solve(p==0,x), solve(p==1,x)
([x == 1], [x == sqrt(5) - 1])
sage: assume(x, 'rational')
sage: assumptions()
[x > 0, x is rational]
sage: solve(p==0,x), solve(p==1,x)
([x == 1], [])

So far so good, and back to your question: is Sage a proof checker, which could help to check derivation of new propositions from assumptions? Answer is definitely negative:

sage: forget(); assume(p==0); assumptions()
[x^2 + 2*x - 3 == 0]
sage: prop = (x==1) or (x==-3); prop
x == -3

This very strange result is explained in a preceeding post.

sage: bool (prop)
False

Imho, no hope for improving your function, Sage is not the right tool. If you are interested in proof checkers, take a look at Coq, but this is another story.

edit flag offensive delete link more

Comments

Thanks for the opinion. Yes I am interesting in finding whether computer algebra system like sage could be useful for checking purpose. Again thanks.

sage_learner gravatar imagesage_learner ( 2013-01-07 07:09:30 +0100 )edit

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

Stats

Asked: 2013-01-04 10:55:37 +0100

Seen: 450 times

Last updated: Jan 06 '13