Skip to content

GitLab

Commit 24e890cc authored by Joachim Bard's avatar Joachim Bard
Browse files

very little work on IEEE_connection

parent 82ac18d4
Hide whitespace changes
Inline Side-by-side
coq/IEEE_connection.v
View file @ 24e890cc
...@@ -4,7 +4,7 @@ From Coq ...@@ -4,7 +4,7 @@ From Coq
From Flover From Flover
Require Import Expressions Infra.RationalSimps TypeValidator IntervalValidation Require Import Expressions Infra.RationalSimps TypeValidator IntervalValidation
ErrorAnalysis CertificateChecker FPRangeValidator RoundoffErrorValidator ErrorAnalysis CertificateChecker SubdivsChecker FPRangeValidator RoundoffErrorValidator
Environments Infra.RealRationalProps Infra.Ltacs. Environments Infra.RealRationalProps Infra.Ltacs.
From Flocq From Flocq
...@@ -1218,7 +1218,7 @@ Proof. ...@@ -1218,7 +1218,7 @@ Proof.
Qed. Qed.
*) *)
Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap: Theorem IEEE_connection_expr e A P qMap subdivs E1 E2 defVars DeltaMap:
(forall (e' : expr R) (m' : mType), (forall (e' : expr R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
is64BitEval (B2Qexpr e) -> is64BitEval (B2Qexpr e) ->
...@@ -1226,8 +1226,9 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap: ...@@ -1226,8 +1226,9 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
noDowncast (B2Qexpr e) -> noDowncast (B2Qexpr e) ->
eval_expr_valid e E2 -> eval_expr_valid e E2 ->
unsat_queries qMap -> unsat_queries qMap ->
(forall qMap, In qMap (queriesInSubdivs subdivs) -> unsat_queries qMap) ->
eval_precond E1 P -> eval_precond E1 P ->
CertificateChecker (B2Qexpr e) A P qMap defVars = true -> CertificateChecker (B2Qexpr e) A P qMap subdivs defVars = true ->
exists Gamma, (* m, currently = M64 *) exists Gamma, (* m, currently = M64 *)
approxEnv E1 Gamma A (freeVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) -> approxEnv E1 Gamma A (freeVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
exists iv err vR vF, exists iv err vR vF,
...@@ -1237,7 +1238,7 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap: ...@@ -1237,7 +1238,7 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
eval_expr (toREnv E2) Gamma DeltaMap (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\ eval_expr (toREnv E2) Gamma DeltaMap (toRExp (B2Qexpr e)) (Q2R (B2Q vF)) M64 /\
(Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R. (Rabs (vR - Q2R (B2Q vF )) <= Q2R err)%R.
Proof. Proof.
intros * deltas_matched is64eval is64bitenv no_cast eval_valid unsat_qs intros * deltas_matched is64eval is64bitenv no_cast eval_valid unsat_qs unsat_qs_subdiv
P_valid certificate_valid. P_valid certificate_valid.
unfold CertificateChecker in certificate_valid. unfold CertificateChecker in certificate_valid.
destruct (getValidMap defVars (B2Qexpr e) (FloverMap.empty mType)) eqn:?; try congruence. destruct (getValidMap defVars (B2Qexpr e) (FloverMap.empty mType)) eqn:?; try congruence.
...@@ -1250,7 +1251,7 @@ Proof. ...@@ -1250,7 +1251,7 @@ Proof.
{ eapply getValidMap_top_correct; eauto. { eapply getValidMap_top_correct; eauto.
intros. cbn in *; congruence. } intros. cbn in *; congruence. }
(* rewrite <- andb_lazy_alt in certificate_valid. *) (* rewrite <- andb_lazy_alt in certificate_valid. *)
andb_to_prop certificate_valid. (* andb_to_prop certificate_valid. *)
pose proof (NatSetProps.empty_union_2 (freeVars e) NatSet.empty_spec) as union_empty. pose proof (NatSetProps.empty_union_2 (freeVars e) NatSet.empty_spec) as union_empty.
hnf in union_empty. hnf in union_empty.
assert (dVars_range_valid NatSet.empty E1 A). assert (dVars_range_valid NatSet.empty E1 A).
......
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