coq plugin: Z and R constants

parent 9c35be57
......@@ -37,9 +37,10 @@ end
theory int.Int
prelude "(* this is a prelude for Alt-Ergo arithmetic *)"
prelude "(* this is a prelude for Alt-Ergo integer arithmetic *)"
syntax logic zero "0"
syntax logic one "1"
syntax logic (_+_) "(%1 + %2)"
syntax logic (_-_) "(%1 - %2)"
......@@ -59,6 +60,45 @@ theory int.Int
remove prop Mul_distr
remove prop Comm.Comm
remove prop Unitary
remove prop Refl
remove prop Trans
remove prop Total
remove prop Antisymm
end
theory real.Real
prelude "(* this is a prelude for Alt-Ergo real arithmetic *)"
syntax logic zero "0.0"
syntax logic one "1.0"
syntax logic (_+_) "(%1 + %2)"
syntax logic (_-_) "(%1 - %2)"
syntax logic (_*_) "(%1 * %2)"
syntax logic (_/_) "(%1 / %2)"
syntax logic (-_) "(-%1)"
syntax logic inv "(1.0 / %1)"
syntax logic (_<=_) "(%1 <= %2)"
syntax logic (_<_) "(%1 < %2)"
syntax logic (_>=_) "(%1 >= %2)"
syntax logic (_>_) "(%1 > %2)"
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 Total
remove prop Antisymm
remove prop Inverse
end
......
Declare ML Module "whytac".
Require Export ZArith.
Open Scope Z_scope.
Goal forall x:Z, x=x.
Require Export Reals.
Print Ropp.
SearchAbout Rinv.
Goal (/1 = 1)%R.
why.
Print Zdiv.
SearchAbout Zdiv_eucl.
Goal forall x:Z, x=1 -> x/1=0.
why.
......@@ -75,18 +75,26 @@ let coq_Rlt = lazy (constant "Rlt")
let coq_Rplus = lazy (constant "Rplus")
let coq_Rmult = lazy (constant "Rmult")
let coq_Ropp = lazy (constant "Ropp")
let coq_Rinv = lazy (constant "Rinv")
let coq_Rminus = lazy (constant "Rminus")
let coq_Rdiv = lazy (constant "Rdiv")
let coq_powerRZ = lazy (constant "powerRZ")
let coq_iff = lazy (constant "iff")
let is_constant t c = try t = Lazy.force c with _ -> false
(* not first-order expressions *)
exception NotFO
(* the task under construction *)
let task = ref None
let why_constant path t s =
let th = Env.find_theory env path t in
task := Task.use_export !task th;
Theory.ns_find_ls th.Theory.th_export s
(* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of
env names, and returns the new variables together with the new
environment *)
......@@ -195,29 +203,45 @@ and tr_term tv bv env t =
tr_arith_constant t
with NotArithConstant -> match kind_of_term t with
(* binary operations on integers *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> *)
(* Plus (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> *)
(* Moins (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> *)
(* Mult (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> *)
(* Div (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a|]) when f = Lazy.force coq_Zopp -> *)
(* Opp (tr_term tv bv env a) *)
| App (c, [|a;b|]) when is_constant c coq_Zplus ->
let ls = why_constant ["int"] "Int" ["infix +"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
| App (c, [|a;b|]) when is_constant c coq_Zminus ->
let ls = why_constant ["int"] "Int" ["infix -"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
| App (c, [|a;b|]) when is_constant c coq_Zmult ->
let ls = why_constant ["int"] "Int" ["infix *"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
| App (c, [|a;b|]) when is_constant c coq_Zdiv ->
let ls = why_constant ["int"] "EuclideanDivision" ["div"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_int
| App (c, [|a|]) when is_constant c coq_Zopp ->
let ls = why_constant ["int"] "Int" ["prefix -"] in
Term.t_app ls [tr_term tv bv env a] Ty.ty_int
(* binary operations on reals *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rplus -> *)
(* Plus (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rminus -> *)
(* Moins (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rmult -> *)
(* Mult (tr_term tv bv env a, tr_term tv bv env b) *)
(* | App (f, [|a;b|]) when f = Lazy.force coq_Rdiv -> *)
(* Div (tr_term tv bv env a, tr_term tv bv env b) *)
| Var id when Idmap.mem id bv ->
Term.t_var (Idmap.find id bv)
| _ ->
assert false (*TODO*)
| App (c, [|a;b|]) when is_constant c coq_Rplus ->
let ls = why_constant ["real"] "Real" ["infix +"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
| App (c, [|a;b|]) when is_constant c coq_Rminus ->
let ls = why_constant ["real"] "Real" ["infix -"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
| App (c, [|a;b|]) when is_constant c coq_Rmult ->
let ls = why_constant ["real"] "Real" ["infix *"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
| App (c, [|a;b|]) when is_constant c coq_Rdiv ->
let ls = why_constant ["real"] "Real" ["infix /"] in
Term.t_app ls [tr_term tv bv env a; tr_term tv bv env b] Ty.ty_real
| App (c, [|a|]) when is_constant c coq_Ropp ->
let ls = why_constant ["real"] "Real" ["prefix -"] in
Term.t_app ls [tr_term tv bv env a] Ty.ty_real
| App (c, [|a|]) when is_constant c coq_Rinv ->
let ls = why_constant ["real"] "Real" ["inv"] in
Term.t_app ls [tr_term tv bv env a] Ty.ty_real
(* first-order terms *)
| Var id when Idmap.mem id bv ->
Term.t_var (Idmap.find id bv)
| _ ->
assert false (*TODO*)
(* let f, cl = decompose_app t in *)
(* begin try *)
(* let r = global_of_constr f in *)
......@@ -271,26 +295,33 @@ and tr_formula tv bv env f =
Term.f_equ (tr_term tv bv env a) (tr_term tv bv env b)
else
raise NotFO
(* comparisons on integers *)
(*
| _, [a;b] when c = Lazy.force coq_Zle ->
Fatom (Le (tr_term tv bv env a, tr_term tv bv env b))
| _, [a;b] when c = Lazy.force coq_Zlt ->
Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b))
| _, [a;b] when c = Lazy.force coq_Zge ->
Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b))
| _, [a;b] when c = Lazy.force coq_Zgt ->
Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b))
(* comparisons on reals *)
| _, [a;b] when c = Lazy.force coq_Rle ->
Fatom (Le (tr_term tv bv env a, tr_term tv bv env b))
| _, [a;b] when c = Lazy.force coq_Rlt ->
Fatom (Lt (tr_term tv bv env a, tr_term tv bv env b))
| _, [a;b] when c = Lazy.force coq_Rge ->
Fatom (Ge (tr_term tv bv env a, tr_term tv bv env b))
| _, [a;b] when c = Lazy.force coq_Rgt ->
Fatom (Gt (tr_term tv bv env a, tr_term tv bv env b))
*)
(* comparisons on integers *)
| _, [a;b] when is_constant c coq_Zle ->
let ls = why_constant ["int"] "Int" ["infix <="] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
| _, [a;b] when is_constant c coq_Zlt ->
let ls = why_constant ["int"] "Int" ["infix <"] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
| _, [a;b] when is_constant c coq_Zge ->
let ls = why_constant ["int"] "Int" ["infix >="] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
| _, [a;b] when is_constant c coq_Zgt ->
let ls = why_constant ["int"] "Int" ["infix >"] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
(* comparisons on reals *)
| _, [a;b] when is_constant c coq_Rle ->
let ls = why_constant ["real"] "Real" ["infix <="] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
| _, [a;b] when is_constant c coq_Rlt ->
let ls = why_constant ["real"] "Real" ["infix <"] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
| _, [a;b] when is_constant c coq_Rge ->
let ls = why_constant ["real"] "Real" ["infix >="] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
| _, [a;b] when is_constant c coq_Rgt ->
let ls = why_constant ["real"] "Real" ["infix >"] in
Term.f_app ls [tr_term tv bv env a; tr_term tv bv env b]
(* propositional logic *)
| _, [] when c = build_coq_False () ->
Term.f_false
| _, [] when c = build_coq_True () ->
......@@ -337,7 +368,7 @@ and tr_formula tv bv env f =
let tr_goal gl =
let f = tr_formula Idmap.empty Idmap.empty (pf_env gl) (pf_concl gl) in
let pr = Decl.create_prsymbol (Ident.id_fresh "goal") in
if debug then Format.printf "%a@." Pretty.print_fmla f;
if debug then Format.printf "---@\n%a@\n---@." Pretty.print_fmla f;
task := Task.add_prop_decl !task Decl.Pgoal pr f
let whytac gl =
......@@ -346,7 +377,7 @@ let whytac gl =
task := Task.use_export None Theory.builtin_theory;
try
tr_goal gl;
Format.printf "@[%a@]@?" (Driver.print_task drv) !task;
if debug then Format.printf "@[%a@]@\n---@." (Driver.print_task drv) !task;
let res = Driver.call_prover ~debug ~timeout drv !task in
match res.pr_answer with
| Valid -> Tactics.admit_as_an_axiom gl
......
......@@ -3,11 +3,12 @@
theory Real
logic (< )(real, real)
logic (<=)(real, real)
logic (> )(real, real)
logic (>=)(real, real)
logic (<=)(x:real, y:real) = x < y or x = y
logic (> )(x:real, y:real) = y < x
logic (>=)(x:real, y:real) = y <= x
(* TODO : they are total order relations *)
clone export relations.TotalOrder with
type t = real, logic rel = (<=)
logic zero : real = 0.0
logic one : real = 1.0
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment