Commit d6c0afc8 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Add a Coq realization for real.ExpLog.

parent b635b059
......@@ -924,7 +924,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 FromInt MinMax Real Square
COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square
COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
ifeq (@enable_coq_fp_libs@,yes)
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import Rtrigo_def.
Require Import Rpower.
Require real.Real.
(* Why3 goal *)
Notation exp := exp (only parsing).
(* Why3 goal *)
Lemma Exp_zero : ((exp 0%R) = 1%R).
exact exp_0.
Qed.
Require Import Exp_prop.
(* Why3 goal *)
Lemma Exp_sum : forall (x:R) (y:R),
((exp (x + y)%R) = ((exp x) * (exp y))%R).
exact exp_plus.
Qed.
(* Why3 goal *)
Notation log := ln (only parsing).
(* Why3 goal *)
Lemma Log_one : ((log 1%R) = 0%R).
exact ln_1.
Qed.
(* Why3 goal *)
Lemma Log_mul : forall (x:R) (y:R), ((0%R < x)%R /\ (0%R < y)%R) ->
((log (x * y)%R) = ((log x) + (log y))%R).
intros x y (Hx,Hy).
now apply ln_mult.
Qed.
(* Why3 goal *)
Lemma Log_exp : forall (x:R), ((log (exp x)) = x).
exact ln_exp.
Qed.
(* Why3 goal *)
Lemma Exp_log : forall (x:R), (0%R < x)%R -> ((exp (log x)) = x).
exact exp_ln.
Qed.
(* Why3 assumption *)
Definition log2(x:R): R := (Rdiv (log x) (log 2%R))%R.
(* Why3 assumption *)
Definition log10(x:R): R := (Rdiv (log x) (log 10%R))%R.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment