From 1009c5dc0f7c0f5f75d69fbb3a0b04758fcf838d Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Wed, 21 Mar 2012 12:30:23 +0100 Subject: [PATCH] Reals: separate PowerInt and PowerReal, add realization of RealInfix --- Makefile.in | 2 +- ROADMAP | 8 +- drivers/coq-common.gen | 13 +- drivers/pvs-common.gen | 2 +- examples/check-builtin/real.why | 12 +- examples/check-builtin/real/why3session.xml | 427 ++++++++++++++++++-- lib/coq/real/RealInfix.v | 7 + theories/real.why | 27 +- 8 files changed, 456 insertions(+), 42 deletions(-) create mode 100644 lib/coq/real/RealInfix.v diff --git a/Makefile.in b/Makefile.in index 5ba680be0..5d1702589 100644 --- a/Makefile.in +++ b/Makefile.in @@ -837,7 +837,7 @@ ifeq (@enable_coq_libs@,yes) COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES)) -COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square +COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES)) ifeq (@enable_coq_fp_libs@,yes) diff --git a/ROADMAP b/ROADMAP index cf717de74..f9cd78978 100644 --- a/ROADMAP +++ b/ROADMAP @@ -133,8 +133,12 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990 ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié - (WHO?) revoir documentation du smoke detector - (WHO?) Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3 - - (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé - ET LES METTRE AU POINT + - (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé. Et les mettre au point: + . Lors d'un replay, le dialogue "replace proof" apparait un nombre important de fois, + il faut absolument pouvoir interrompre, ou donner une reponse qui soit appliquée pour le reste. + (le 3e bouton "never replace..." ne semble pas jourer ce role...) + . le dialogue "replace proof" est de toute facon trop large, et les choix possibles sont confus. + - DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable - (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit" - (WHO?) complete api.tex: explain how to build theories, apply diff --git a/drivers/coq-common.gen b/drivers/coq-common.gen index dd4f06540..454aa8147 100644 --- a/drivers/coq-common.gen +++ b/drivers/coq-common.gen @@ -256,11 +256,20 @@ theory real.ExpLog end -theory real.Power +theory real.PowerInt prelude "Require Import Rpower." - (* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *) + syntax function power "(powerRZ %1)" + +end + +theory real.PowerReal + + prelude "Require Import Rpower." + + syntax function pow "(Rpower %1)" + end theory real.Trigonometry diff --git a/drivers/pvs-common.gen b/drivers/pvs-common.gen index 891cb602c..2fd2958ae 100644 --- a/drivers/pvs-common.gen +++ b/drivers/pvs-common.gen @@ -242,7 +242,7 @@ theory real.ExpLog end -theory real.Power +theory real.PowerReal syntax function pow "(%1 ^ %2)" diff --git a/examples/check-builtin/real.why b/examples/check-builtin/real.why index ded841c23..434a5109c 100644 --- a/examples/check-builtin/real.why +++ b/examples/check-builtin/real.why @@ -2,5 +2,15 @@ theory Test use import real.Real goal G1 : 5.5 * 10. = 55. goal G2 : 9. / 3. = 3. - goal G3 : inv(5.) = 0.2 + goal G3 : inv 5. = 0.2 +end + +theory TestInfix + use import real.RealInfix + goal Add : 5.5 +. 10. = 15.5 + goal Sub : 9. -. 3. = 6. + goal Neg : -. 5. +. 3.5 = -. 1.5 + goal Mul : 5.5 *. 10. = 55. + goal Div : 9. /. 2. = 4.5 + goal Inv : inv 5. = 0.2 end diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml index b4063c81c..54e1cd10b 100644 --- a/examples/check-builtin/real/why3session.xml +++ b/examples/check-builtin/real/why3session.xml @@ -1,7 +1,7 @@ + name="real/why3session.xml"> + name="CVC3" + version="2.4.1"/> + + + expanded="true"> - + + + + + + + @@ -78,36 +100,50 @@ + + + + + + - + @@ -115,36 +151,363 @@ + + + + + + + + + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/lib/coq/real/RealInfix.v b/lib/coq/real/RealInfix.v new file mode 100644 index 000000000..cb3404443 --- /dev/null +++ b/lib/coq/real/RealInfix.v @@ -0,0 +1,7 @@ +(* This file is generated by Why3's Coq driver *) +(* Beware! Only edit allowed sections below *) +Require Import ZArith. +Require Import Rbase. +Require real.Real. + + diff --git a/theories/real.why b/theories/real.why index 0e0269e06..b4c424d29 100644 --- a/theories/real.why +++ b/theories/real.why @@ -26,6 +26,7 @@ theory RealInfix function ( *.) (x:real) (y:real) : real = x * y function (/.) (x:real) (y:real) : real = x / y function (-._) (x:real) : real = - x + function inv (x:real) : real = Real.inv x predicate (<=.) (x:real) (y:real) = x <= y predicate (>=.) (x:real) (y:real) = x >= y @@ -220,7 +221,27 @@ theory ExpLogTest end -theory Power +theory PowerInt + + use int.Int + use Real + + clone export int.Exponentiation with + type t = real, constant one = Real.one, function (*) = Real.(*) + + +end + +theory PowerIntTest + + use import PowerInt + + lemma Pow_2_2 : power 2.0 2 = 4.0 + +end + + +theory PowerReal use import Real use import Square @@ -251,9 +272,9 @@ theory Power end -theory PowerTest +theory PowerRealTest - use import Power + use import PowerReal lemma Pow_2_2 : pow 2.0 2.0 = 4.0 -- GitLab