diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 84f6b18afe0ef5f6a1e0102171c4676954d30ab4..6984a8930a808f6c623b17eb2509cafec8a9dfdb 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -80,7 +80,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, 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)))). Proof. induction f; unfold validIntervalbounds. @@ -99,7 +99,7 @@ Proof. - intros approx_true v0 v_in_fV; simpl in *. inversion 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. destruct (absenv (Unop u f)); destruct (absenv f); simpl in *. apply andb_prop_elim in approx_unary_true. @@ -173,18 +173,18 @@ Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) (forall v, NatSet.mem v dVars = true -> exists vR, E v = Some vR /\ (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 -> exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> eval_exp 0%R E (toRExp f) vR -> (Q2R (fst (fst(absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. 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. env_assert absenv (Var Q n) absenv_var. destruct absenv_var as [ iv [err absenv_var]]. - specialize (valid_freeVars n). + specialize (valid_usedVars n). 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 *. @@ -205,15 +205,15 @@ Proof. * assert (NatSet.In n (NatSet.singleton n)) as in_singleton by (rewrite NatSet.singleton_spec; auto). rewrite NatSet.mem_spec. - hnf in freeVars_subset. - apply freeVars_subset. + hnf in usedVars_subset. + apply usedVars_subset. rewrite NatSet.diff_spec, NatSet.singleton_spec. split; try auto. hnf; intros in_dVars. rewrite <- NatSet.mem_spec in in_dVars. rewrite in_dVars in case_mem; congruence. - * specialize (valid_freeVars in_fVars); - destruct valid_freeVars as [vR' [vR_def P_valid]]. + * specialize (valid_usedVars in_fVars); + destruct valid_usedVars as [vR' [vR_def P_valid]]. rewrite vR_def in H0; inversion H0; subst. lra. - unfold validIntervalbounds in valid_bounds. @@ -244,7 +244,7 @@ Proof. destruct valid_bounds as [valid_rec valid_unop]. apply Is_true_eq_true in valid_rec. 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. (* TODO: Make lemma *) unfold isSupersetIntv in valid_unop. @@ -262,7 +262,7 @@ Proof. * eapply Rle_trans. Focus 2. apply valid_hi. 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. apply andb_prop_elim in valid_unop. destruct valid_unop as [nodiv0 valid_unop]. @@ -351,15 +351,15 @@ Proof. assert ((Q2R (fst (fst (iv1, err1))) <= v1 <= Q2R (snd (fst (iv1, err1))))%R) as valid_bounds_e1. + apply IHf1; try auto. intros v in_diff_e1. - apply freeVars_subset. + apply usedVars_subset. simpl. rewrite NatSet.diff_spec,NatSet.union_spec. 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. + 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. - apply freeVars_subset. + apply usedVars_subset. simpl. rewrite NatSet.diff_spec, NatSet.union_spec. rewrite NatSet.diff_spec in in_diff_e2. destruct in_diff_e2; split; auto. @@ -506,14 +506,14 @@ Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult): exists vR, E v = Some vR /\ (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 -> absenv (getRetExp f) = ((elo, ehi), err) -> (Q2R elo <= vR <= Q2R ehi)%R. Proof. induction f; 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 eval_f; subst. unfold validIntervalboundsCmd in valid_bounds_f. @@ -544,16 +544,16 @@ Proof. rewrite <- eq_lo, <- eq_hi. exists v; split; auto. eapply validIntervalbounds_sound; eauto. - simpl in freeVars_subset. - hnf. intros a in_freeVars. - apply freeVars_subset. + simpl in usedVars_subset. + hnf. intros a in_usedVars. + apply usedVars_subset. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. - rewrite NatSet.diff_spec in in_freeVars. - destruct in_freeVars as [ in_freeVars not_dVar]. + rewrite NatSet.diff_spec in in_usedVars. + destruct in_usedVars as [ in_usedVars not_dVar]. repeat split; try auto. { hnf; intros; subst. - apply validVars_subset_freeVars in H2. - specialize (H2 n in_freeVars). + apply validVars_subset_usedVars in H2. + specialize (H2 n in_usedVars). rewrite <- NatSet.mem_spec in H2. rewrite H2 in H5; congruence. } * apply dVars_sound. rewrite NatSet.mem_spec. @@ -573,7 +573,7 @@ Proof. hnf. intros a a_freeVar. rewrite NatSet.diff_spec in a_freeVar. destruct a_freeVar as [a_freeVar a_no_dVar]. - apply freeVars_subset. + apply usedVars_subset. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. repeat split; try auto. diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v index 7daf78c6d191373938e6ea1791bec792cb487f66..7220ea9e25c8489fdac644bf717cec7f1fbe8bdd 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -421,15 +421,15 @@ Proof. econstructor; eauto. apply bli; eauto. 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. +(* 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: ssaPrg (toREvalCmd (toRCmd f)) inVars outVars -> @@ -449,9 +449,9 @@ Proof. econstructor; auto. rewrite <- exp_subst_correct; eauto. apply bli; apply H7. - apply bla. +(* /!\ *) apply bla. rewrite <- IHf; eauto. - apply bla; auto. +(* /!\ *) apply bla; auto. rewrite NatSet.add_spec; right; auto. apply validVars_add; auto. apply bli. @@ -462,14 +462,14 @@ Proof. econstructor. auto. 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. - admit. (*TODO: modify lemma. eapply ssa_shadowing_free; eauto.*) - rewrite <- exp_subst_correct in H7; eauto. - rewrite NatSet.add_spec. - right; auto. - apply validVars_add; auto. - apply bli. eapply dummy_bind_ok; eauto. + * admit. (* should be ok. Maybe using updEnv_comp_toREval? *) + * rewrite <- exp_subst_correct in H7; eauto. + rewrite NatSet.add_spec. + right; auto. + * apply validVars_add; auto. + * apply bli. eapply dummy_bind_ok; eauto. - split; [intros bstep_let | intros bstep_subst]. + inversion bstep_let; subst. simpl in *. @@ -507,7 +507,7 @@ Proof. simpl in subst_step. case_eq (let_subst f). + 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). rewrite subst_f_eq in subst_step. inversion IHf; subst.