coq.drv 2.93 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
valid 0
6 7 8
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"

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

MARCHE Claude's avatar
MARCHE Claude committed
12
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
13 14 15 16

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

17 18 19
  syntax type   int   "Z"
  syntax type   real  "R"
  syntax logic  (=)   "(%1 = %2)" 
MARCHE Claude's avatar
MARCHE Claude committed
20 21
end

MARCHE Claude's avatar
MARCHE Claude committed
22 23
theory bool.Bool

24
  syntax type bool   "bool"
MARCHE Claude's avatar
MARCHE Claude committed
25

26
  syntax logic True  "true"
MARCHE Claude's avatar
MARCHE Claude committed
27 28
  syntax logic False "false"

29 30 31 32
  syntax logic andb  "(andb %1 %2)"
  syntax logic orb   "(orb %1 %2)"
  syntax logic xorb  "(xorb %1 %2)"
  syntax logic notb  "(negb %1)"
MARCHE Claude's avatar
MARCHE Claude committed
33 34 35

end

MARCHE Claude's avatar
MARCHE Claude committed
36 37 38 39

theory int.Int

  syntax logic zero "0%Z"
40
  syntax logic one  "1%Z"
MARCHE Claude's avatar
MARCHE Claude committed
41

42 43 44 45
  syntax logic (+)  "(%1 + %2)%Z"
  syntax logic (-)  "(%1 - %2)%Z"
  syntax logic (*)  "(%1 * %2)%Z"
  syntax logic (-_) "(-%1)%Z"
MARCHE Claude's avatar
MARCHE Claude committed
46

47 48 49 50
  syntax logic (<=) "(%1 <= %2)%Z"
  syntax logic (<)  "(%1 <  %2)%Z"
  syntax logic (>=) "(%1 >= %2)%Z"
  syntax logic (>)  "(%1 >  %2)%Z"
MARCHE Claude's avatar
MARCHE Claude committed
51 52 53 54 55 56 57 58 59

  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
60 61 62 63
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
MARCHE Claude's avatar
MARCHE Claude committed
64 65
end

MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69 70 71 72 73 74
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

theory real.Real

  syntax logic zero "0%R"
75
  syntax logic one  "1%R"
MARCHE Claude's avatar
MARCHE Claude committed
76

77 78 79 80 81
  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"
MARCHE Claude's avatar
MARCHE Claude committed
82 83
  syntax logic inv  "(Rinv %1)"

84 85 86 87
  syntax logic (<=) "(%1 <= %2)%R"
  syntax logic (<)  "(%1 <  %2)%R"
  syntax logic (>=) "(%1 >= %2)%R"
  syntax logic (>)  "(%1 >  %2)%R"
MARCHE Claude's avatar
MARCHE Claude committed
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109

  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
110 111 112 113 114 115
theory real.FromInt

  syntax logic from_int "(IZR %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
116 117 118 119
theory real.Square

  prelude "Require Import R_sqrt."

120
  syntax logic sqr  "(Rsqr %1)"
MARCHE Claude's avatar
MARCHE Claude committed
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 153 154 155 156 157
  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