coq.drv 735 Bytes
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1

2
prelude "(* This file is generated by Why3's Coq driver *)"
3
prelude "(* Beware! Only edit allowed sections below    *)"
MARCHE Claude's avatar
MARCHE Claude committed
4

5 6
printer "coq"
filename "%f_%t_%g.v"
7

8
import "coq-common.gen"
MARCHE Claude's avatar
MARCHE Claude committed
9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34

theory real.Trigonometry

  prelude "Require Import Rtrigo."
  prelude "Require Import AltSeries. (* for def of pi *)"

  syntax function cos "(Rtrigo_def.cos %1)"
  syntax function sin "(Rtrigo_def.sin %1)"

  syntax function pi "PI"

  syntax function tan "(Rtrigo.tan %1)"

  (* syntax function atan "atan not defined in Coq ?" *)

  remove prop Pythagorean_identity
  remove prop Cos_le_one
  remove prop Sin_le_one
  remove prop Cos_0
  remove prop Sin_0
  remove prop Cos_pi
  remove prop Sin_pi
  remove prop Cos_pi2
  remove prop Sin_pi2

end