Commit 91277a12 authored by MARCHE Claude's avatar MARCHE Claude

Fixed the pseudo coq-realize prover. But do we really want that ?

parent 8d448d00
valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
prelude "Require Import ZArith."
prelude "Require Import Rbase."
syntax type int "Z"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
theory bool.Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax function andb "(andb %1 %2)"
syntax function orb "(orb %1 %2)"
syntax function xorb "(xorb %1 %2)"
syntax function notb "(negb %1)"
end
theory int.Int
syntax function zero "0%Z"
syntax function one "1%Z"
syntax function (+) "(%1 + %2)%Z"
syntax function (-) "(%1 - %2)%Z"
syntax function (*) "(%1 * %2)%Z"
syntax function (-_) "(-%1)%Z"
syntax predicate (<=) "(%1 <= %2)%Z"
syntax predicate (<) "(%1 < %2)%Z"
syntax predicate (>=) "(%1 >= %2)%Z"
syntax predicate (>) "(%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
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
end
theory int.Abs
syntax function abs "(Zabs %1)"
remove prop Abs_pos
end
theory int.MinMax
syntax function min "(Zmin %1 %2)"
syntax function max "(Zmax %1 %2)"
end
(* removed: Coq Zdiv is NOT true Euclidean division:
Zmod can be negative, in fact (Zmod x y) has the same sign as y,
which is not the usual convention of programming language either.
theory int.EuclideanDivision
prelude "Require Import Zdiv."
syntax function div "(Zdiv %1 %2)"
syntax function mod "(Zmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Mod_1
remove prop Div_1
end
*)
theory int.ComputerDivision
(* Coq Z0div provides the division and modulo operators
with the same convention as mainstream programming language
such C, Java, OCaml *)
prelude "Require Import ZOdiv."
syntax function div "(ZOdiv %1 %2)"
syntax function mod "(ZOmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Div_sign_pos
remove prop Div_sign_neg
remove prop Mod_sign_pos
remove prop Mod_sign_neg
remove prop Rounds_toward_zero
remove prop Div_1
remove prop Mod_1
remove prop Div_inf
remove prop Mod_inf
remove prop Div_mult
remove prop Mod_mult
end
theory real.Real
syntax function zero "0%R"
syntax function one "1%R"
syntax function (+) "(%1 + %2)%R"
syntax function (-) "(%1 - %2)%R"
syntax function (-_) "(-%1)%R"
syntax function (*) "(%1 * %2)%R"
syntax function (/) "(Rdiv %1 %2)%R"
syntax function inv "(Rinv %1)"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
syntax predicate (>=) "(%1 >= %2)%R"
syntax predicate (>) "(%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
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop assoc_mul_div
remove prop assoc_div_mul
remove prop assoc_div_div
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)%R"
syntax function (-.) "(%1 - %2)%R"
syntax function (-._) "(-%1)%R"
syntax function ( *.) "(%1 * %2)%R"
syntax function (/.) "(%1 / %2)%R"
syntax predicate (<=.) "(%1 <= %2)%R"
syntax predicate (<.) "(%1 < %2)%R"
syntax predicate (>=.) "(%1 >= %2)%R"
syntax predicate (>.) "(%1 > %2)%R"
end
theory real.Abs
prelude "Require Import Rbasic_fun."
syntax function abs "(Rabs %1)"
remove prop Abs_le
remove prop Abs_pos
end
theory real.FromInt
syntax function from_int "(IZR %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Square
prelude "Require Import R_sqrt."
syntax function sqr "(Rsqr %1)"
syntax function sqrt "(sqrt %1)" (* and not Rsqrt *)
remove prop Sqrt_positive
remove prop Sqrt_square
remove prop Square_sqrt
end
theory real.ExpLog
prelude "Require Import Rtrigo_def."
prelude "Require Import Rpower."
syntax function exp "(exp %1)"
syntax function log "(ln %1)"
remove prop Exp_zero
remove prop Exp_sum
remove prop Log_one
remove prop Log_mul
remove prop Log_exp
remove prop Exp_log
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 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
printer "coq-realize"
filename "%f_%t_%g.v"
valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
prelude "(* This file is generated by Why3's Coq driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
prelude "Require Import ZArith."
prelude "Require Import Rbase."
syntax type int "Z"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
theory bool.Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax function andb "(andb %1 %2)"
syntax function orb "(orb %1 %2)"
syntax function xorb "(xorb %1 %2)"
syntax function notb "(negb %1)"
end
theory int.Int
syntax function zero "0%Z"
syntax function one "1%Z"
syntax function (+) "(%1 + %2)%Z"
syntax function (-) "(%1 - %2)%Z"
syntax function (*) "(%1 * %2)%Z"
syntax function (-_) "(-%1)%Z"
syntax predicate (<=) "(%1 <= %2)%Z"
syntax predicate (<) "(%1 < %2)%Z"
syntax predicate (>=) "(%1 >= %2)%Z"
syntax predicate (>) "(%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
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
end
theory int.Abs
syntax function abs "(Zabs %1)"
remove prop Abs_pos
end
theory int.MinMax
syntax function min "(Zmin %1 %2)"
syntax function max "(Zmax %1 %2)"
end
(* removed: Coq Zdiv is NOT true Euclidean division:
Zmod can be negative, in fact (Zmod x y) has the same sign as y,
which is not the usual convention of programming language either.
theory int.EuclideanDivision
prelude "Require Import Zdiv."
syntax function div "(Zdiv %1 %2)"
syntax function mod "(Zmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Mod_1
remove prop Div_1
end
*)
theory int.ComputerDivision
(* Coq Z0div provides the division and modulo operators
with the same convention as mainstream programming language
such C, Java, OCaml *)
prelude "Require Import ZOdiv."
syntax function div "(ZOdiv %1 %2)"
syntax function mod "(ZOmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Div_sign_pos
remove prop Div_sign_neg
remove prop Mod_sign_pos
remove prop Mod_sign_neg
remove prop Rounds_toward_zero
remove prop Div_1
remove prop Mod_1
remove prop Div_inf
remove prop Mod_inf
remove prop Div_mult
remove prop Mod_mult
end
theory real.Real
syntax function zero "0%R"
syntax function one "1%R"
syntax function (+) "(%1 + %2)%R"
syntax function (-) "(%1 - %2)%R"
syntax function (-_) "(-%1)%R"
syntax function (*) "(%1 * %2)%R"
syntax function (/) "(Rdiv %1 %2)%R"
syntax function inv "(Rinv %1)"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
syntax predicate (>=) "(%1 >= %2)%R"
syntax predicate (>) "(%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
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop assoc_mul_div
remove prop assoc_div_mul
remove prop assoc_div_div
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)%R"
syntax function (-.) "(%1 - %2)%R"
syntax function (-._) "(-%1)%R"
syntax function ( *.) "(%1 * %2)%R"
syntax function (/.) "(%1 / %2)%R"
syntax predicate (<=.) "(%1 <= %2)%R"
syntax predicate (<.) "(%1 < %2)%R"
syntax predicate (>=.) "(%1 >= %2)%R"
syntax predicate (>.) "(%1 > %2)%R"
end
theory real.Abs
prelude "Require Import Rbasic_fun."
syntax function abs "(Rabs %1)"
remove prop Abs_le
remove prop Abs_pos
end
theory real.FromInt
syntax function from_int "(IZR %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Square
prelude "Require Import R_sqrt."
syntax function sqr "(Rsqr %1)"
syntax function sqrt "(sqrt %1)" (* and not Rsqrt *)
remove prop Sqrt_positive
remove prop Sqrt_square
remove prop Square_sqrt
end
theory real.ExpLog
prelude "Require Import Rtrigo_def."
prelude "Require Import Rpower."
syntax function exp "(exp %1)"
syntax function log "(ln %1)"
remove prop Exp_zero
remove prop Exp_sum
remove prop Log_one
remove prop Log_mul
remove prop Log_exp
remove prop Exp_log
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 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 ?" *)
printer "coq-realize"
filename "%t.v"
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
import "coq-common.drv"
end
printer "coq"
filename "%f_%t_%g.v"
valid 0
unknown "Error: \\(.*\\)$" "\\1"
fail "Syntax error: \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
prelude "(* This file is generated by Why3's Coq driver *)"
prelude "(* Beware! Only edit allowed sections below *)"
(* À discuter *)
(*transformation "simplify_recursive_definition"*)
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "simplify_formula"
(*transformation "simplify_trivial_quantification_in_goal"*)
theory BuiltIn
prelude "Require Import ZArith."
prelude "Require Import Rbase."
syntax type int "Z"
syntax type real "R"
syntax predicate (=) "(%1 = %2)"
end
theory bool.Bool
syntax type bool "bool"
syntax function True "true"
syntax function False "false"
syntax function andb "(andb %1 %2)"
syntax function orb "(orb %1 %2)"
syntax function xorb "(xorb %1 %2)"
syntax function notb "(negb %1)"
end
theory int.Int
syntax function zero "0%Z"
syntax function one "1%Z"
syntax function (+) "(%1 + %2)%Z"
syntax function (-) "(%1 - %2)%Z"
syntax function (*) "(%1 * %2)%Z"
syntax function (-_) "(-%1)%Z"
syntax predicate (<=) "(%1 <= %2)%Z"
syntax predicate (<) "(%1 < %2)%Z"
syntax predicate (>=) "(%1 >= %2)%Z"
syntax predicate (>) "(%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
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
end
theory int.Abs
syntax function abs "(Zabs %1)"
remove prop Abs_pos
end
theory int.MinMax
syntax function min "(Zmin %1 %2)"
syntax function max "(Zmax %1 %2)"
end
(* removed: Coq Zdiv is NOT true Euclidean division:
Zmod can be negative, in fact (Zmod x y) has the same sign as y,
which is not the usual convention of programming language either.
theory int.EuclideanDivision
prelude "Require Import Zdiv."
syntax function div "(Zdiv %1 %2)"
syntax function mod "(Zmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Mod_1
remove prop Div_1
end
*)
theory int.ComputerDivision
(* Coq Z0div provides the division and modulo operators
with the same convention as mainstream programming language
such C, Java, OCaml *)
prelude "Require Import ZOdiv."
syntax function div "(ZOdiv %1 %2)"
syntax function mod "(ZOmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Div_sign_pos
remove prop Div_sign_neg
remove prop Mod_sign_pos
remove prop Mod_sign_neg
remove prop Rounds_toward_zero
remove prop Div_1
remove prop Mod_1
remove prop Div_inf
remove prop Mod_inf
remove prop Div_mult
remove prop Mod_mult
end
theory real.Real
syntax function zero "0%R"
syntax function one "1%R"
syntax function (+) "(%1 + %2)%R"
syntax function (-) "(%1 - %2)%R"
syntax function (-_) "(-%1)%R"
syntax function (*) "(%1 * %2)%R"
syntax function (/) "(Rdiv %1 %2)%R"
syntax function inv "(Rinv %1)"
syntax predicate (<=) "(%1 <= %2)%R"
syntax predicate (<) "(%1 < %2)%R"
syntax predicate (>=) "(%1 >= %2)%R"
syntax predicate (>) "(%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
remove prop NonTrivialRing
remove prop CompatOrderAdd
remove prop CompatOrderMult
remove prop Refl
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop assoc_mul_div
remove prop assoc_div_mul
remove prop assoc_div_div
end
theory real.RealInfix
syntax function (+.) "(%1 + %2)%R"
syntax function (-.) "(%1 - %2)%R"
syntax function (-._) "(-%1)%R"
syntax function ( *.) "(%1 * %2)%R"
syntax function (/.) "(%1 / %2)%R"
syntax predicate (<=.) "(%1 <= %2)%R"
syntax predicate (<.) "(%1 < %2)%R"
syntax predicate (>=.) "(%1 >= %2)%R"
syntax predicate (>.) "(%1 > %2)%R"
end
theory real.Abs
prelude "Require Import Rbasic_fun."