Re: verification
- To: mathgroup at smc.vnet.net
- Subject: [mg74724] Re: verification
- From: "David W.Cantrell" <DWCantrell at sigmaxi.net>
- Date: Mon, 2 Apr 2007 06:57:00 -0400 (EDT)
- References: <eunpso$772$1@smc.vnet.net>
"dimitris" <dimmechan at yahoo.com> wrote:
> Hello.
>
> foo = {ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 -
> 4*I])] + ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])], ArcTan[3] + ArcTan[5] +
> ArcTan[41/3] + ArcTan[21], 2*Pi - ArcTan[1/4] - ArcTan[5/12]};
>
> The elements of foo list are equal
>
> Chop[N[foo, 30]]
> {5.64341552435296080601310475496,5.64341552435296080601310475496,5.\
> 64341552435296080601310475496}
>
> Block[{Message}, FullSimplify[foo[[2]] == foo[[3]]]]
> Block[{Message}, FullSimplify[foo[[1]] == foo[[3]]]]
> Block[{Message}, FullSimplify[foo[[1]] == foo[[2]]]]
>
> True
OK, so you easily showed that foo[[2]] and foo[[3]] are the same. Here's
the easiest way I know to show that foo[[1]] and foo[[3]] are the same:
In[4]:= FullSimplify[TrigToExp[foo[[1]]]] == FullSimplify[foo[[3]]]
Out[4]= True
What really disturbs me is that I can also "show" that foo[[1]] and
foo[[3]] are NOT the same:
In[6]:= FullSimplify[TrigToExp[foo[[1]]] == foo[[3]]]
messages regarding Internal precision limit snipped
Out[6]= False
It seems that Mathematica is asserting that two _equal_ expressions
are _not equal_. What am I missing?! (Of course, if Mathematica had merely
left the logical expression unevaluated, I wouldn't have been disturbed...)
BTW, I haven't found a direct way to use Mathematica to show that foo[[1]]
and foo[[2]] are the same.
David W. Cantrell
> ArcCot[4] + ArcTan[5/12] + ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/
> (1 + Sqrt[-15 - 4*I])] + ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])] == 2*Pi
> ArcTan[8/(1 - Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 - 4*I])] +
> ArcTan[8/(1 - Sqrt[-15 + 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])] == ArcTan[3] + ArcTan[5] +
> ArcTan[41/3] + ArcTan[21]
>
> In one of my attempts to show that foo[[1]]=foo[[3]] and
> foo[[1]]=foo[[2]] I try
>
> Block[{Message}, (FullSimplify[#1, ComplexityFunction -> LeafCount] & )
> [foo[[1]] == foo[[3]]]]
> Block[{Message}, (FullSimplify[#1, ComplexityFunction -> LeafCount] & )
> [foo[[1]] == foo[[2]]]]
>
> 2*Pi + ArcTan[8/(-1 + Sqrt[-15 - 4*I])] + ArcTan[8/(-1 + Sqrt[-15 +
> 4*I])] ==
> ArcCot[4] + ArcTan[5/12] + ArcTan[8/(1 + Sqrt[-15 - 4*I])] +
> ArcTan[8/(1 + Sqrt[-15 + 4*I])]
> ArcTan[8/(1 + Sqrt[-15 - 4*I])] + ArcTan[8/(1 + Sqrt[-15 + 4*I])] ==
> ArcTan[3] + ArcTan[5] + ArcTan[41/3] + ArcTan[21] + ArcTan[8/(-1 +
> Sqrt[-15 - 4*I])] + ArcTan[8/(-1 + Sqrt[-15 + 4*I])]
>
> but I failed.
>
> Introducing the following ComplexityFunction
>
> lst = Alternatives @@ Replace[ToExpression[Names["Arc*"]], x_ -> _x,
> -1]
> _ArcCos | _ArcCosh | _ArcCot | _ArcCoth | _ArcCsc | _ArcCsch | _ArcSec
> | _ArcSech | _ArcSin | _ArcSinh | _ArcTan | _ArcTanh
>
> I got
>
> TimeConstrained[Block[{Message}, (FullSimplify[#1, ComplexityFunction -
> > (Count[{#1}, lst, Infinity] & )] & )[
> foo[[1]] == foo[[3]]]], 300]
> $Aborted
>
> TimeConstrained[Block[{Message}, (FullSimplify[#1, ComplexityFunction -
> > (Count[{#1}, lst, Infinity] & )] & )[
> foo[[1]] == foo[[2]]]], 300]
> 0 == 4*Pi + 2*Log[(825/2873 - (2752*I)/2873)^(-(I/2))] + I*Log[-(((-1
> - 8*I) + Sqrt[-15 - 4*I])/(1 - Sqrt[-15 - 4*I]))] -
> I*Log[-(((-1 + 8*I) + Sqrt[-15 - 4*I])/(1 - Sqrt[-15 - 4*I]))] -
> I*Log[((1 - 8*I) + Sqrt[-15 - 4*I])/(1 + Sqrt[-15 - 4*I])] +
> I*Log[((1 + 8*I) + Sqrt[-15 - 4*I])/(1 + Sqrt[-15 - 4*I])] + I*Log[-
> (((-1 - 8*I) + Sqrt[-15 + 4*I])/(1 - Sqrt[-15 + 4*I]))] -
> I*Log[-(((-1 + 8*I) + Sqrt[-15 + 4*I])/(1 - Sqrt[-15 + 4*I]))] -
> I*Log[((1 - 8*I) + Sqrt[-15 + 4*I])/(1 + Sqrt[-15 + 4*I])] + I*Log[((1
> + 8*I) + Sqrt[-15 + 4*I])/(1 + Sqrt[-15 + 4*I])]
>
> Having failed also in similar attempts I would really appreciate any
> ideas!
>
> Dimitris
- Follow-Ups:
- Re: Re: verification
- From: Andrzej Kozlowski <akoz@mimuw.edu.pl>
- Re: Re: verification