Commit be4c3a5c authored by Heiko Becker's avatar Heiko Becker

Documentation for Infra directories

parent f5ba4315
(**
Some type abbreviations, to ease writing
This file contains some type abbreviations, to ease writing.
**)
Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qreals.
(**
......
(**
Some abbreviations that require having defined expressions beforehand
Some abbreviations that require having defined expressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
**)
Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals.
Require Export Daisy.Infra.Abbrevs Daisy.Expressions.
......
(**
Some simplification properties of rationals, not proven in the Standard Library
**)
Require Import Coq.QArith.QArith Coq.QArith.Qminmax Coq.QArith.Qabs.
Require Import Daisy.Infra.Abbrevs.
......@@ -6,60 +9,17 @@ Definition Qeqb := Qeq_bool.
Definition machineEpsilon := (1#(2^53)).
(*
Definition Qc2Q (q:Qc) :Q := match q with
Qcmake a P => a end.
Definition maxAbs (iv:intv) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Lemma double_inject_eq:
forall q, Qc2Q (Q2Qc q) = Qred q.
Proof.
intros q. unfold Q2Qc.
unfold Qc2Q; auto.
Qed. *)
(*
Definition Qcmax (a:Qc) (b:Qc) := Q2Qc (Qmax a b).
Definition Qcabs (a:Qc) := Q2Qc (Qabs a). *)
Definition maxAbs (iv:intv) :=
Qmax (Qabs (fst iv)) (Qabs (snd iv)).
Lemma maxAbs_pointIntv a:
maxAbs (a,a) == Qabs a.
Proof.
unfold maxAbs; simpl.
(* unfold Qcmax.
unfold Qcabs.
apply Qc_is_canon.
apply Qabs_case; intros.
- pose proof (Q.max_id (Qred a)).
unfold Q2Qc; simpl.
rewrite H0.
rewrite Qred_involutive; apply Qeq_refl.
- pose proof (Q.max_id (Qred (-a))).
unfold Q2Qc; simpl.
rewrite H0.
rewrite Qred_involutive.
apply Qeq_refl.
Qed. *)
apply Qabs_case; intros; eapply Q.max_id.
Qed.
(*
Lemma abs_QR (n:Qc):
Rabs (Q2R n) = Q2R (Qcabs n).
Proof.
unfold Rabs.
unfold Qcabs.
apply Qabs_case; intros.
- destruct Rcase_abs.
+ apply Qle_Rle in H.
unfold Q2R at 1 in H.
unfold Qabs.
simpl.
*)
Lemma maxAbs_pointIntv a:
maxAbs (a,a) == Qabs a.
Proof.
unfold maxAbs; simpl.
apply Qabs_case; intros; eapply Q.max_id.
Qed.
Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) :
Lemma Qsub_eq_Qopp_Qplus (a:Q) (b:Q) :
(a - b = a + (- b))%Q.
Proof.
field_simplify; reflexivity.
......
......@@ -4,7 +4,6 @@ These are used in the soundness proofs since we want to have the final theorem o
**)
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.*)
Require Import Daisy.Infra.RationalSimps Daisy.Infra.Abbrevs Daisy.Expressions Daisy.IntervalArith.
Fixpoint toRExp (e:exp Q) :=
......
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid.
Require Import Daisy.Infra.RealConstruction.
(**
TODO REORDER AND DOCUMENT
Some simplification properties of real numbers, not proven in the Standard Library
**)
Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.Setoids.Setoid.
Require Import Daisy.Infra.RealConstruction.
Lemma Rsub_eq_Ropp_Rplus (a:R) (b:R) :
(a - b = a + (- b))%R.
Proof.
......
(*
Some type abbreviations, to ease writing.
Additionally define getter functions to make stuff more portable if we change the infrastructure later.
*)
(**
This file contains some type abbreviations, to ease writing.
**)
new_type_abbrev ("interval", `:real#real`);;
new_type_abbrev ("err", `:real`);;
new_type_abbrev ("intv", `:real#real`);;
......
(**
Some abbreviations that require having defined expressions beforehand
If we would put them in the Abbrevs file, this would create a circular dependency which Coq cannot resolve.
**)
needs "Infra/Abbrevs.hl";;
needs "Expressions.hl";;
......
(* POW IS INFIX IN HOL LIGHT! DUMB IDEA! *)
(**
Abbreviations for construction proper real numbers from injected natural numbers
**)
let negPow = define
`negPow (base:num) (exp:num) = (&1) / ((&base) pow exp)`;;
let realFromNum = define
......
(**
Some simplification properties of real numbers, not proven in the Standard Library
**)
needs "Infra/tactics.hl";;
let REAL_MUL_LE_COMPAT_NEG_L =
......
(**
Custom conversions to simulate evaluation of the certificate checker on the inputs
Used only inside the printed certificates
**)
(* Define a list containing all defined functions, that need to be unfolded while evaluating *)
let Checker_Rewrites =
[CertificateChecker;validIntervalbounds; validErrorbound;
......
(**
tactics library used in the proofs in the framework to ease writing the proofs.
**)
(*
First some tactics that can only work on goals
*)
......
(**
Add printers to HOL-Light to be able to print terms annotated with their terms.
Snippet obtained from HOL-Light mailing list.
https://sourceforge.net/p/hol/mailman/message/35203735/
Code taken from the Flyspeck project.
**)
let print_varandtype fmt tm =
let hop,args = strip_comb tm in
let s = name_of hop
......
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