Commit 06a72735 authored by Heiko Becker's avatar Heiko Becker

Add some small docstrings

parent 62fa1565
(**
Full Certtificate Checker.
This function must be run on the daisy output.
**)
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Daisy.Infra.RealSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.PreconditionValidation.
......@@ -8,6 +12,9 @@ Require Export Daisy.Infra.ExpressionAbbrevs.
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
andb (andb (validIntervalbounds e absenv P) (approximatesPrecond e absenv P)) (validErrorbound e absenv).
(**
Soundness proof.
**)
Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P:
forall (cenv:env_ty) (vR:R) (vF:R),
precondValidForExec P cenv ->
......
Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Expressions.
(**
TODO: Check wether we need Rabs (n * machineEpsilon) instead
Proofs of general bounds on the error of arithmetic expressions.
This shortens soundness proofs later.
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Interval.Interval_tactic.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Expressions.
Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R):
forall cenv:nat -> R,
eval_exp 0%R cenv (Const n) nR ->
......@@ -19,10 +21,6 @@ Proof.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
(**
TODO: Maybe improve bound by adding interval constraint and proving that it is leq than maxAbs of bounds
(nlo <= cenv n <= nhi)%R -> (Rabs (nR - nF) <= Rabs ((Rmax (Rabs nlo) (Rabs nhi)) * machineEpsilon))%R.
**)
Lemma param_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R):
eval_exp 0%R cenv (Param R n) nR ->
eval_exp machineEpsilon cenv (Param R n) nF ->
......
(**
Error bound checker and its soundness proof
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals Coq.Lists.List.
(*Coq.QArith.Qcanon.*)
Require Import Coq.micromega.Psatz Coq.Reals.Reals Interval.Interval_tactic.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.RealSimps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArith Daisy.IntervalArithQ.
......@@ -30,10 +32,8 @@ Fixpoint validErrorbound (e:exp Q) (env:analysisResult) :=
end
in andb (andb rec errPos) theVal
end.
(*
Functional Scheme validErrorbound_ind := Induction for validErrorbound Sort Prop.
*)
(** Since errors are intervals with 0 as center, we track them as single value since this eases proving upper bounds **)
Lemma err_always_positive e (absenv:analysisResult) iv err:
validErrorbound e absenv = true ->
(iv,err) = absenv e ->
......
(**
Some rewriting properties for translating between rationals and real numbers.
These are used in the soundness proofs since we want to have the final theorem on the real valued evaluation.
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs Coq.QArith.Qreals.
Require Import Coq.Reals.Reals Coq.micromega.Psatz.
Require Import Flocq.Core.Fcore_Raux.
......@@ -167,17 +171,4 @@ Proof.
unfold machineEpsilon.
apply Qle_bool_iff.
unfold Qle_bool; auto.
Qed.
(*
Lemma errorIsPos:
forall e:error, (0 <= Q2R e)%R.
Proof.
intros e.
unfold error in e.
pose proof (QposGeq0 e).
apply Qle_bool_iff in H.
apply Qle_Rle in H.
rewrite Q2R0_is_0 in H; auto.
Qed.
*)
\ No newline at end of file
Qed.
\ No newline at end of file
......@@ -179,18 +179,6 @@ Proof.
apply interval_negation_valid; auto.
Qed.
(*
FIXME: This needs to be beautified
*)
Definition interval_mult_err (I1:interval) (e1:err) (I2:interval) (e2:err) :=
addInterval
(addInterval
(addInterval
(absIntvUpd Rmult I1 I2)
(absIntvUpd Rmult I1 (e1,e1)))
(absIntvUpd Rmult I2 (e2,e2)))
(Rmult e1 e2, Rmult e1 e2).
Definition multInterval (iv1:interval) (iv2:interval) :=
absIntvUpd Rmult iv1 iv2.
......@@ -275,19 +263,7 @@ Qed.
Definition divideInterval (I1:interval) (I2:interval) :=
multInterval I1 (mkInterval (/ (IVhi I2)) (/ (IVlo I2))).
(*
Corollary interval_divisision_valid (I1:interval) (I2:interval) :
validIntervalDiv I1 I2 (divideInterval I1 I2).
Proof.
unfold validIntervalDiv.
intros a b contained_a contained_b; unfold divideInterval.
apply interval_multiplication_valid; auto.
unfold contained in *; simpl.
split. *)
Definition intv_div_err (I1:interval) (e1:err) (I2:interval) (e2:err) :=
interval_mult_err I1 e1 ( (/ IVlo (I2))%R, (/ IVhi (I2))%R) e2.
(** Define the maxAbs function on R and prove some minor properties of it. **)
Definition RmaxAbsFun (iv:interval) :=
Rmax (Rabs (fst iv)) (Rabs (snd iv)).
......
......@@ -193,18 +193,6 @@ Proof.
apply intv_negation_valid; auto.
Qed.
(*
FIXME: This needs to be beautified
*)
Definition intv_mult_err (I1:intv) (e1:error) (I2:intv) (e2:error) :=
addIntv
(addIntv
(addIntv
(absIvUpd Qmult I1 I2)
(absIvUpd Qmult I1 (e1,e1)))
(absIvUpd Qmult I2 (e2,e2)))
(Qmult e1 e2, Qmult e1 e2).
Definition multIntv (iv1:intv) (iv2:intv) :=
absIvUpd Qmult iv1 iv2.
......@@ -298,17 +286,4 @@ Proof.
Qed.
Definition divideIntv (I1:intv) (I2:intv) :=
multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))).
(*
Corollary intv_divisision_valid (I1:intv) (I2:intv) :
validIntvDiv I1 I2 (divideIntv I1 I2).
Proof.
unfold validIntvDiv.
intros a b contained_a contained_b; unfold divideIntv.
apply intv_multiplication_valid; auto.
unfold contained in *; simpl.
split. *)
Definition iv_div_err (I1:intv) (e1:error) (I2:intv) (e2:error) :=
intv_mult_err I1 e1 ( (/ ivlo (I2))%Q, (/ ivhi (I2))%Q) e2.
\ No newline at end of file
multIntv I1 (mkIntv (/ (ivhi I2)) (/ (ivlo I2))).
\ No newline at end of file
(**
Interval arithmetic checker and its soundness proof
**)
Require Import Coq.QArith.QArith Coq.QArith.Qreals QArith.Qminmax Coq.Lists.List.
Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps.
Require Import Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.RealSimps Daisy.PreconditionValidation.
......@@ -6,8 +9,6 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond):=
let (intv, _) := absenv e in
match e with
| Var v => false
(* let bounds_v := P v in
andb (Qeq_bool (fst intv) (fst (bounds_v))) (Qeq_bool (snd bounds_v) (snd (intv))) *)
| Param v =>
isSupersetIntv (P v) intv
| Const n =>
......
(**
Precondition agreement checker and its soundness proof
**)
Require Import Coq.Reals.Reals Coq.Lists.List Coq.QArith.QArith.
Require Import Daisy.Infra.Abbrevs Daisy.Expressions Daisy.Infra.RationalSimps Daisy.Infra.ExpressionAbbrevs Daisy.IntervalArithQ.
......
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