Commit 3d84d953 authored by Raphaël Monat's avatar Raphaël Monat

Small updates

parent e0ab9274
...@@ -80,7 +80,7 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v ...@@ -80,7 +80,7 @@ Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (v
Theorem ivbounds_approximatesPrecond_sound f absenv P V: Theorem ivbounds_approximatesPrecond_sound f absenv P V:
validIntervalbounds f absenv P V = true -> validIntervalbounds f absenv P V = true ->
forall v, NatSet.In v (NatSet.diff (Expressions.freeVars f) V) -> forall v, NatSet.In v (NatSet.diff (Expressions.usedVars f) V) ->
Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))). Is_true(isSupersetIntv (P v) (fst (absenv (Var Q v)))).
Proof. Proof.
induction f; unfold validIntervalbounds. induction f; unfold validIntervalbounds.
...@@ -99,7 +99,7 @@ Proof. ...@@ -99,7 +99,7 @@ Proof.
- intros approx_true v0 v_in_fV; simpl in *. - intros approx_true v0 v_in_fV; simpl in *.
inversion v_in_fV. inversion v_in_fV.
- intros approx_unary_true v v_in_fV. - intros approx_unary_true v v_in_fV.
unfold freeVars in v_in_fV. unfold usedVars in v_in_fV.
apply Is_true_eq_left in approx_unary_true. apply Is_true_eq_left in approx_unary_true.
destruct (absenv (Unop u f)); destruct (absenv f); simpl in *. destruct (absenv (Unop u f)); destruct (absenv f); simpl in *.
apply andb_prop_elim in approx_unary_true. apply andb_prop_elim in approx_unary_true.
...@@ -173,18 +173,18 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) ...@@ -173,18 +173,18 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond)
(forall v, NatSet.mem v dVars = true -> (forall v, NatSet.mem v dVars = true ->
exists vR, E v = Some vR /\ exists vR, E v = Some vR /\
(Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
NatSet.Subset (NatSet.diff (Expressions.freeVars f) dVars) fVars -> NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars ->
(forall v, NatSet.mem v fVars = true -> (forall v, NatSet.mem v fVars = true ->
exists vR, E v = Some vR /\ exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
eval_exp 0%R E (toRExp f) vR -> eval_exp 0%R E (toRExp f) vR ->
(Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R.
Proof. Proof.
induction f; intros vR valid_bounds valid_definedVars freeVars_subset valid_freeVars eval_f. induction f; intros vR valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f.
- unfold validIntervalbounds in valid_bounds. - unfold validIntervalbounds in valid_bounds.
env_assert absenv (Var Q n) absenv_var. env_assert absenv (Var Q n) absenv_var.
destruct absenv_var as [ iv [err absenv_var]]. destruct absenv_var as [ iv [err absenv_var]].
specialize (valid_freeVars n). specialize (valid_usedVars n).
rewrite absenv_var in *; simpl in *. rewrite absenv_var in *; simpl in *.
inversion eval_f; subst. inversion eval_f; subst.
case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *. case_eq (NatSet.mem n dVars); intros case_mem; rewrite case_mem in *; simpl in *.
...@@ -205,15 +205,15 @@ Proof. ...@@ -205,15 +205,15 @@ Proof.
* assert (NatSet.In n (NatSet.singleton n)) * assert (NatSet.In n (NatSet.singleton n))
as in_singleton by (rewrite NatSet.singleton_spec; auto). as in_singleton by (rewrite NatSet.singleton_spec; auto).
rewrite NatSet.mem_spec. rewrite NatSet.mem_spec.
hnf in freeVars_subset. hnf in usedVars_subset.
apply freeVars_subset. apply usedVars_subset.
rewrite NatSet.diff_spec, NatSet.singleton_spec. rewrite NatSet.diff_spec, NatSet.singleton_spec.
split; try auto. split; try auto.
hnf; intros in_dVars. hnf; intros in_dVars.
rewrite <- NatSet.mem_spec in in_dVars. rewrite <- NatSet.mem_spec in in_dVars.
rewrite in_dVars in case_mem; congruence. rewrite in_dVars in case_mem; congruence.
* specialize (valid_freeVars in_fVars); * specialize (valid_usedVars in_fVars);
destruct valid_freeVars as [vR' [vR_def P_valid]]. destruct valid_usedVars as [vR' [vR_def P_valid]].
rewrite vR_def in H0; inversion H0; subst. rewrite vR_def in H0; inversion H0; subst.
lra. lra.
- unfold validIntervalbounds in valid_bounds. - unfold validIntervalbounds in valid_bounds.
...@@ -244,7 +244,7 @@ Proof. ...@@ -244,7 +244,7 @@ Proof.
destruct valid_bounds as [valid_rec valid_unop]. destruct valid_bounds as [valid_rec valid_unop].
apply Is_true_eq_true in valid_rec. apply Is_true_eq_true in valid_rec.
inversion eval_f; subst. inversion eval_f; subst.
+ specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H2). + specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H2).
rewrite absenv_f in IHf; simpl in IHf. rewrite absenv_f in IHf; simpl in IHf.
(* TODO: Make lemma *) (* TODO: Make lemma *)
unfold isSupersetIntv in valid_unop. unfold isSupersetIntv in valid_unop.
...@@ -262,7 +262,7 @@ Proof. ...@@ -262,7 +262,7 @@ Proof.
* eapply Rle_trans. * eapply Rle_trans.
Focus 2. apply valid_hi. Focus 2. apply valid_hi.
rewrite Q2R_opp; lra. rewrite Q2R_opp; lra.
+ specialize (IHf v1 valid_rec valid_definedVars freeVars_subset valid_freeVars H3). + specialize (IHf v1 valid_rec valid_definedVars usedVars_subset valid_usedVars H3).
rewrite absenv_f in IHf; simpl in IHf. rewrite absenv_f in IHf; simpl in IHf.
apply andb_prop_elim in valid_unop. apply andb_prop_elim in valid_unop.
destruct valid_unop as [nodiv0 valid_unop]. destruct valid_unop as [nodiv0 valid_unop].
...@@ -351,15 +351,15 @@ Proof. ...@@ -351,15 +351,15 @@ Proof.
assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1. assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1.
+ apply IHf1; try auto. + apply IHf1; try auto.
intros v in_diff_e1. intros v in_diff_e1.
apply freeVars_subset. apply usedVars_subset.
simpl. rewrite NatSet.diff_spec,NatSet.union_spec. simpl. rewrite NatSet.diff_spec,NatSet.union_spec.
rewrite NatSet.diff_spec in in_diff_e1. rewrite NatSet.diff_spec in in_diff_e1.
destruct in_diff_e1 as [ in_freeVars not_dVar]. destruct in_diff_e1 as [ in_usedVars not_dVar].
split; try auto. split; try auto.
+ assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2. + assert (Q2R (fst (fst (iv2, err2))) <= v2 <= Q2R (snd (fst (iv2, err2))))%R as valid_bounds_e2.
* apply IHf2; try auto. * apply IHf2; try auto.
intros v in_diff_e2. intros v in_diff_e2.
apply freeVars_subset. apply usedVars_subset.
simpl. rewrite NatSet.diff_spec, NatSet.union_spec. simpl. rewrite NatSet.diff_spec, NatSet.union_spec.
rewrite NatSet.diff_spec in in_diff_e2. rewrite NatSet.diff_spec in in_diff_e2.
destruct in_diff_e2; split; auto. destruct in_diff_e2; split; auto.
...@@ -506,14 +506,14 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): ...@@ -506,14 +506,14 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
exists vR, exists vR,
E v = Some vR /\ E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) ->
NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> NatSet.Subset (NatSet.diff (Commands.usedVars f) dVars) fVars ->
validIntervalboundsCmd f absenv P dVars = true -> validIntervalboundsCmd f absenv P dVars = true ->
absenv (getRetExp f) = ((elo, ehi), err) -> absenv (getRetExp f) = ((elo, ehi), err) ->
(Q2R elo <= vR <= Q2R ehi)%R. (Q2R elo <= vR <= Q2R ehi)%R.
Proof. Proof.
induction f; induction f;
intros E vR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound intros E vR fVars dVars outVars elo ehi err P ssa_f eval_f dVars_sound
fVars_valid freeVars_subset valid_bounds_f absenv_f. fVars_valid usedVars_subset valid_bounds_f absenv_f.
- inversion ssa_f; subst. - inversion ssa_f; subst.
inversion eval_f; subst. inversion eval_f; subst.
unfold validIntervalboundsCmd in valid_bounds_f. unfold validIntervalboundsCmd in valid_bounds_f.
...@@ -544,16 +544,16 @@ Proof. ...@@ -544,16 +544,16 @@ Proof.
rewrite <- eq_lo, <- eq_hi. rewrite <- eq_lo, <- eq_hi.
exists v; split; auto. exists v; split; auto.
eapply validIntervalbounds_sound; eauto. eapply validIntervalbounds_sound; eauto.
simpl in freeVars_subset. simpl in usedVars_subset.
hnf. intros a in_freeVars. hnf. intros a in_usedVars.
apply freeVars_subset. apply usedVars_subset.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
rewrite NatSet.diff_spec in in_freeVars. rewrite NatSet.diff_spec in in_usedVars.
destruct in_freeVars as [ in_freeVars not_dVar]. destruct in_usedVars as [ in_usedVars not_dVar].
repeat split; try auto. repeat split; try auto.
{ hnf; intros; subst. { hnf; intros; subst.
apply validVars_subset_freeVars in H2. apply validVars_subset_usedVars in H2.
specialize (H2 n in_freeVars). specialize (H2 n in_usedVars).
rewrite <- NatSet.mem_spec in H2. rewrite <- NatSet.mem_spec in H2.
rewrite H2 in H5; congruence. } rewrite H2 in H5; congruence. }
* apply dVars_sound. rewrite NatSet.mem_spec. * apply dVars_sound. rewrite NatSet.mem_spec.
...@@ -573,7 +573,7 @@ Proof. ...@@ -573,7 +573,7 @@ Proof.
hnf. intros a a_freeVar. hnf. intros a a_freeVar.
rewrite NatSet.diff_spec in a_freeVar. rewrite NatSet.diff_spec in a_freeVar.
destruct a_freeVar as [a_freeVar a_no_dVar]. destruct a_freeVar as [a_freeVar a_no_dVar].
apply freeVars_subset. apply usedVars_subset.
simpl. simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
repeat split; try auto. repeat split; try auto.
......
...@@ -421,15 +421,15 @@ Proof. ...@@ -421,15 +421,15 @@ Proof.
econstructor; eauto. econstructor; eauto.
apply bli; eauto. apply bli; eauto.
apply IHc; auto. apply IHc; auto.
remember (updEnv n0 M0 v (toREvalEnv E)) as E'.
replace E' with (toREvalEnv E') in H9.
+ apply IHc in H9.
rewrite HeqE' in H9.
replace E with (toREvalEnv E) by admit.
apply H9.
Admitted. Admitted.
(* remember (updEnv n0 M0 v (toREvalEnv E)) as E'. *)
(* replace E' with (toREvalEnv E') in H9. *)
(* + apply IHc in H9. *)
(* rewrite HeqE' in H9. *)
(* replace E with (toREvalEnv E) by admit. *)
(* apply H9. *)
(* Admitted. *)
Lemma stepwise_substitution x e v f E vR inVars outVars: Lemma stepwise_substitution x e v f E vR inVars outVars:
ssaPrg (toREvalCmd (toRCmd f)) inVars outVars -> ssaPrg (toREvalCmd (toRCmd f)) inVars outVars ->
...@@ -449,9 +449,9 @@ Proof. ...@@ -449,9 +449,9 @@ Proof.
econstructor; auto. econstructor; auto.
rewrite <- exp_subst_correct; eauto. rewrite <- exp_subst_correct; eauto.
apply bli; apply H7. apply bli; apply H7.
apply bla. (* /!\ *) apply bla.
rewrite <- IHf; eauto. rewrite <- IHf; eauto.
apply bla; auto. (* /!\ *) apply bla; auto.
rewrite NatSet.add_spec; right; auto. rewrite NatSet.add_spec; right; auto.
apply validVars_add; auto. apply validVars_add; auto.
apply bli. apply bli.
...@@ -462,14 +462,14 @@ Proof. ...@@ -462,14 +462,14 @@ Proof.
econstructor. econstructor.
auto. auto.
apply bli. rewrite exp_subst_correct; eauto. apply bli. rewrite exp_subst_correct; eauto.
apply bla in H8; rewrite <- IHf in H8; eauto. (* /!\ *) apply bla in H8; rewrite <- IHf in H8; eauto.
rewrite <- shadowing_free_rewriting_cmd in H8; eauto. rewrite <- shadowing_free_rewriting_cmd in H8; eauto.
admit. (*TODO: modify lemma. eapply ssa_shadowing_free; eauto.*) * admit. (* should be ok. Maybe using updEnv_comp_toREval? *)
rewrite <- exp_subst_correct in H7; eauto. * rewrite <- exp_subst_correct in H7; eauto.
rewrite NatSet.add_spec. rewrite NatSet.add_spec.
right; auto. right; auto.
apply validVars_add; auto. * apply validVars_add; auto.
apply bli. eapply dummy_bind_ok; eauto. * apply bli. eapply dummy_bind_ok; eauto.
- split; [intros bstep_let | intros bstep_subst]. - split; [intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst. + inversion bstep_let; subst.
simpl in *. simpl in *.
...@@ -507,7 +507,7 @@ Proof. ...@@ -507,7 +507,7 @@ Proof.
simpl in subst_step. simpl in subst_step.
case_eq (let_subst f). case_eq (let_subst f).
+ intros f_subst subst_f_eq. + intros f_subst subst_f_eq.
apply bla in H8. (* /!\ *) apply bla in H8.
specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H10 H8 subst_f_eq). specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H10 H8 subst_f_eq).
rewrite subst_f_eq in subst_step. rewrite subst_f_eq in subst_step.
inversion IHf; subst. inversion IHf; 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