[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] real square roots and complex numbers

 Dear all, I'm trying to re-prove the algebraic formula for square roots 
 of complex numbers given, e.g., here

 I'm getting stuck with silly things for example PVS not accepting a 
 trivial identity such as

 [-1]  w!1`2 > 0
 [1]   (w!1`1 + r!1) / 2 - (r!1 - w!1`1) / 2 = w!1`1

 unless I do (name-replace "x!1" "w!1`1").

 Normally, I would have thought that a proof of the "lemma" below should 
 be automatic once the right hints are installed which is why I'm asking 
 you for help :-)

 Looking forward, Martin

 sqrt: THEORY
 	sqrt : [nnreal -> nnreal]
 	sqrt_ax : AXIOM FORALL(x:nnreal):sqrt(x)*sqrt(x) = x
 	% more axioms needed ???

 	CC : TYPE = [real,real]
 	CCtimes(w,z:CC) : CC = (w`1*z`1 - w`2*z`2, w`1*z`2+w`2*z`1)
 	CCsqrt(w:CC) : CC = LET r=sqrt(w`1*w`1+w`2*w`2) IN
                             LET  sign = IF w`2 > 0 THEN 1 ELSE -1 ENDIF 
         lemma : LEMMA FORALL(w:CC):CCtimes(CCsqrt(w),CCsqrt(w))=w
 END sqrt