Skip to content

GitLab

Commit 9df78c50 authored by ='s avatar =
Browse files
Options

trying something else

parent 3fa5e0ce
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1005 additions and 680 deletions
coq/Expressions.v
View file @ 9df78c50
......@@ -180,6 +180,50 @@ Proof.
+ apply IHe.
Qed.
Lemma expEqBool_trans e f g:
expEqBool e f = true ->
expEqBool f g = true ->
expEqBool e g = true.
Proof.
revert e f g; induction e; destruct f; intros; simpl in H; inversion H; rewrite H; clear H; destruct g; simpl in H0; inversion H0; rewrite H0; clear H0; apply andb_true_iff in H1; destruct H1; apply andb_true_iff in H2; destruct H2; simpl.
- apply EquivEqBoolEq in H1.
apply EquivEqBoolEq in H.
apply beq_nat_true in H2.
apply beq_nat_true in H0.
subst.
rewrite <- beq_nat_refl,mTypeEqBool_refl.
auto.
- apply EquivEqBoolEq in H1.
apply EquivEqBoolEq in H.
subst.
rewrite mTypeEqBool_refl; simpl.
apply Qeq_bool_iff in H2.
apply Qeq_bool_iff in H0.
apply Qeq_bool_iff.
lra.
- assert (u = u0) by (destruct u; destruct u0; inversion H1; auto).
assert (u0 = u1) by (destruct u0; destruct u1; inversion H; auto).
subst.
assert (unopEqBool u1 u1 = true) by (destruct u1; auto).
apply andb_true_iff; split; try auto.
eapply IHe; eauto.
- apply andb_true_iff; split.
+ destruct b; destruct b0; destruct b1; auto.
+ apply andb_true_iff in H2; destruct H2.
apply andb_true_iff in H0; destruct H0.
apply andb_true_iff; split.
eapply IHe1; eauto.
eapply IHe2; eauto.
- apply EquivEqBoolEq in H1.
apply EquivEqBoolEq in H.
subst.
rewrite mTypeEqBool_refl; simpl.
eapply IHe; eauto.
Qed.
Fixpoint toRExp (e:exp Q) :=
match e with
|Var _ m v => Var R m v
......
coq/IntervalValidation.v
View file @ 9df78c50
......@@ -81,7 +81,7 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true ->
forall v m, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
(typeExpression f) (Var Q m v) = Some m ->
(typeMap f) (Var Q m v) = Some m ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q m v)))).
Proof.
induction f; unfold validIntervalbounds.
......@@ -115,9 +115,11 @@ Proof.
destruct v_in_fV as [ v_in_fV v_not_in_V].
rewrite NatSet.union_spec in v_in_fV.
apply Is_true_eq_left in approx_bin_true.
case_eq (typeExpression f1 (Var Q m0 v));
case_eq (typeExpression f2 (Var Q m0 v)); intros; auto; subst.
+ pose proof (detTypingBinop f1 f2 b _ _ typef H0 H) as [H01 H02]; subst.
case_eq (typeMap f1 (Var Q m0 v));
case_eq (typeMap f2 (Var Q m0 v)); intros; auto; subst.
+ pose proof (typeMapVarDet _ _ _ H);
pose proof (typeMapVarDet _ _ _ H0); subst.
(* pose proof (detTypingBinop f1 f2 b _ _ typef H0 H) as [H01 H02]; subst. *)
destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
......@@ -128,7 +130,7 @@ Proof.
apply Is_true_eq_true; auto.
rewrite NatSet.diff_spec; split; auto.
eapply typedVarIsUsed; eauto.
+ simpl in *; rewrite H0,H in typef; inversion typef; subst.
+ simpl in *; rewrite H0 in typef; inversion typef; subst.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
......@@ -196,80 +198,79 @@ Proof.
Qed.
Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
(typeExpression (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
(typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
(forall (v : NatSet.elt) (m : mType),
NatSet.mem v dVars = true ->
typeExpression (Binop b f1 f2) (Var Q m v) = Some m ->
typeMap (Binop b f1 f2) (Var Q m v) = Some m ->
exists vR : R,
E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)
->
(forall (v : NatSet.elt) (m : mType),
NatSet.mem v dVars = true ->
typeExpression f1 (Var Q m v) = Some m ->
typeMap f1 (Var Q m v) = Some m ->
exists vR : R,
E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R).
Proof.
intros.
specialize (H0 v m H1).
case_eq (typeExpression f2 (Var Q m v)); intros; auto.
case_eq (typeMap f2 (Var Q m v)); intros; auto.
- case_eq (mTypeEqBool m m1); intros.
+ (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*)
assert (typeExpression (Binop b f1 f2) (Var Q m v) = Some m).
simpl typeExpression; rewrite H2, H3.
rewrite H4; auto.
assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m).
simpl typeMap. rewrite H2.
auto.
specialize (H0 H5); auto.
+ pose proof (typingVarDet _ _ _ H3).
+ pose proof (typeMapVarDet _ _ _ H3).
rewrite H5 in H4.
rewrite mTypeEqBool_refl in H4.
inversion H4.
- assert (typeExpression (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2,H3; auto).
- assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2; auto).
specialize (H0 H4).
auto.
Qed.
Qed.
Lemma validVarsUnfolding_r (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
(typeExpression (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
(typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
(forall (v : NatSet.elt) (m : mType),
NatSet.mem v dVars = true ->
typeExpression (Binop b f1 f2) (Var Q m v) = Some m ->
typeMap (Binop b f1 f2) (Var Q m v) = Some m ->
exists vR : R,
E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R)
->
(forall (v : NatSet.elt) (m : mType),
NatSet.mem v dVars = true ->
typeExpression f2 (Var Q m v) = Some m ->
typeMap f2 (Var Q m v) = Some m ->
exists vR : R,
E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R).
Proof.
intros.
specialize (H0 v m H1).
case_eq (typeExpression f1 (Var Q m v)); intros; auto.
case_eq (typeMap f1 (Var Q m v)); intros; auto.
- case_eq (mTypeEqBool m1 m); intros.
+ (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*)
assert (typeExpression (Binop b f1 f2) (Var Q m v) = Some m).
simpl typeExpression; rewrite H2, H3.
rewrite H4; auto.
assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m).
simpl typeMap; rewrite H3.
apply EquivEqBoolEq in H4; rewrite H4; auto.
specialize (H0 H5); auto.
+ pose proof (typingVarDet _ _ _ H3).
+ pose proof (typeMapVarDet _ _ _ H3).
rewrite H5 in H4.
rewrite mTypeEqBool_refl in H4.
inversion H4.
- assert (typeExpression (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2,H3; auto).
- assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2,H3; auto).
specialize (H0 H4).
auto.
Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env):
forall vR m,
(typeExpression f) f = Some m ->
(typeMap f) f = Some m ->
validIntervalbounds f absenv P dVars = true ->
(forall v m, NatSet.mem v dVars = true ->
(typeExpression f) (Var Q m v) = Some m ->
(typeMap f) (Var Q m v) = Some m ->
exists vR, E v = Some (vR, M0) /\
(Q2R (fst (fst (absenv (Var Q m v)))) <= vR <= Q2R (snd (fst (absenv (Var Q m v)))))%R) ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
......@@ -350,7 +351,7 @@ Proof.
destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec.
inversion eval_f; subst.
+ assert (typeExpression f f = Some mf) as typing_f_ok by (simpl typeExpression in typing_ok; rewrite expEqBool_refl in typing_ok; auto).
+ assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).
specialize (IHf v1 mf typing_f_ok valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
rewrite absenv_f in IHf; simpl in IHf.
(* TODO: Make lemma *)
......@@ -369,7 +370,7 @@ Proof.
* eapply Rle_trans.
Focus 2. apply valid_hi.
rewrite Q2R_opp; lra.
+ assert (typeExpression f f = Some mf) as typing_f_ok by (simpl typeExpression in typing_ok; rewrite expEqBool_refl in typing_ok; auto).
+ assert (typeMap f f = Some mf) as typing_f_ok by (simpl in typing_ok; rewrite expEqBool_refl in typing_ok; apply typeGivesTypeMap; auto).
specialize (IHf v1 mf typing_f_ok valid_rec valid_definedVars usedVars_subset valid_usedVars H4).
rewrite absenv_f in IHf; simpl in IHf.
apply andb_prop_elim in valid_unop.
......@@ -454,12 +455,17 @@ Proof.
apply andb_prop_elim in valid_rec.
destruct valid_rec as [valid_e1 valid_e2].
apply Is_true_eq_true in valid_e1; apply Is_true_eq_true in valid_e2.
destruct m1; destruct m2; cbv in H2; inversion H2.
pose proof (typeMap_gives_type _ typing_ok).
simpl in H. case_eq (typeExpression f1); intros; rewrite H0 in H; [ | inversion H ].
case_eq (typeExpression f2); intros; rewrite H1 in H; inversion H.
pose proof (validVarsUnfolding_l _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f1.
pose proof (validVarsUnfolding_r _ _ _ _ _ _ typing_ok valid_definedVars) as valid_definedVars_f2.
pose proof (binop_type_unfolding _ _ _ typing_ok) as subtypes.
destruct subtypes as [mf1 [mf2 [typing_f1 [typing_f2 join_f1_f2]]]].
specialize (IHf1 v1 mf1 typing_f1 valid_e1 valid_definedVars_f1).
specialize (IHf2 v2 mf2 typing_f2 valid_e2 valid_definedVars_f2).
(* pose proof (binop_type_unfolding _ _ _ typing_ok) as subtypes. *)
(* destruct subtypes as [mf1 [mf2 [typing_f1 [typing_f2 join_f1_f2]]]]. *)
apply typeGivesTypeMap in H0. apply typeGivesTypeMap in H1.
specialize (IHf1 v1 m H0 valid_e1 valid_definedVars_f1).
specialize (IHf2 v2 m0 H1 valid_e2 valid_definedVars_f2).
rewrite absenv_f1 in IHf1.
rewrite absenv_f2 in IHf2.
assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1.
......@@ -470,7 +476,6 @@ Proof.
rewrite NatSet.diff_spec in in_diff_e1.
destruct in_diff_e1 as [ in_usedVars not_dVar].
split; try auto.
destruct m1; destruct m2; inversion H2; subst; auto.
+ assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2.
* apply IHf2; try auto.
intros v in_diff_e2.
......@@ -478,7 +483,6 @@ Proof.
simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
rewrite NatSet.diff_spec in in_diff_e2.
destruct in_diff_e2; split; auto.
destruct m1; destruct m2; inversion H2; auto.
* destruct b; simpl in *.
{ pose proof (interval_addition_valid (iv1 :=(Q2R (fst iv1),Q2R (snd iv1))) (iv2 :=(Q2R (fst iv2), Q2R (snd iv2)))) as valid_add.
unfold validIntervalAdd in valid_add.
......@@ -576,21 +580,21 @@ Proof.
[ | exfalso; apply neq_0; auto | | exfalso; apply neq_0; symmetry; auto]; auto.
- destruct valid_div as [valid_div_lo valid_div_hi]; simpl; try auto.
+ rewrite <- Q2R0_is_0.
destruct H; [left | right]; apply Qlt_Rlt; auto.
destruct H3; [left | right]; apply Qlt_Rlt; auto.
+ unfold divideInterval, IVlo, IVhi in valid_div_lo, valid_div_hi.
simpl in *.
assert (Q2R (fst iv2) <= (Q2R (snd iv2)))%R by lra.
assert (~ snd iv2 == 0).
* destruct H; try lra.
hnf; intros ivhi2_0.
apply Rle_Qle in H0.
rewrite ivhi2_0 in H0.
apply Rle_Qle in H8.
rewrite ivhi2_0 in H8.
lra.
* assert (~ fst iv2 == 0).
{ destruct H; try lra.
hnf; intros ivlo2_0.
apply Rle_Qle in H0.
rewrite ivlo2_0 in H0.
apply Rle_Qle in H8.
rewrite ivlo2_0 in H8.
lra. }
{ split.
- eapply Rle_trans. (*rewrite absenv_bin;*) apply valid_lo.
......@@ -627,11 +631,9 @@ Proof.
simpl in *.
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.
case_eq (typeExpression f f); intros; rewrite H0 in typing_ok.
+ case_eq (isMorePrecise m0 m); intros; rewrite H1 in typing_ok; inversion typing_ok.
subst.
apply (IHf vR m0); auto.
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.
Qed.
......
coq/Typing.v
View file @ 9df78c50
This diff is collapsed.
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