Return-Path: owner-stds-754@majordomo.ieee.org Delivery-Date: Fri Aug 16 21:10:10 2002 Received: from relay1.EECS.Berkeley.EDU (relay1.EECS.Berkeley.EDU [169.229.60.163]) by mailspool.CS.Berkeley.EDU (8.9.3/) with ESMTP id VAA04909; Fri, 16 Aug 2002 21:10:09 -0700 (PDT) Received: from EECS.Berkeley.EDU (localhost.Berkeley.EDU [127.0.0.1]) by relay1.EECS.Berkeley.EDU (8.9.3/8.9.3) with ESMTP id VAA27431; Fri, 16 Aug 2002 21:10:09 -0700 (PDT) Received: from ruebert.ieee.org (ruebert.ieee.org [140.98.193.10]) by EECS.Berkeley.EDU (8.9.3/8.9.3) with ESMTP id VAA27425; Fri, 16 Aug 2002 21:09:48 -0700 (PDT) Received: (from daemon@localhost) by ruebert.ieee.org (Switch-2.1.0/Switch-2.1.0) id g7H45Ns28254 for stds-754-resent; Sat, 17 Aug 2002 00:05:24 -0400 (EDT) From: "Marc Daumas" To: Cc: "Cesar A. Munoz H." , "Gilles Dowek" , "Wolfgang J. Paul" , "John Harrison" , =?iso-8859-1?Q?Laurent_Th=E9ry?= , =?iso-8859-1?Q?Lo=EFc_Pottier?= , Subject: A question from Professor Kahan Date: Fri, 16 Aug 2002 23:59:34 -0400 Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 8bit X-Priority: 3 (Normal) X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook IMO, Build 9.0.2416 (9.0.2911.0) Importance: Normal X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2600.0000 Sender: owner-stds-754@majordomo.ieee.org Precedence: bulk X-Resent-To: Multiple Recipients X-Listname: stds-754 X-Info: [Un]Subscribe requests to majordomo@majordomo.ieee.org X-Moderator-Address: stds-754-approval@majordomo.ieee.org Dear attendees, Dear members of the mailing list, On July 18th meeting on the revision of the IEEE 754 standard, Professor Kahan reacted to my talk on automatic proof checking for floating point arithmetic. (Please refer to the previous announcement on the mailing list and the PDF of the slides http://grouper.ieee.org/groups/754/meeting-materials/2002-07-18-daumas.pdf) One of the concerns of Professor Kahan was on our ability to do difficult or even simple mathematics with automatic proof systems. He offered a small puzzle. I will present you the puzzle first, then our model and our solution using Coq automatic proof checker. The problem involves complex numbers. We define the principle square root (Psqrt) of a number as the (unique) square root with a positive real component. A convention is fixed for the case where both square roots are imaginary numbers. Professor Kahan said that one of the statements is always true and the other fails on some complex numbers. Psqrt(1 - z^2) =? Psqrt (1 - z) Psqrt (1 + z) Psqrt(z^2 - 1) =? Psqrt (z - 1) Psqrt (1 + z) The correct answer can be easily prompted to a human being using polar properties of the complex field. However, we used the Cartesian notation in our proof as the tedious aspects of the proof are handled automatically by our system. The proof uses a tools that eliminates quantifiers (Hormander's algorithm) due to Loïc Pottier and Assia Mahboubi at the INRIA in Sophia Antipolis. We assume that Psqrt(1 + z) = S1 = a1 + i b1 Psqrt(1 - z) = S2 = a2 + i b2 The hypotheses are - both square roots are principle a1 >= 0 and a2 >= 0 - S1 and S2 squared are related so that z = S1^2 - 1 = 1 - S2^2 leading to an equation for the real component and an equation for the imaginary component a1*a1 + a2*a2 = b1*b1 + b2*b2 + 2 a1*b1 + a2*b2 = 0 We have to prove that a1*a2 - b1*b2 >= 0 For the other equality, we assume that Psqrt(1 + z) = S1 = a1 + i b1 Psqrt(z - 1) = S2 = a2 + i b2 The hypotheses are now - both square roots are still principle a1 >= 0 and a2 >= 0 - S1 and S2 squared are now related so that z = S1^2 - 1 = S2^2 + 1 leading to an equation for the real component and an equation for the imaginary component a1*a1 + b2*b2 = a2*a2 + b1*b1 + 2 a1*b1 = a2*b2 We have to prove once again that a1*a2 - b1*b2 >= 0 The tool provides a proof of the statement directly readable by Coq that is checked automatically. It answers that the first fact is always true whereas the second one cannot be proved. Laurent Thery (Laurent.Thery@sophia.inria.fr), Loic Pottier (Loic.Pottier@sophia.inria.fr) or Assia Mahboubi (Assia.Mahboubi@sophia.inria.fr) of the INRIA at Sophia Antipolis can provide more details on the tool that they have used and on matters on Coq. -- Marc Daumas - Charge de recherches au CNRS (LIP - ENS de Lyon) mailto:Marc.Daumas@ENS-Lyon.Fr - http://www.ens-lyon.fr/~daumas PGP Key FP : 69B6 11D1 DA61 717F DF76 5B92 E4EC B289 D607 F324 ENS de Lyon - 46, allee d'Italie - 69364 Lyon Cedex 07 - FRANCE Phone: (+33) 4 72 72 83 52 - Fax: (+33) 4 72 72 80 80