Big cleanup in Coq dev

coq/abs_err.v → coq/AbsoluteError.v

@@ -3,7 +3,8 @@
   used to verify analsysis result in the final theorem of a certificate.
  **)
 Require Import Coq.Reals.Reals.
-Require Import Daisy.daisy_lang Daisy.exps Daisy.Infra.abbrevs Daisy.newIntervalArith.
+Require Import Daisy.Infra.Abbrevs Daisy.Infra.RealConstruction.
+Require Import Daisy.IntervalArith Daisy.Expressions Daisy.Commands.
 
 Definition abs_env:Type := exp R -> interval -> err -> Prop.
 

coq/daisy_lang.v → coq/Commands.v

@@ -2,7 +2,7 @@
  Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
  **)
 Require Import Coq.Reals.Reals.
-Require Import Daisy.exps.
+Require Import Daisy.Expressions.
 (**
   Next define what a program is.
   Currently no loops, only conditionals and assignments

coq/exps.v → coq/Expressions.v

@@ -2,7 +2,7 @@
 Formalization of the base expression language for the daisy framework
  **)
 Require Import Coq.Reals.Reals Interval.Interval_tactic.
-Require Import Daisy.realConversion.
+Require Import Daisy.Infra.RealConstruction.
 Set Implicit Arguments.
 (**
   Expressions will use binary operators.
@@ -138,7 +138,7 @@ Proof.
   - apply Rabs_pos.
   - assert (Rabs machineEpsilon = machineEpsilon).
     + unfold machineEpsilon.
-      unfold realFromNum, negPow.
+      unfold realFromNum, negativePower.
       unfold Rabs.
       destruct Rcase_abs; auto.
       exfalso.
@@ -155,7 +155,9 @@ Lemma var_abs_err_bounded (n:nat) (nR:R) (nF:R) (cenv:nat->R) (nlo:R) (nhi:R):
 Proof.
   intros [lo_le_env env_le_hi] eval_real eval_float.
   inversion eval_real; subst.
-  rewrite perturb_0_val.
+  (* rewrite perturb_0_val. *)
+Admitted.
+
 (**
   Using the parametric expressions, define boolean expressions for conditionals
 **)

coq/Infra/RealConstruction.v

+Require Import Coq.Reals.Reals.
+
+(**
+  Abbreviations for construction proper real numbers from injected natural numbers
+**)
+Definition negativePower (base:R) (exp:nat) :R := 1 / (pow base exp).
+Definition realFromNum (n:R) (unitsBehindColon:nat) (exp:nat) :=
+  (n * (negativePower (10)%R unitsBehindColon) * (negativePower (2)%R exp))%R.
\ No newline at end of file

coq/Infra/abbrevs.v.d

-Infra/abbrevs.vo Infra/abbrevs.glob Infra/abbrevs.v.beautified: Infra/abbrevs.v
-Infra/abbrevs.vio: Infra/abbrevs.v

coq/newIntervalArith.v → coq/IntervalArith.v

@@ -3,7 +3,7 @@
   TODO: Package this into a class or module that depends only on proving the existence of basic operators instead
 **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz.
-Require Import Daisy.Infra.abbrevs.
+Require Import Daisy.Infra.Abbrevs Daisy.Expressions.
 (**
   Intervals are a type, consisting of a pair of two real numbers
   Additionally add some constructing and destructing definitions for encapsulation and
@@ -185,8 +185,7 @@ Proof.
   unfold substractInterval.
   intros a b.
   intros contained_1 contained_I2.
-  rewrite Rsub_eq_Ropp_plus.
-  rewrite simpl_eq.
+  rewrite Rsub_eq_Ropp_Rplus.
   apply additionIsValid; auto.
   apply negationIsValid; auto.
 Qed.

coq/simple_doppler.v → coq/SimpleDoppler.v

 Require Import Coq.Reals.Reals Interval.Interval_tactic Coq.micromega.Psatz.
-Require Import Daisy.abs_err Daisy.daisy_lang Daisy.newIntervalArith Daisy.exps Daisy.realConversion.
+Require Import Daisy.AbsoluteError Daisy.Commands Daisy.IntervalArith Daisy.Expressions Daisy.Infra.RealConstruction.
 
 (*
 [  Info  ]
@@ -69,18 +69,18 @@ Proof.
       apply (AbsErrConst cst1 (mkInterval cst1 cst1) errCst1); [constructor | ].
       unfold isSoundErr; simpl.
       unfold errCst1, cst1, machineEpsilon.
-      assert (1657 / 5 >= 0)%R by (unfold realFromNum, negPow; interval).
+      assert (1657 / 5 >= 0)%R by (unfold realFromNum, negativePower; interval).
       unfold Rabs;
       destruct Rcase_abs as [lt_plus | ge_plus];
       [ exfalso; apply Rlt_not_le in lt_plus; apply lt_plus; apply Rge_le in H; auto | ].
       rewrite Rmax_left; [ | apply Req_le; auto].
-      unfold realFromNum, negPow.
+      unfold realFromNum, negativePower.
       interval.
     + apply (AbsErrVar u (mkInterval (- 100) (100)) errVaru); [constructor | ].
       unfold isSoundErr; simpl.
       unfold machineEpsilon, errVaru.
       unfold realFromNum.
-      unfold negPow.
+      unfold negativePower.
       assert (Rabs (-100) = 100%R) by (unfold Rabs; destruct Rcase_abs; lra).
       rewrite H.
       assert (Rabs 100 = 100)%R by (unfold Rabs; destruct Rcase_abs; lra).
@@ -106,7 +106,7 @@ Proof.
         apply Req_le; auto.
       * unfold isSoundErr; simpl.
         unfold lowerBoundAddUCst, upperBoundAddUCst, errAddUCst.
-        unfold machineEpsilon, realFromNum, negPow.
+        unfold machineEpsilon, realFromNum, negativePower.
         assert (0 <= (1157/5))%R by interval.
         assert (0 <= (2157/5))%R by interval.
         repeat rewrite Rabs_pos_eq; auto.
@@ -131,11 +131,11 @@ Proof.
         by (apply additionIsValid; auto).
     assert (contained (errCst1) (mkInterval (-errCst1) (errCst1))) as errCst1Contained.
     + unfold contained; simpl; split.
-      * unfold errCst1. unfold realFromNum. unfold negPow. interval.
+      * unfold errCst1. unfold realFromNum. unfold negativePower. interval.
       * apply Req_le; auto.
     + assert (contained (errVaru) (mkInterval (-errVaru) (errVaru)))
         as errVaruContained
-          by (split; [ simpl; unfold errVaru, realFromNum, negPow; interval | apply Req_le; auto]).
+          by (split; [ simpl; unfold errVaru, realFromNum, negativePower; interval | apply Req_le; auto]).
       assert (contained (cst1 + errCst1) (addInterval (mkInterval cst1 cst1) (mkInterval (-errCst1) (errCst1))))
         as floatCst1Contained
           by (apply additionIsValid; auto).
@@ -149,7 +149,7 @@ Proof.
           by (apply additionIsValid; auto).
       assert (contained errAddUCst (mkInterval (- errAddUCst) errAddUCst))
         as errAddUCstContained
-          by (split; [ simpl; unfold errAddUCst, realFromNum, negPow; interval | apply Req_le; auto]).
+          by (split; [ simpl; unfold errAddUCst, realFromNum, negativePower; interval | apply Req_le; auto]).
       assert (contained ((cst1 + errCst1) + (cenv u + errVaru) + errAddUCst)
              (addInterval
                 (addInterval (addInterval (mkInterval cst1 cst1) (mkInterval (-errCst1) (errCst1)))

coq/_CoqProject

--R ./ Daisy
-Infra/abbrevs.v
-exps.v
-daisy_lang.v
-newIntervalArith.v
-interval_arith.v
-abs_err.v
-simple_doppler.v
-realConversion.v
+-R . Daisy
+./Expressions.v
+./AbsoluteError.v
+./Infra/Abbrevs.v
+./Infra/RealConstruction.v
+./Commands.v
+./IntervalArith.v
+./SimpleDoppler.v

coq/configure_coq.sh

+#!/bin/sh
+
+echo "-R . Daisy" > _CoqProject
+
+find . -path ./attic -prune -o -name "*.v" -print >> _CoqProject

coq/realConversion.v

-Require Import Coq.Reals.Reals.
-
-(** Abbreviations for construction proper real numbers from injected natural numbers **)
-Definition negPow (base:R) (exp:nat) :R := 1 / (pow base exp).
-Definition realFromNum (n:R) (unitsBehindColon:nat) (exp:nat) :=
-  (n * (negPow (10)%R unitsBehindColon) * (negPow (2)%R exp))%R.
\ No newline at end of file