Skip to content
GitLab
Commit 752ac724 authored by Heiko Becker's avatar Heiko Becker
Browse files

Remove not yet used lemmas from ssaPrgs.v to get a clean state before sending next merge request

parent d3d60c41
Hide whitespace changes
Inline Side-by-side
coq/ssaPrgs.v
View file @ 752ac724
......@@ -70,332 +70,3 @@ Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
validVars V e inVars = true ->
NatSet.equal inVars (NatSet.remove 0%nat Vterm) = true->
ssaPrg V (Ret V e) inVars Vterm.
Fixpoint validSSA (f:cmd Q) (inVars:NatSet.t) :=
match f with
|Let _ x e g =>
andb (andb (negb (NatSet.mem x inVars)) (validVars Q e inVars)) (validSSA g (NatSet.add x inVars))
|Ret _ e => validVars Q e inVars && (negb (NatSet.mem 0%nat inVars))
|Nop _ => false
end.
Lemma validSSA_sound f inVars:
validSSA f inVars = true ->
exists outVars, ssaPrg Q f inVars outVars.
Proof.
revert inVars; induction f.
- intros inVars validSSA_let.
simpl in *.
andb_to_prop validSSA_let.
specialize (IHf (NatSet.add n inVars) R).
destruct IHf as [outVars IHf].
exists outVars.
constructor; eauto.
rewrite negb_true_iff in L0. auto.
- intros inVars validSSA_ret.
simpl in *.
exists (NatSet.add 0%nat inVars).
andb_to_prop validSSA_ret.
constructor; auto.
rewrite negb_true_iff in R.
hnf in R.
rewrite NatSet.equal_spec.
hnf.
intros a.
rewrite NatSet.remove_spec, NatSet.add_spec.
split.
+ intros in_inVars.
case_eq (a =? 0%nat).
* intros a_zero.
rewrite Nat.eqb_eq in a_zero.
rewrite a_zero in in_inVars.
rewrite <- NatSet.mem_spec in in_inVars.
rewrite in_inVars in R.
inversion R.
* intros a_neq_zero. apply beq_nat_false in a_neq_zero.
split; auto.
+ intros in_add_rem.
destruct in_add_rem as [ [a_zero | a_inVars] a_neq_zero]; try auto.
exfalso; eauto.
- intros inVars validSSA_nop. simpl in *.
inversion validSSA_nop.
Qed.
Lemma ssa_shadowing_free x y v v' e f inVars outVars VarEnv ParamEnv P:
ssaPrg Q (Let Q x e f) inVars outVars ->
NatSet.In y inVars ->
eval_exp 0 VarEnv ParamEnv P (toRExp e) v ->
forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n.
Proof.
intros ssa_let y_free eval_e.
inversion ssa_let; subst.
intros E n; unfold updEnv.
case_eq (n =? x).
- intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
case_eq (n =? y); try auto.
intros n_eq_y.
rewrite Nat.eqb_eq in n_eq_y.
rewrite n_eq_x in n_eq_y.
rewrite <- n_eq_y in y_free.
rewrite <- NatSet.mem_spec in y_free.
rewrite y_free in H5. inversion H5.
- intros n_neq_x.
case_eq (n =? y); auto.
Qed.
Lemma shadowing_free_rewriting_exp e v VarEnv1 VarEnv2 ParamEnv P:
(forall n, VarEnv1 n = VarEnv2 n) ->
eval_exp 0 VarEnv1 ParamEnv P e v <->
eval_exp 0 VarEnv2 ParamEnv P e v.
Proof.
revert v VarEnv1 VarEnv2 ParamEnv P.
induction e; intros v' VarEnv1 VarEnv2 ParamEnv P agree_on_vars.
- split; intros eval_Var.
+ inversion eval_Var; subst.
rewrite agree_on_vars. constructor.
+ inversion eval_Var; subst.
rewrite <- agree_on_vars; constructor.
- split; intros eval_Param; inversion eval_Param; subst.
+ econstructor.
apply H0. apply H1. apply H2. auto.
+ econstructor.
apply H0. apply H1. apply H2. auto.
- split; intros eval_Const; inversion eval_Const; subst; econstructor; auto.
- split; intros eval_Unop; inversion eval_Unop; subst; econstructor; try auto.
+ erewrite IHe; eauto.
+ erewrite IHe; eauto.
+ erewrite <- IHe; eauto.
+ erewrite <- IHe; eauto.
- split; intros eval_Binop; inversion eval_Binop; subst; econstructor; try auto;
try (erewrite IHe1; eauto);
try (erewrite IHe2; eauto).
Qed.
Lemma shadowing_free_rewriting_cmd f VarEnv1 VarEnv2 ParamEnv P vR:
(forall n, VarEnv1 n = VarEnv2 n) ->
bstep f VarEnv1 ParamEnv P 0 (Nop R) vR <->
bstep f VarEnv2 ParamEnv P 0 (Nop R) vR.
Proof.
revert VarEnv1 VarEnv2 ParamEnv P vR.
induction f; intros VarEnv1 VarEnv2 ParamEnv P vR agree_on_vars.
- split; intros bstep_Let; inversion bstep_Let; subst.
+ erewrite shadowing_free_rewriting_exp in H8; auto.
econstructor; eauto.
rewrite <- IHf.
apply H9.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
+ erewrite <- shadowing_free_rewriting_exp in H8; auto.
econstructor; eauto.
rewrite IHf.
apply H9.
intros n'; unfold updEnv.
case_eq (n' =? n); auto.
- split; intros bstep_Ret; inversion bstep_Ret; subst.
+ erewrite shadowing_free_rewriting_exp in H0; auto.
constructor; auto.
+ erewrite <- shadowing_free_rewriting_exp in H0; auto.
constructor; auto.
- split; intros bstep_Nop; inversion bstep_Nop.
Qed.
Lemma dummy_bind_ok e v x v' inVars VarEnv ParamEnv P:
validVars Q e inVars = true ->
NatSet.mem x inVars = false ->
eval_exp 0 VarEnv ParamEnv P (toRExp e) v ->
eval_exp 0 (updEnv x v' VarEnv) ParamEnv P (toRExp e) v.
Proof.
revert v x v' inVars VarEnv ParamEnv P.
induction e; intros v1 x v2 inVars VarEnv ParamEnv P valid_vars x_not_free eval_e.
- inversion eval_e; subst.
assert ((updEnv x v2 VarEnv) n = VarEnv n).
+ unfold updEnv.
case_eq (n =? x); try auto.
intros n_eq_x.
rewrite Nat.eqb_eq in n_eq_x.
subst; simpl in *.
rewrite x_not_free in valid_vars; inversion valid_vars.
+ rewrite <- H; constructor.
- inversion eval_e; subst; econstructor.
apply H0. apply H1. apply H2. auto.
- inversion eval_e; subst; constructor; auto.
- inversion eval_e; subst; constructor; auto.
+ eapply IHe; eauto.
+ eapply IHe; eauto.
- simpl in valid_vars.
apply Is_true_eq_left in valid_vars.
apply andb_prop_elim in valid_vars.
destruct valid_vars.
inversion eval_e; subst; constructor; auto.
+ eapply IHe1; eauto.
apply Is_true_eq_true; auto.
+ eapply IHe2; eauto.
apply Is_true_eq_true; auto.
Qed.
Fixpoint exp_subst (e:exp Q) x e_new :=
match e with
|Var _ v => if v =? x then e_new else Var Q v
|Unop op e1 => Unop op (exp_subst e1 x e_new)
|Binop op e1 e2 => Binop op (exp_subst e1 x e_new) (exp_subst e2 x e_new)
| e => e
end.
Lemma exp_subst_correct e e_sub VarEnv ParamEnv P x v v_res:
eval_exp (0%R) VarEnv ParamEnv P (toRExp e_sub) v ->
eval_exp (0%R) (updEnv x v VarEnv) ParamEnv P (toRExp e) v_res <->
eval_exp (0%R) VarEnv ParamEnv P (toRExp (exp_subst e x e_sub)) v_res.
Proof.
intros eval_e.
revert v_res.
induction e.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ unfold updEnv in eval_upd. simpl in *.
inversion eval_upd; subst.
case_eq (n =? x); intros; try auto.
constructor.
+ simpl in eval_subst.
case_eq (n =? x); intros n_eq_case;
rewrite n_eq_case in eval_subst.
* simpl.
assert (v_res = (updEnv x v VarEnv) n).
{ unfold updEnv.
rewrite n_eq_case.
eapply meps_0_deterministic; eauto. }
{ rewrite H. constructor. }
* simpl. inversion eval_subst; subst.
assert (VarEnv n = updEnv x v VarEnv n).
{ unfold updEnv; rewrite n_eq_case; reflexivity. }
{ rewrite H; constructor. }
- intros v_res; split; simpl; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; subst. eapply Param_acc.
assumption.
apply H1.
apply H2.
assumption.
+ inversion eval_subst; subst.
eapply Param_acc.
assumption.
apply H1.
apply H2.
assumption.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; auto.
+ inversion eval_subst; constructor; auto.
- split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; try auto.
* rewrite <- IHe. assumption.
* rewrite <- IHe. assumption.
+ inversion eval_subst; constructor; try auto.
* rewrite IHe; assumption.
* rewrite IHe; assumption.
- intros v_res; split; [intros eval_upd | intros eval_subst].
+ inversion eval_upd; constructor; try auto.
* rewrite <- IHe1. assumption.
* rewrite <- IHe2. assumption.
+ inversion eval_subst; constructor; try auto.
* rewrite IHe1; assumption.
* rewrite IHe2; assumption.
Qed.
Fixpoint map_subst (f:cmd Q) x e :=
match f with
|Let _ y e_y g => Let Q y (exp_subst e_y x e) (map_subst g x e)
|Ret _ e_r => Ret Q (exp_subst e_r x e)
|Nop _ => Nop Q
end.
Lemma stepwise_substitution x e v f VarEnv ParamEnv P vR inVars outVars:
ssaPrg Q f inVars outVars ->
NatSet.In x inVars ->
validVars Q e inVars = true ->
eval_exp 0%R VarEnv ParamEnv P (toRExp e) v ->
bstep (toRCmd f) (updEnv x v VarEnv) ParamEnv P 0%R (Nop R) vR <->
bstep (toRCmd (map_subst f x e)) VarEnv ParamEnv P 0%R (Nop R) vR.
Proof.
revert VarEnv ParamEnv e x P vR inVars outVars.
induction f; intros VarEnv ParamEnv e0 x P vR inVars outVars ssa_f x_free valid_vars_e eval_e.
- split; [ intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst.
simpl in *.
inversion ssa_f; subst.
assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var).
* eapply ssa_shadowing_free.
apply ssa_f.
apply x_free.
apply H8.
* rewrite (shadowing_free_rewriting_cmd _ _ _ _ _ _ (H VarEnv)) in H9.
econstructor; auto.
rewrite <- exp_subst_correct; eauto.
rewrite <- IHf; eauto.
rewrite NatSet.add_spec.
right; auto.
apply validVars_add; auto.
eapply dummy_bind_ok; eauto.
+ inversion bstep_subst; subst.
simpl in *.
inversion ssa_f; subst.
econstructor.
rewrite exp_subst_correct; eauto.
rewrite <- IHf in H9; eauto.
rewrite <- shadowing_free_rewriting_cmd in H9; eauto.
eapply ssa_shadowing_free; eauto.
rewrite <- exp_subst_correct in H8; eauto.
rewrite NatSet.add_spec.
right; auto.
apply validVars_add; auto.
eapply dummy_bind_ok; eauto.
- split; [intros bstep_let | intros bstep_subst].
+ inversion bstep_let; subst.
simpl in *.
rewrite exp_subst_correct in H0; eauto.
constructor. assumption.
+ inversion bstep_subst; subst.
simpl in *.
rewrite <- exp_subst_correct in H0; eauto.
constructor; assumption.
- split; intros step; inversion step.
Qed.
Fixpoint let_subst (f:cmd Q) :=
match f with
| Let _ x e1 g =>
match (let_subst g) with
|Some e' => Some (exp_subst e' x e1)
|None => None
end
| Ret _ e1 => Some e1
| Nop _ => None
end.
Theorem let_free_form f VarEnv ParamEnv P vR inVars outVars e:
ssaPrg Q f inVars outVars ->
bstep (toRCmd f) VarEnv ParamEnv P 0 (Nop R) vR ->
let_subst f = Some e ->
bstep (toRCmd (Ret Q e)) VarEnv ParamEnv P 0 (Nop R) vR.
Proof.
revert VarEnv ParamEnv P vR inVars outVars e;
induction f;
intros VarEnv ParamEnv P vR inVars outVars e_subst ssa_f bstep_f subst_step.
- simpl.
inversion bstep_f; subst.
inversion ssa_f; subst.
simpl in subst_step.
case_eq (let_subst f).
+ intros f_subst subst_f_eq.
specialize (IHf (updEnv n v VarEnv) ParamEnv P vR (NatSet.add n inVars) outVars f_subst H6 H9 subst_f_eq).
rewrite subst_f_eq in subst_step.
inversion IHf; subst.
constructor.
inversion subst_step.
subst.
rewrite <- exp_subst_correct; eauto.
+ intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step.
- inversion bstep_f; subst.
constructor.
simpl in *.
inversion subst_step; subst.
assumption.
- simpl in *; inversion subst_step.
Qed.
\ No newline at end of file
Supports Markdown
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