Skip to content

GitLab

Commit 783b5d4a authored by ='s avatar =
Browse files

Proof of ivbounds_approximatesPrecond_soud: done

parent d2e8cff4
Hide whitespace changes
Inline Side-by-side
coq/IntervalValidation.v
View file @ 783b5d4a
......@@ -78,19 +78,22 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
validIntervalbounds e absenv P validVars
end.
Theorem ivbounds_approximatesPrecond_sound f absenv P V Gamma mF:
Theorem ivbounds_approximatesPrecond_sound f absenv P V Gamma:
validIntervalbounds f absenv P V = true ->
validType Gamma f mF ->
forall v m, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
Gamma (Var Q m v) = Some m ->
(exists mF, validType Gamma f mF) ->
forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
exists m, 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 valid_tf v m0 v_in_fV type_var; simpl in *.
- simpl. intros approx_true valid_tf v v_in_fV; 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 valid_tf as [mF valid_tf].
inversion valid_tf; subst.
exists mF; split; auto.
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 *.
......@@ -99,68 +102,50 @@ Proof.
+ apply Is_true_eq_left in approx_true.
apply andb_prop_elim in approx_true.
destruct approx_true; auto.
- intros approx_true v0 m0 v_in_fV typef; simpl in *.
- intros approx_true valid_tf v0 v_in_fV; simpl in *.
inversion v_in_fV.
- intros approx_unary_true v m0 v_in_fV typef; simpl in *.
unfold typeExpression in typef; inversion typef.
- intros approx_unary_true valid_tf v v_in_fV; simpl in *.
apply Is_true_eq_left in approx_unary_true.
simpl in *.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
apply andb_prop_elim in approx_unary_true.
destruct approx_unary_true.
apply IHf; try auto.
apply Is_true_eq_true; auto.
- intros approx_bin_true v m0 v_in_fV typef.
+ apply Is_true_eq_true; auto.
+ destruct valid_tf as [mF valid_tf].
inversion valid_tf; subst; auto.
exists mF; auto.
- intros approx_bin_true valid_tf v v_in_fV.
simpl in v_in_fV.
rewrite NatSet.diff_spec in v_in_fV.
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 (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.
destruct approx_bin_true.
apply andb_prop_elim in H1.
destruct H1.
apply IHf1; auto.
apply Is_true_eq_true; auto.
rewrite NatSet.diff_spec; split; auto.
eapply typedVarIsUsed; eauto.
+ 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.
destruct approx_bin_true.
apply andb_prop_elim in H1.
destruct H1.
apply IHf1; auto.
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.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true.
apply andb_prop_elim in H1.
destruct H1.
apply IHf2; auto.
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.
- intros approx_rnd_true v m0 v_in_fV typef.
destruct valid_tf as [mf valid_tf].
inversion valid_tf; subst.
destruct (absenv (Binop b f1 f2)); destruct (absenv f1);
destruct (absenv f2); simpl in *.
apply andb_prop_elim in approx_bin_true.
destruct approx_bin_true.
apply andb_prop_elim in H.
destruct H.
destruct v_in_fV.
+ apply IHf1; try auto.
* apply Is_true_eq_true; auto.
* eauto.
* rewrite NatSet.diff_spec; split; auto.
+ apply IHf2; try auto.
* apply Is_true_eq_true; auto.
* eauto.
* rewrite NatSet.diff_spec; split; auto.
- intros approx_rnd_true [mf valid_tf] v v_in_fV.
simpl in *; destruct (absenv (Downcast m f)); destruct (absenv f).
apply Is_true_eq_left in approx_rnd_true.
apply andb_prop_elim in approx_rnd_true.
destruct approx_rnd_true.
apply IHf; auto.
apply Is_true_eq_true in H; auto.
apply Is_true_eq_true in H; try auto.
inversion valid_tf; subst; eauto.
Qed.
Corollary Q2R_max4 a b c d:
......@@ -198,82 +183,81 @@ Proof.
apply le_neq_bool_to_lt_prop; auto.
Qed.
Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
(typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
(forall (v : NatSet.elt) (m : mType),
NatSet.mem v dVars = true ->
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 ->
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 (typeMap f2 (Var Q m v)); intros; auto.
- case_eq (mTypeEqBool m m1); intros.
+ (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*)
assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m).
simpl typeMap. rewrite H2.
auto.
specialize (H0 H5); auto.
+ pose proof (typeMapVarDet _ _ _ H3).
rewrite H5 in H4.
rewrite mTypeEqBool_refl in H4.
inversion H4.
- assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2; auto).
specialize (H0 H4).
auto.
Qed.
(* Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0: *)
(* (typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 -> *)
(* (forall (v : NatSet.elt) (m : mType), *)
(* NatSet.mem v dVars = true -> *)
(* 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 -> *)
(* 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 (typeMap f2 (Var Q m v)); intros; auto. *)
(* - case_eq (mTypeEqBool m m1); intros. *)
(* + (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*) *)
(* assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m). *)
(* simpl typeMap. rewrite H2. *)
(* auto. *)
(* specialize (H0 H5); auto. *)
(* + pose proof (typeMapVarDet _ _ _ H3). *)
(* rewrite H5 in H4. *)
(* rewrite mTypeEqBool_refl in H4. *)
(* inversion H4. *)
(* - assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2; auto). *)
(* specialize (H0 H4). *)
(* auto. *)
(* Qed. *)
Lemma validVarsUnfolding_r (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0:
(typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 ->
(forall (v : NatSet.elt) (m : mType),
NatSet.mem v dVars = true ->
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 ->
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 (typeMap f1 (Var Q m v)); intros; auto.
- case_eq (mTypeEqBool m1 m); intros.
+ (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*)
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 (typeMapVarDet _ _ _ H3).
rewrite H5 in H4.
rewrite mTypeEqBool_refl in H4.
inversion H4.
- assert (typeMap (Binop b f1 f2) (Var Q m v) = Some m) by (simpl; rewrite H2,H3; auto).
specialize (H0 H4).
auto.
Qed.
(* Lemma validVarsUnfolding_r (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0: *)
(* (typeMap (Binop b f1 f2)) (Binop b f1 f2) = Some m0 -> *)
(* (forall (v : NatSet.elt) (m : mType), *)
(* NatSet.mem v dVars = true -> *)
(* 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 -> *)
(* 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 (typeMap f1 (Var Q m v)); intros; auto. *)
(* - case_eq (mTypeEqBool m1 m); intros. *)
(* + (*apply EquivEqBoolEq in H4. ; rewrite <- H4 in H3.*) *)
(* 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 (typeMapVarDet _ _ _ H3). *)
(* rewrite H5 in H4. *)
(* rewrite mTypeEqBool_refl in H4. *)
(* inversion H4. *)
(* - 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):
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) Gamma:
forall vR m,
(typeMap f) f = Some m ->
validType Gamma f m ->
validIntervalbounds f absenv P dVars = true ->
(forall v m, NatSet.mem v dVars = true ->
(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) ->
(forall v, NatSet.mem v dVars = true ->
exists vR mv, E v = Some (vR, M0) /\ Gamma (Var Q mv v) = Some mv /\
(Q2R (fst (fst (absenv (Var Q mv v)))) <= vR <= Q2R (snd (fst (absenv (Var Q mv v)))))%R) ->
NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some (vR, M0) /\
......@@ -289,13 +273,16 @@ Proof.
simpl; rewrite absenv_var in *; simpl in *.
inversion eval_f; subst.
case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
+ specialize (valid_definedVars n m case_mem).
assert (mTypeEqBool m m && (n =? n) = true).
apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto.
+ specialize (valid_definedVars n case_mem).
inversion typing_ok; subst.
destruct valid_definedVars as [vR' [mv [E_n_eq [gamma_n iv_n]]]].
rewrite H2 in E_n_eq; inversion E_n_eq; subst.
(* assert (mTypeEqBool m m && (n =? n) = true). *)
(* apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto. *)
(* rewrite H in valid_definedVars. *)
(* assert (Some m = Some m) by auto. *)
(* specialize (valid_definedVars H0). *)
destruct valid_definedVars as [vR' [E_n_eq precond_sound]].
rewrite H; auto.
rewrite E_n_eq in *.
inversion H2; subst.
......
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