Commit e2419de3 authored by ='s avatar =

Trying to use Gammas in the proofs

parent 9df78c50
......@@ -65,13 +65,13 @@ Fixpoint validErrorbound (e:exp Q) (typeMap:exp Q -> option mType) (absenv:analy
end.
(** Error bound command validator **)
Fixpoint validErrorboundCmd (f:cmd Q) (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
|Let m x e g =>
if ((validErrorbound e (typeExpression e) env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q m x)))))
then validErrorboundCmd g env (NatSet.add x dVars)
if ((validErrorbound e typeMap env dVars) && (Qeq_bool (snd (env e)) (snd (env (Var Q m x)))))
then validErrorboundCmd g typeMap env (NatSet.add x dVars)
else false
|Ret e => validErrorbound e (typeExpression e) env dVars
|Ret e => validErrorbound e typeMap env dVars
end.
......@@ -119,16 +119,15 @@ Qed.
Lemma validErrorboundCorrectVariable:
forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m f,
(typeMap f) (Var Q m v) = Some m ->
approxEnv E1 absenv fVars dVars E2 ->
eval_exp E1 (toREval (toRExp (Var Q m v))) nR M0 ->
eval_exp E2 (toRExp (Var Q m v)) nF m ->
validIntervalbounds (Var Q m v) absenv P dVars = true ->
isSubExpression (Var Q m v) f = true ->
validErrorbound (Var Q m v) (typeExpression f) absenv dVars = true ->
validErrorbound (Var Q m v) (typeMap f) absenv dVars = true ->
(forall v1 m1,
NatSet.mem v1 dVars = true ->
(*isSubExpression (Var Q m1 v1) f = true ->*)
(typeExpression f) (Var Q m1 v1) = Some m1 ->
(typeMap f) (Var Q m1 v1) = Some m1 ->
exists r : R,
E1 v1 = Some (r, M0) /\
(Q2R (fst (fst (absenv (Var Q m1 v1)))) <= r <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) ->
......@@ -138,7 +137,7 @@ Lemma validErrorboundCorrectVariable:
absenv (Var Q m v) = ((nlo, nhi), e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
Proof.
intros * approxCEnv eval_real eval_float bounds_valid subexpr_ok error_valid dVars_sound P_valid absenv_var.
intros * typing_ok approxCEnv eval_real eval_float bounds_valid subexpr_ok error_valid dVars_sound P_valid absenv_var.
simpl in eval_real; inversion eval_real; inversion eval_float; subst.
rename H2 into E1_v;
rename H7 into E2_v.
......
......@@ -78,19 +78,20 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
validIntervalbounds e absenv P validVars
end.
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
Theorem ivbounds_approximatesPrecond_sound f absenv P V Gamma mF:
validIntervalbounds f absenv P V = true ->
validType Gamma f mF ->
forall v m, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
(typeMap f) (Var Q m v) = Some m ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q m v)))).
Gamma (Var Q m v) = Some m ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q m v)))).
Proof.
induction f; unfold validIntervalbounds.
- simpl. intros approx_true v m0 v_in_fV typef; simpl in *.
case_eq (mTypeEqBool m m0 && (n =? v)); intros; rewrite H in typef; inversion typef; subst.
- simpl. intros approx_true valid_tf v m0 v_in_fV type_var; simpl in *.
inversion valid_tf; subst.
rewrite NatSet.diff_spec in v_in_fV.
rewrite NatSet.singleton_spec in v_in_fV;
destruct v_in_fV; subst.
destruct (absenv (Var Q m0 n)); simpl in *.
destruct (absenv (Var Q mF n)); simpl in *.
case_eq (NatSet.mem n V); intros case_mem;
rewrite case_mem in approx_true; simpl in *.
+ rewrite NatSet.mem_spec in case_mem.
......@@ -617,6 +618,7 @@ Proof.
+ destruct m1; destruct m2; inversion H2.
simpl in H4; rewrite Q2R0_is_0 in H4; auto.
- unfold validIntervalbounds in valid_bounds.
pose proof (typeMap_gives_type _ typing_ok) as t_downcast.
(*simpl erasure in valid_bounds.*)
simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f); simpl in *.
apply Is_true_eq_left in valid_bounds.
......@@ -632,10 +634,11 @@ Proof.
apply Qeq_eqR in Eqlo; rewrite Eqlo.
apply Qeq_eqR in Eqhi; rewrite Eqhi.
pose proof (expEqBool_refl (Downcast m f)); simpl in H; rewrite H in typing_ok; inversion typing_ok; subst.
case_eq (typeMap f f); intros.
+ apply (IHf vR m); auto.
apply Is_true_eq_true in vI1; auto.
+ inversion typing_ok.
case_eq (typeExpression f); intros.
+ apply (IHf vR m); auto.
* apply typeGivesTypeMap; auto.
* apply Is_true_eq_true in vI1; auto.
+ rewrite H0 in t_downcast; inversion t_downcast.
Qed.
......
......@@ -39,7 +39,23 @@ Fixpoint typeMap (e:exp Q) (e': exp Q) : option mType :=
Lemma typeMapVarDet e m m' v:
typeMap e (Var Q m v) = Some m' ->
m = m'.
Admitted.
Proof.
revert e; induction e; intros.
- simpl in H.
case_eq (mTypeEqBool m0 m && (n =? v)); intros; rewrite H0 in H.
apply andb_true_iff in H0; destruct H0.
inversion H; subst.
apply EquivEqBoolEq in H0; subst; auto.
inversion H.
- simpl in H. inversion H.
- simpl in H. apply IHe; auto.
- simpl in H.
case_eq (typeMap e1 (Var Q m v)); intros; rewrite H0 in H.
+ inversion H; subst.
apply IHe1; auto.
+ apply IHe2; auto.
- simpl in H. apply IHe; auto.
Qed.
Lemma typedVarIsUsed f1 m1 v:
typeMap f1 (Var Q m1 v) = Some m1 ->
......@@ -133,6 +149,10 @@ Proof.
econstructor; eauto.
Qed.
Definition GammaStronger (Gamma1 Gamma2:exp Q -> option mType):=
forall e m, Gamma1 e = Some m -> Gamma2 e = Some m.
Lemma unop_neq u e:
expEqBool (Unop u e) e = true -> False .
Proof.
......
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