Commit e367b4b4 authored by MARCHE Claude's avatar MARCHE Claude

Coq proofs can be given a context

parent 4b48e6c9
......@@ -6,6 +6,15 @@ Require Import Rbasic_fun.
Require Import R_sqrt.
Require Import Rtrigo.
Require Import AltSeries. (* for def of pi *)
Axiom assoc_mul_div : forall (x:R) (y:R) (z:R), (~ (z = (0)%R)) ->
((Rdiv (x * y)%R z)%R = (x * (Rdiv y z)%R)%R).
Axiom assoc_div_mul : forall (x:R) (y:R) (z:R), ((~ (y = (0)%R)) /\
~ (z = (0)%R)) -> ((Rdiv (Rdiv x y)%R z)%R = (Rdiv x (y * z)%R)%R).
Axiom assoc_div_div : forall (x:R) (y:R) (z:R), ((~ (y = (0)%R)) /\
~ (z = (0)%R)) -> ((Rdiv x (Rdiv y z)%R)%R = (Rdiv (x * z)%R y)%R).
Axiom Abs_le : forall (x:R) (y:R), ((Rabs x) <= y)%R <-> (((-y)%R <= x)%R /\
(x <= y)%R).
......@@ -129,11 +138,14 @@ Axiom Round_down_neg : forall (x:R), ((round (Down ) (-x)%R) = (-(round (Up )
Axiom Round_up_neg : forall (x:R), ((round (Up ) (-x)%R) = (-(round (Down )
x))%R).
(* YOU MAY EDIT THE CONTEXT BELOW *)
Require Import Interval_tactic.
(* DO NOT EDIT BELOW *)
Theorem MethodError : forall (x:R), ((Rabs x) <= (1 / 32)%R)%R ->
((Rabs (((1)%R - ((05 / 10)%R * (x * x)%R)%R)%R - (Rtrigo_def.cos x))%R) <= (1 / 16777216)%R)%R.
(* YOU MAY EDIT THE PROOF BELOW *)
intros x H.
Require Import Interval_tactic.
interval with (i_bisect_diff x).
Qed.
(* DO NOT EDIT BELOW *)
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="examples/my_cosine/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../my_cosine.why" verified="true" expanded="true">
<theory name="CosineSingle" verified="true" expanded="true">
<goal name="MethodError" sum="04d7ba2ad67e6273c77266e812fe0b5d" proved="true" expanded="true">
<goal name="MethodError" sum="04d7ba2ad67e6273c77266e812fe0b5d" proved="true" expanded="true" shape="ainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *V0V0acosV0c0x1.p-24Iainfix <=aabsV0c0x1.p-5F">
<proof prover="coq" timelimit="2" edited="my_cosine_CosineSingle_MethodError_1.v" obsolete="false">
<result status="valid" time="3.63"/>
<result status="valid" time="3.61"/>
</proof>
</goal>
<goal name="TotalErrorFullyExpanded" sum="86136c1aa7501342a2789f26b4088e3b" proved="true" expanded="true">
<goal name="TotalErrorFullyExpanded" sum="86136c1aa7501342a2789f26b4088e3b" proved="true" expanded="true" shape="ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix =V3aroundaNearestTiesToEvenainfix -c1.0V2Iainfix =V2aroundaNearestTiesToEvenainfix *c0.5V1Iainfix =V1aroundaNearestTiesToEvenainfix *avalueV0avalueV0FIainfix <=aabsainfix -ainfix -c1.0ainfix *c0.5ainfix *avalueV0avalueV0acosavalueV0c0x1.p-24Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="gappa" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="TotalErrorExpanded" sum="1d2075874f81d542bc1500ae6147faec" proved="true" expanded="true">
<goal name="TotalErrorExpanded" sum="1d2075874f81d542bc1500ae6147faec" proved="true" expanded="true" shape="LaroundaNearestTiesToEvenainfix *avalueV0avalueV0LaroundaNearestTiesToEvenainfix *c0.5V1LaroundaNearestTiesToEvenainfix -c1.0V2ainfix <=aabsainfix -V3acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.72"/>
<result status="valid" time="0.80"/>
</proof>
</goal>
<goal name="TotalError" sum="84d328c047b191246fda42eaa2ab5255" proved="true" expanded="true">
<goal name="TotalError" sum="84d328c047b191246fda42eaa2ab5255" proved="true" expanded="true" shape="Lacos_singleV0ainfix <=aabsainfix -avalueV1acosavalueV0c0x1.p-23Iainfix <=aabsavalueV0c0x1.p-5F">
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="2.06"/>
<result status="valid" time="2.13"/>
</proof>
</goal>
</theory>
......
......@@ -348,8 +348,57 @@ let print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params =
let definition fmt info =
fprintf fmt "%s" (if info.realization then "Definition" else "Parameter")
(*
copy of old user scripts
*)
let copy_user_script begin_string end_string ch fmt =
fprintf fmt "%s@\n" begin_string;
try
while true do
let s = input_line ch in
fprintf fmt "%s@\n" s;
if s = end_string then raise Exit
done
with
| Exit -> fprintf fmt "@\n"
| End_of_file -> fprintf fmt "%s@\n@\n" end_string
let proof_begin = "(* YOU MAY EDIT THE PROOF BELOW *)"
let proof_end = "(* DO NOT EDIT BELOW *)"
let context_begin = "(* YOU MAY EDIT THE CONTEXT BELOW *)"
let context_end = "(* DO NOT EDIT BELOW *)"
(* current kind of script in an old file *)
type old_file_state = InContext | InProof | NoWhere
let copy_proof s ch fmt =
copy_user_script proof_begin proof_end ch fmt;
s := NoWhere
let copy_context s ch fmt =
copy_user_script context_begin context_end ch fmt;
s := NoWhere
let lookup_context_or_proof old_state old_channel =
match !old_state with
| InProof | InContext -> ()
| NoWhere ->
let rec loop () =
let s = input_line old_channel in
if s = proof_begin then old_state := InProof else
if s = context_begin then old_state := InContext else
loop ()
in
try loop ()
with End_of_file -> ()
let print_empty_context fmt =
fprintf fmt "%s@\n" context_begin;
fprintf fmt "@\n";
fprintf fmt "%s@\n@\n" context_end
let print_empty_proof ?(def=false) fmt =
fprintf fmt "%s@\n" proof_begin;
......@@ -358,6 +407,7 @@ let print_empty_proof ?(def=false) fmt =
fprintf fmt "%s.@\n" (if def then "Defined" else "Qed");
fprintf fmt "%s@\n@\n" proof_end
(*
let print_next_proof ?def ch fmt =
try
while true do
......@@ -375,7 +425,40 @@ let print_next_proof ?def ch fmt =
with
| End_of_file -> print_empty_proof ?def fmt
| Exit -> fprintf fmt "@\n"
*)
let print_context ~old fmt =
match old with
| None -> print_empty_context fmt
| Some(s,ch) ->
lookup_context_or_proof s ch;
match !s with
| InProof | NoWhere -> print_empty_context fmt
| InContext -> copy_context s ch fmt
let print_proof ~old ?def fmt =
match old with
| None -> print_empty_proof ?def fmt
| Some(s,ch) ->
lookup_context_or_proof s ch;
match !s with
| InContext | NoWhere -> print_empty_proof ?def fmt
| InProof -> copy_proof s ch fmt
let produce_remaining_contexts_and_proofs ~old fmt =
match old with
| None -> ()
| Some(s,ch) ->
let rec loop () =
lookup_context_or_proof s ch;
match !s with
| NoWhere -> ()
| InContext -> copy_context s ch fmt; loop ()
| InProof -> copy_proof s ch fmt; loop ()
in
loop ()
(*
let produce_remaining_proofs ~old fmt =
match old with
| None -> ()
......@@ -400,17 +483,20 @@ let produce_remaining_proofs ~old fmt =
done
with
| End_of_file -> fprintf fmt "@\n"
*)
let realization ~old ?def fmt produce_realization =
if produce_realization then
print_proof ~old ?def fmt
(*
begin match old with
| None -> print_empty_proof ?def fmt
| Some ch -> print_next_proof ?def ch fmt
end
*)
else
fprintf fmt "@\n"
let print_type_decl ~old info fmt (ts,def) =
if is_ts_tuple ts then () else
match def with
......@@ -540,6 +626,13 @@ let print_proof ~old info fmt = function
realization ~old fmt info.realization
| Pskip -> ()
let print_proof_context ~old info fmt = function
| Plemma | Pgoal ->
print_context ~old fmt
| Paxiom ->
if info.realization then print_context ~old fmt
| Pskip -> ()
let print_decl ~old info fmt d = match d.d_node with
| Dtype tl ->
print_list nothing (print_type_decl ~old info) fmt tl
......@@ -552,6 +645,7 @@ let print_decl ~old info fmt d = match d.d_node with
| Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem ->
()
| Dprop (k,pr,f) ->
print_proof_context ~old info fmt k;
let params = t_ty_freevars Stv.empty f in
fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a"
(print_pkind info) k
......@@ -572,6 +666,10 @@ let print_task _env pr thpr ?old fmt task =
info_rem = get_remove_set task;
realization = false;
} in
let old = match old with
| None -> None
| Some ch -> Some(ref NoWhere,ch)
in
print_decls ~old info fmt (Task.task_decls task)
let () = register_printer "coq" print_task
......@@ -610,8 +708,12 @@ let print_theory _env pr thpr ?old fmt th =
realization = true;
}
in
let old = match old with
| None -> None
| Some ch -> Some(ref NoWhere,ch)
in
print_tdecls ~old info fmt th.th_decls;
produce_remaining_proofs ~old fmt
produce_remaining_contexts_and_proofs ~old fmt
(*
......
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