coq.drv 2.76 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
1 2

printer "coq"
3
filename "%f_%t_%g.v"
MARCHE Claude's avatar
MARCHE Claude committed
4

MARCHE Claude's avatar
MARCHE Claude committed
5
prelude "(* generated by Why3's Coq driver *)" 
MARCHE Claude's avatar
MARCHE Claude committed
6

MARCHE Claude's avatar
MARCHE Claude committed
7
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
8 9 10 11

  prelude "Require Import ZArith."
  prelude "Require Import Rbase."

MARCHE Claude's avatar
MARCHE Claude committed
12 13
  syntax type   int     "Z"
  syntax type   real    "R"
MARCHE Claude's avatar
MARCHE Claude committed
14
  syntax logic  (_=_)   "(%1 = %2)" 
MARCHE Claude's avatar
MARCHE Claude committed
15 16 17
  syntax logic  (_<>_)  "(%1 <> %2)"
end

MARCHE Claude's avatar
MARCHE Claude committed
18 19 20 21 22 23 24 25 26 27 28 29 30 31
theory bool.Bool

  syntax type bool "bool"

  syntax logic True "true"
  syntax logic False "false"

  syntax logic andb "(andb %1 %2)"
  syntax logic orb "(orb %1 %2)"
  syntax logic xorb "(xorb %1 %2)"
  syntax logic notb "(negb %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58

theory int.Int

  syntax logic zero "0%Z"
  syntax logic one "1%Z"

  syntax logic (_+_) "(%1 + %2)%Z"
  syntax logic (_-_) "(%1 - %2)%Z"
  syntax logic (_*_) "(%1 * %2)%Z"
  syntax logic (-_)  "(-%1)%Z"

  syntax logic (_<=_) "(%1 <= %2)%Z"
  syntax logic (_<_) "(%1 <  %2)%Z"
  syntax logic (_>=_) "(%1 >= %2)%Z"
  syntax logic (_>_) "(%1 >  %2)%Z"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary

end

MARCHE Claude's avatar
MARCHE Claude committed
59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

theory real.Real

  syntax logic zero "0%R"
  syntax logic one "1%R"

  syntax logic (_+_) "(%1 + %2)%R"
  syntax logic (_-_) "(%1 - %2)%R"
  syntax logic (-_)  "(-%1)%R"
  syntax logic (_*_) "(%1 * %2)%R"
  syntax logic (_/_) "(Rdiv %1 %2)%R"
  syntax logic inv  "(Rinv %1)"

  syntax logic (_<=_) "(%1 <= %2)%R"
  syntax logic (_<_) "(%1 <  %2)%R"
  syntax logic (_>=_) "(%1 >= %2)%R"
  syntax logic (_>_) "(%1 >  %2)%R"

  remove prop CommutativeGroup.Comm.Comm
  remove prop CommutativeGroup.Assoc.Assoc
  remove prop CommutativeGroup.Unit_def
  remove prop CommutativeGroup.Inv_def
  remove prop Assoc.Assoc
  remove prop Mul_distr
  remove prop Comm.Comm
  remove prop Unitary
  remove prop Inverse

end


theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax logic abs "(Rabs %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106 107 108
theory real.FromInt

  syntax logic from_int "(IZR %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
theory real.Square

  prelude "Require Import R_sqrt."

  syntax logic sqr "(Rsqr %1)"

  syntax logic sqrt "(sqrt %1)"  (* and not Rsqrt *)

end


theory real.ExpLog

  prelude "Require Import Rtrigo_def."
  prelude "Require Import Rpower."

  syntax logic exp "(exp %1)"

  syntax logic log "(ln %1)"

end


theory real.Power 

  prelude "Require Import Rpower."

  (* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *)
end

theory real.Trigonometry

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

  syntax logic cos "(cos %1)"
  syntax logic sin "(sin %1)"

  syntax logic pi "PI"

  syntax logic tan "(tan %1)"
  (* syntax logic atan "atan not defined in Coq ?" *)

end