Commit 4c7f41e8 authored by ='s avatar =

Cleaning coq file

parent 3f0f4ba7
......@@ -2000,24 +2000,6 @@ Proof.
apply Qle_Rle.
assumption.
Qed.
(* Lemma test E e v m m' Gamma: *)
(* eval_exp E (toRExp e) v m -> *)
(* validType Gamma e m' -> *)
(* m = m'. *)
(* Proof. *)
(* revert v m m'; induction e; intros * eval_e vt_e. *)
(* - inversion eval_e; subst; inversion vt_e; subst; auto. *)
(* - inversion eval_e; subst; inversion vt_e; subst; auto. *)
(* - inversion vt_e; subst; auto; inversion eval_e; subst. *)
(* + eapply IHe; eauto. *)
(* + eapply IHe; eauto. *)
(* - inversion vt_e; subst; inversion eval_e; subst; try auto. *)
(* assert (m0 = m1) by (eapply IHe1; eauto). *)
(* assert (m3 = m2) by (eapply IHe2; eauto). *)
(* subst; simpl; auto. *)
(* - inversion vt_e; subst; inversion eval_e; subst; auto. *)
(* Qed. *)
(**
Soundness theorem for the error bound validator.
......@@ -2116,23 +2098,6 @@ Proof.
andb_to_prop valid_intv.
inversion eval_real; subst.
destruct m0; destruct m3; inversion H5; clear H5.
(* inversion eval_float; subst. *)
(* rename v0 into vF1. *)
(* rename v3 into vF2. *)
(* pose proof (validIntervalbounds_sound e1 absenv P (vR:=v1) defVars L2 valid_dVars (fVars:=fVars)) *)
(* as valid_bounds_e1. *)
(* rewrite absenv_e1 in valid_bounds_e1. *)
(* pose proof (validIntervalbounds_sound e2 absenv P (vR:=v2) defVars R4 valid_dVars (fVars:=fVars)) *)
(* as valid_bounds_e2. *)
(* rewrite absenv_e2 in valid_bounds_e2; *)
(* simpl in *. *)
(* rewrite Q2R0_is_0 in H6; apply Rabs_0_impl_eq in H6; subst. *)
(* unfold perturb; simpl. *)
(* assert (Rabs (v1 - vF1) <= Q2R err1 /\ Rabs (v2 - vF2) <= Q2R err2)%R. *)
apply binary_unfolding in eval_float.
destruct eval_float as [vF1 [vF2 [ mF1 [mF2 [joinF12 [eval_e1 [eval_e2 eval_float ]]]]]]].
simpl in *.
......
......@@ -80,7 +80,6 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true ->
(*(exists mF, validType Gamma f mF) ->*)
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))).
Proof.
......
......@@ -192,7 +192,7 @@ Theorem typingSoundnessExp e defVars E:
eval_exp E defVars (toRExp e) v m ->
Gamma e = Some m.
Proof.
revert e; induction e; intros * (*gamma_def*) typechecks evals.
revert e; induction e; intros * typechecks evals.
- simpl in typechecks.
inversion evals; subst.
rewrite H0 in typechecks.
......@@ -235,7 +235,7 @@ Qed.
Theorem typingSoundnessCmd c defVars E v m Gamma:
typeCheckCmd c defVars Gamma = true ->
bstep (toRCmd c) E defVars v m ->
(*(typeMapCmd defVars c)*) Gamma (getRetExp c) = Some m.
Gamma (getRetExp c) = Some m.
Proof.
revert E defVars; induction c; intros * tc bc.
- simpl in tc.
......
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