Commit e8c5b014 authored by ='s avatar =

Tentative proofs in ErrorValidation

parent 7ac1c370
...@@ -21,7 +21,7 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy ...@@ -21,7 +21,7 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
if (Qleb 0 err) if (Qleb 0 err)
then then
match e with match e with
|Var _ _ v => |Var _ v =>
if (NatSet.mem v dVars) if (NatSet.mem v dVars)
then true then true
else (Qleb (maxAbs intv * (meps m)) err) else (Qleb (maxAbs intv * (meps m)) err)
...@@ -69,7 +69,7 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy ...@@ -69,7 +69,7 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool := Fixpoint validErrorboundCmd (f:cmd Q) (typeMap:exp Q -> option mType) (env:analysisResult) (dVars:NatSet.t) {struct f} : bool :=
match f with match f with
|Let m x e g => |Let m x e g =>
if ((validErrorbound e typeMap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q m x))))) if ((validErrorbound e typeMap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q x)))))
then validErrorboundCmd g typeMap env (NatSet.add x dVars) then validErrorboundCmd g typeMap env (NatSet.add x dVars)
else false else false
|Ret e => validErrorbound e typeMap env dVars |Ret e => validErrorbound e typeMap env dVars
...@@ -90,7 +90,7 @@ Proof. ...@@ -90,7 +90,7 @@ Proof.
rewrite <- absenv_e in validErrorbound_e; simpl in *. rewrite <- absenv_e in validErrorbound_e; simpl in *.
- case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+ apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+ destruct (tmap (Var Q m n)); inversion validErrorbound_e. + destruct (tmap (Var Q n)); inversion validErrorbound_e.
- case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e. - case_eq (Qleb 0 err); intros; auto; rewrite H in validErrorbound_e.
+ apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto. + apply Qle_bool_iff,Qle_Rle in H; rewrite Q2R0_is_0 in H; auto.
+ destruct (tmap (Const m q)); inversion validErrorbound_e. + destruct (tmap (Const m q)); inversion validErrorbound_e.
...@@ -107,22 +107,21 @@ Qed. ...@@ -107,22 +107,21 @@ Qed.
Lemma validErrorboundCorrectVariable: Lemma validErrorboundCorrectVariable:
forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma, forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars,
validType Gamma (Var Q m v) m -> typeCheck (Var Q v) defVars Gamma = true ->
approxEnv E1 absenv fVars dVars E2 -> approxEnv E1 absenv fVars dVars E2 ->
eval_exp E1 (toREval (toRExp (Var Q m v))) nR M0 -> eval_exp E1 defVars (toREval (toRExp (Var Q v))) nR M0 ->
eval_exp E2 (toRExp (Var Q m v)) nF m -> eval_exp E2 defVars (toRExp (Var Q v)) nF m ->
validIntervalbounds (Var Q m v) absenv P dVars = true -> validIntervalbounds (Var Q v) absenv P dVars = true ->
validErrorbound (Var Q m v) Gamma absenv dVars = true -> validErrorbound (Var Q v) Gamma absenv dVars = true ->
(forall v1 m1, (forall v1,
NatSet.mem v1 dVars = true -> NatSet.mem v1 dVars = true ->
exists r mv1, exists r, E1 v1 = Some (r, M0) /\
E1 v1 = Some (r, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\ (Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) ->
(Q2R (fst (fst (absenv (Var Q m1 v1)))) <= r <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
(forall v1, NatSet.mem v1 fVars= true -> (forall v1, NatSet.mem v1 fVars= true ->
exists r, E1 v1 = Some (r, M0) /\ exists r, E1 v1 = Some (r, M0) /\
(Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) -> (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) ->
absenv (Var Q m v) = ((nlo, nhi), e) -> absenv (Var Q v) = ((nlo, nhi), e) ->
(Rabs (nR - nF) <= (Q2R e))%R. (Rabs (nR - nF) <= (Q2R e))%R.
Proof. Proof.
intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var. intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var.
......
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