coq.drv 3.97 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 13 14 15 16 17 18 19 20 21 22
(* À discuter *)
transformation "simplify_recursive_definition"
transformation "inline_trivial"

transformation "eliminate_builtin"
transformation "eliminate_recursion"

transformation "simplify_formula"
transformation "simplify_trivial_quantification_in_goal"


MARCHE Claude's avatar
MARCHE Claude committed
23
theory BuiltIn
MARCHE Claude's avatar
MARCHE Claude committed
24 25 26 27

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

28 29 30
  syntax type   int   "Z"
  syntax type   real  "R"
  syntax logic  (=)   "(%1 = %2)" 
MARCHE Claude's avatar
MARCHE Claude committed
31 32
end

MARCHE Claude's avatar
MARCHE Claude committed
33 34
theory bool.Bool

35
  syntax type bool   "bool"
MARCHE Claude's avatar
MARCHE Claude committed
36

37
  syntax logic True  "true"
MARCHE Claude's avatar
MARCHE Claude committed
38 39
  syntax logic False "false"

40 41 42 43
  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
44 45 46

end

MARCHE Claude's avatar
MARCHE Claude committed
47 48 49 50

theory int.Int

  syntax logic zero "0%Z"
51
  syntax logic one  "1%Z"
MARCHE Claude's avatar
MARCHE Claude committed
52

53 54 55 56
  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
57

58 59 60 61
  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
62 63 64 65 66 67 68 69 70

  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
71 72 73 74
  remove prop Refl
  remove prop Trans
  remove prop Antisymm
  remove prop Total
75 76 77 78
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult

MARCHE Claude's avatar
MARCHE Claude committed
79 80
end

MARCHE Claude's avatar
MARCHE Claude committed
81 82 83 84 85 86
theory int.Abs

  syntax logic abs "(Zabs %1)"

end

87 88
theory int.EuclideanDivision

MARCHE Claude's avatar
MARCHE Claude committed
89
  prelude "Require Import Zdiv."
90 91 92 93 94 95 96 97

  syntax logic div "(Zdiv %1 %2)"
  syntax logic mod "(Zmod %1 %2)"

end

theory int.ComputerDivision

MARCHE Claude's avatar
MARCHE Claude committed
98
  prelude "Require Import ZOdiv."
99 100 101 102 103 104 105

  syntax logic div "(ZOdiv %1 %2)"
  syntax logic mod "(ZOmod %1 %2)"

end


MARCHE Claude's avatar
MARCHE Claude committed
106 107 108
theory real.Real

  syntax logic zero "0%R"
109
  syntax logic one  "1%R"
MARCHE Claude's avatar
MARCHE Claude committed
110

111 112 113 114 115
  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
116 117
  syntax logic inv  "(Rinv %1)"

118 119 120 121
  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
122 123 124 125 126 127 128 129 130 131

  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
132 133 134
  remove prop NonTrivialRing
  remove prop CompatOrderAdd
  remove prop CompatOrderMult
MARCHE Claude's avatar
MARCHE Claude committed
135 136 137

end

MARCHE Claude's avatar
MARCHE Claude committed
138 139 140 141 142 143 144 145 146 147 148 149 150 151
theory real.RealInfix

  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 (<=.) "(%1 <= %2)%R"
  syntax logic (<.)  "(%1 <  %2)%R"
  syntax logic (>=.) "(%1 >= %2)%R"
  syntax logic (>.)  "(%1 >  %2)%R"

end
MARCHE Claude's avatar
MARCHE Claude committed
152 153 154 155 156 157 158 159 160

theory real.Abs

  prelude "Require Import Rbasic_fun."

  syntax logic abs "(Rabs %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
161 162 163 164 165 166
theory real.FromInt

  syntax logic from_int "(IZR %1)"

end

MARCHE Claude's avatar
MARCHE Claude committed
167 168 169 170
theory real.Square

  prelude "Require Import R_sqrt."

171
  syntax logic sqr  "(Rsqr %1)"
MARCHE Claude's avatar
MARCHE Claude committed
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208
  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