Commit 4e212b4d authored by Joachim Bard's avatar Joachim Bard

fixing ssaPrgs and some Expressions

parent 8d6b69e2
......@@ -120,7 +120,8 @@ Fixpoint validErrorbound (e:expr Q) (* analyzed exprression *)
then
match FloverMap.find e2 A with
| Some (iv_e2, err_e2) => Qeq_bool err_e2 err
| _,_ => false
| _ => false
end
else false
| _,_ => false
end
......
......@@ -1055,6 +1055,85 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
by (rewrite Pos.compare_lt_iff in *;
eapply Pos.lt_trans; eauto);
rewrite G; auto. }
+ destruct (mTypeEq m m0) eqn:?;
destruct (mTypeEq m0 m1) eqn:?;
[type_conv; subst; rewrite mTypeEq_refl | | | ].
{ destruct (n ?= n0)%nat eqn:c1; destruct (n0 ?= n1)%nat eqn:c2; try congruence.
- apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
rewrite Nat.compare_refl.
destruct (exprCompare e1_1 y1) eqn:?;
destruct (exprCompare y1 z1) eqn:?; try congruence.
+ erewrite exprCompare_eq_trans; eauto.
+ erewrite exprCompare_eq_lt_is_lt; eauto.
+ erewrite exprCompare_lt_eq_is_lt; eauto.
+ erewrite IHe1_1; eauto.
- apply Nat.compare_eq in c1. subst.
now rewrite c2.
- apply Nat.compare_eq in c2. subst.
now rewrite c1.
- apply nat_compare_lt in c1. apply nat_compare_lt in c2.
assert (c3: (n ?= n1)%nat = Lt) by (apply nat_compare_lt; omega).
now rewrite c3. }
{ admit. }
{ admit. }
{ admit. }
(*
destruct (morePrecise m m0); destruct m, m0; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
* rewrite mTypeEq_compat_eq in Heqb; subst.
rewrite Heqb0; destruct (morePrecise m0 m1); congruence.
* rewrite mTypeEq_compat_eq in Heqb0; subst.
rewrite Heqb. destruct (morePrecise m m1); congruence.
* destruct (mTypeEq m m1) eqn:?.
{ rewrite mTypeEq_compat_eq in Heqb1; subst.
destruct (morePrecise m1 m0) eqn:prec1;
destruct (morePrecise m0 m1) eqn:prec2;
destruct m1, m0;
try rewrite mTypeEq_refl in *; try congruence;
try pose proof (morePrecise_antisym _ _ prec1 prec2);
type_conv; try congruence;
simpl in *; try congruence;
rewrite Pos.compare_antisym in lt_e2_e3;
rewrite N.compare_antisym in lt_e2_e3;
destruct (w ?= w0) eqn:?; destruct (f ?= f0)%N eqn:?;
cbn in *; try congruence. }
{ type_conv; subst.
destruct (morePrecise m1 m0) eqn:prec1;
destruct (morePrecise m0 m1) eqn:prec2;
destruct m, m0, m1; simpl in *; try congruence; try auto;
try rewrite prec1 in *; try rewrite prec2 in *; try congruence;
destruct (w ?= w0) eqn:case_w0; destruct (w0 ?= w1) eqn:case_w1;
try (apply Ndec.Pcompare_Peqb in case_w0);
try (apply Ndec.Pcompare_Peqb in case_w1);
try rewrite Pos.eqb_eq in *;
try rewrite N.eqb_eq in *;
subst;
try congruence;
try rewrite case_w0;
try rewrite case_w1; try auto;
try rewrite Pos.compare_refl;
try (rewrite N.compare_lt_iff in *; eapply N.lt_trans; eauto);
assert (w ?= w1 = Lt) as G
by (rewrite Pos.compare_lt_iff in *;
eapply Pos.lt_trans; eauto);
rewrite G; auto. }
*)
+ destruct (exprCompare e1_1 y1) eqn:?; try congruence;
destruct (exprCompare y1 z1) eqn:?; try congruence;
try (erewrite exprCompare_eq_lt_is_lt; eauto; fail);
try (erewrite exprCompare_lt_eq_is_lt; eauto; fail);
try (erewrite IHe1_1; eauto; fail).
apply (exprCompare_eq_trans _ _ _ Heqc) in Heqc0;
rewrite Heqc0.
destruct (exprCompare e1_2 y2) eqn:?; try congruence;
destruct (exprCompare y2 z2) eqn:?; try congruence;
try (erewrite exprCompare_eq_trans; eauto; fail);
try (erewrite exprCompare_eq_lt_is_lt; eauto; fail);
try (erewrite exprCompare_lt_eq_is_lt; eauto; fail);
try (erewrite IHe1_2; eauto).
Admitted.
Instance eq_compat: Proper (eq ==> eq ==> iff) eq.
......@@ -1145,8 +1224,79 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; rewrite mTypeEq_refl in *; congruence.
-
Admitted.
- destruct (mTypeEq m m0) eqn:?; destruct (mTypeEq m1 m2) eqn:?;
[type_conv | | |].
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
destruct (mTypeEq m0 m2); try reflexivity; try congruence.
destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e3_1 e4_1) eqn:?;
try congruence.
destruct (n0 ?= n2)%nat; try tauto.
destruct (exprCompare e1_1 e3_1) eqn:?;
destruct (exprCompare e2_1 e4_1) eqn:?;
try (split; congruence).
* now specialize (IHe1_2 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *.
* split; try congruence. intros H.
specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite <- Heqc2. tauto.
* split; try congruence. intros H.
specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite <- Heqc2. tauto.
* split; try congruence. intros H.
specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite <- Heqc1. tauto.
* split; try congruence. intros H.
specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite <- Heqc1. tauto.
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
type_conv.
destruct (morePrecise m1 m2); destruct m1, m2; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
type_conv.
destruct (morePrecise m m0); destruct m, m0; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
type_conv.
destruct (morePrecise m m0); destruct m, m0; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
- try (split; auto; fail);
destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e3_1 e4_1) eqn:?;
try congruence;
destruct (exprCompare e1_1 e3_1) eqn:?;
destruct (exprCompare e2_1 e4_1) eqn:?;
try (split; congruence);
try (specialize (IHe1_2 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *; rewrite IHe1_2 in *; split; auto; fail);
try (split; try congruence; intros);
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite IHe1_1 in *; congruence);
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence);
try (split; auto; fail);
destruct (exprCompare e1_2 e2_2) eqn:?;
destruct (exprCompare e3_2 e4_2) eqn:?;
try congruence;
destruct (exprCompare e1_2 e3_2) eqn:?;
destruct (exprCompare e2_2 e4_2) eqn:?;
try (split; congruence);
try (split; try congruence; intros);
try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite IHe1_2 in *; congruence);
try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite <- IHe1_2 in *; congruence);
try congruence;
erewrite exprCompare_eq_trans; eauto;
erewrite exprCompare_eq_trans; eauto;
rewrite exprCompare_antisym;
now (try rewrite e3_eq_e4; try rewrite e1_eq_e2).
Qed.
Instance lt_compat: Proper (eq ==> eq ==> iff) lt.
Proof.
......@@ -1262,7 +1412,91 @@ Module ExprOrderedType (V_ordered:OrderType) <: OrderType.
apply N.compare_eq in case2;
rewrite Pos.eqb_eq in *; subst; cbn in *;
repeat rewrite N.eqb_refl, Pos.eqb_refl in *; simpl in *; try congruence.
Admitted.
- pose proof eq_compat as eq_comp. unfold Proper, eq in eq_comp.
destruct (mTypeEq m m0) eqn:?; destruct (mTypeEq m1 m2) eqn:?;
[type_conv | | |].
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
destruct (mTypeEq m0 m2); try reflexivity; try congruence.
destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e3_1 e4_1) eqn:?;
try congruence.
destruct (n0 ?= n2)%nat; try tauto.
destruct (exprCompare e1_1 e3_1) eqn:?;
destruct (exprCompare e2_1 e4_1) eqn:?;
try (split; congruence).
* now specialize (IHe1_2 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *.
* specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite <- IHe1_1 in *. congruence.
* pose proof (exprCompare_eq_trans _ _ _ Heqc1 Heqc0).
apply exprCompare_eq_sym in Heqc.
pose proof (exprCompare_eq_trans _ _ _ Heqc H).
congruence.
* specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite IHe1_1 in *. congruence.
* specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *.
rewrite IHe1_1 in *. congruence.
* pose proof (exprCompare_eq_trans _ _ _ Heqc Heqc2).
apply exprCompare_eq_sym in Heqc0.
pose proof (exprCompare_eq_trans _ _ _ H Heqc0).
congruence.
* pose proof (exprCompare_eq_lt_is_lt _ _ _ Heqc Heqc2).
apply exprCompare_eq_sym in Heqc0.
pose proof (exprCompare_lt_eq_is_lt _ _ _ H Heqc0).
congruence.
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
type_conv.
destruct (morePrecise m1 m2); destruct m1, m2; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
+ destruct (n ?= n0)%nat; try congruence.
type_conv.
destruct (morePrecise m m0); destruct m, m0; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
+ destruct (n ?= n0)%nat eqn:c1; destruct (n1 ?= n2)%nat eqn:c2; try congruence.
apply Nat.compare_eq in c1. apply Nat.compare_eq in c2. subst.
type_conv.
destruct (morePrecise m m0); destruct m, m0; try congruence;
destruct (w ?= w0) eqn:c1; destruct (f ?= f0)%N eqn:c2; try congruence;
apply Ndec.Pcompare_Peqb in c1; apply N.compare_eq in c2;
rewrite Pos.eqb_eq in *; subst; congruence.
- pose proof eq_compat as eq_comp. unfold Proper, eq in eq_comp.
destruct (exprCompare e1_1 e2_1) eqn:?;
destruct (exprCompare e3_1 e4_1) eqn:?;
try congruence;
destruct (exprCompare e1_1 e3_1) eqn:?;
destruct (exprCompare e2_1 e4_1) eqn:?;
try (split; congruence);
try (specialize (IHe1_2 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *; rewrite IHe1_2 in *; split; auto; fail);
try (split; try congruence; intros);
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite IHe1_1 in *; congruence);
try (specialize (IHe1_1 _ Heqc _ _ Heqc0); simpl in *; rewrite <- IHe1_1 in *; congruence);
try (rewrite (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence);
try (rewrite <- (eq_comp _ _ Heqc _ _ Heqc0) in *; congruence);
destruct (exprCompare e1_2 e2_2) eqn:?;
destruct (exprCompare e3_2 e4_2) eqn:?;
try congruence;
destruct (exprCompare e1_2 e3_2) eqn:?;
destruct (exprCompare e2_2 e4_2) eqn:?;
try (split; congruence);
try (specialize (IHe1_3 _ e1_eq_e2 _ _ e3_eq_e4); simpl in *; rewrite IHe1_3 in *; split; auto; fail);
try (split; try congruence; intros);
try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite IHe1_2 in *; congruence);
try (specialize (IHe1_2 _ Heqc3 _ _ Heqc4); simpl in *; rewrite <- IHe1_2 in *; congruence);
try (rewrite (eq_comp _ _ Heqc3 _ _ Heqc4) in *; congruence);
try (rewrite <- (eq_comp _ _ Heqc3 _ _ Heqc4) in *; congruence);
try congruence.
+ apply (exprCompare_lt_eq_is_lt _ _ _ H) in e3_eq_e4;
rewrite exprCompare_eq_sym in e1_eq_e2;
now apply (exprCompare_eq_lt_is_lt _ _ _ e1_eq_e2).
+ rewrite exprCompare_eq_sym in e3_eq_e4;
apply (exprCompare_lt_eq_is_lt _ _ _ H) in e3_eq_e4;
now apply (exprCompare_eq_lt_is_lt _ _ _ e1_eq_e2).
Qed.
Lemma compare_spec : forall x y, CompSpec eq lt x y (exprCompare x y).
Proof.
......
......@@ -143,7 +143,6 @@ Proof.
- intros n. set_tac. intros [?|[?|?]]; auto.
Qed.
Lemma ssa_equal_set V (f:expr V) inVars inVars' outVars:
NatSet.Equal inVars' inVars ->
ssa f inVars outVars ->
......@@ -152,10 +151,19 @@ Proof.
intros set_eq ssa_f.
revert set_eq; revert inVars'.
induction ssa_f; constructor; auto.
- admit.
- admit.
- apply IHssa_f2. admit.
Admitted.
- now apply set_eq.
- apply NatSetProps.Dec.F.not_mem_iff. intros ?. set_tac. now apply H, set_eq.
- apply IHssa_f2.
split; set_tac; intros[?|Ha]; auto; apply set_eq in Ha; auto.
Qed.
(* TODO: shows that outVars is not needed *)
Lemma ssa_open_out V (f:expr V) inVars outVars outVars' :
ssa f inVars outVars ->
ssa f inVars outVars'.
Proof.
intros ssa_f. induction ssa_f; constructor; auto.
Qed.
Fixpoint validSSA (f:expr Q) (inVars:NatSet.t) :=
match f with
......@@ -166,7 +174,7 @@ Fixpoint validSSA (f:expr Q) (inVars:NatSet.t) :=
| Fma e1 e2 e3 => validSSA e1 inVars && validSSA e2 inVars && validSSA e3 inVars
| Downcast _ e => validSSA e inVars
| Let m x e g =>
(negb (NatSet.mem x inVars)) && (NatSet.subset (freeVars e) inVars) && (validSSA g (NatSet.add x inVars))
(negb (NatSet.mem x inVars)) && validSSA e inVars && validSSA g (NatSet.add x inVars)
| Cond e1 e2 e3 => validSSA e1 inVars && validSSA e2 inVars && validSSA e3 inVars
end.
......@@ -174,78 +182,96 @@ Lemma validSSA_sound f inVars:
validSSA f inVars = true ->
exists outVars, ssa f inVars outVars.
Proof.
(*
revert inVars; induction f.
- intros inVars validSSA_let.
simpl in *.
andb_to_prop validSSA_let.
specialize (IHf2 (NatSet.add n inVars) R).
destruct IHf2 as [outVars IHf].
exists outVars.
constructor; eauto.
+ rewrite <- NatSet.subset_spec; auto.
+ rewrite negb_true_iff in L0. auto.
- intros inVars validSSA_ret.
simpl in *.
exists inVars.
constructor; auto.
+ rewrite <- NatSet.subset_spec; auto.
+ hnf; intros; split; auto.
induction f in inVars |- *; cbn; intros H.
- exists NatSet.empty. constructor. set_tac.
- exists NatSet.empty. constructor.
- destruct (IHf _ H) as [O ?]. exists O.
now constructor.
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
exists (O1 O2).
constructor; eauto using ssa_open_out.
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
edestruct IHf3 as [O3 ?]; eauto.
exists (O1 O2 O3).
constructor; eauto using ssa_open_out.
- destruct (IHf _ H) as [O ?]. exists O.
now constructor.
- andb_to_prop H.
apply negb_true_iff in L0.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
exists (O1 O2).
constructor; eauto using ssa_open_out.
- andb_to_prop H.
edestruct IHf1 as [O1 ?]; eauto.
edestruct IHf2 as [O2 ?]; eauto.
edestruct IHf3 as [O3 ?]; eauto.
exists (O1 O2 O3).
constructor; eauto using ssa_open_out.
Qed.
*)
Admitted.
Lemma validSSA_checks_freeVars f S :
validSSA f S = true ->
NatSet.Subset (freeVars f) S.
Proof.
(*
induction f in S |- *; intros * validSSA_true; cbn in *.
induction f in S |- *; intros * validSSA_true; cbn in *; set_tac.
- now subst.
- apply IHf; auto.
- andb_to_prop validSSA_true.
destruct H; [apply IHf1 | apply IHf2]; auto.
- andb_to_prop validSSA_true.
destruct H; set_tac; [apply IHf1 | destruct H; [apply IHf2 | apply IHf3]]; auto.
- apply IHf; auto.
- andb_to_prop validSSA_true.
destruct H; [apply IHf1; auto |].
pose proof (IHf2 _ R).
intros x; set_tac.
apply NatSetProps.FM.subset_2 in R0.
intros [?|[? ?]]; try now set_tac.
pose proof (H _ H0).
clear R0. set_tac. intuition.
- now apply NatSetProps.FM.subset_2.
revert H. set_tac.
intros [? ?].
pose proof (H0 _ H).
set_tac. firstorder.
- andb_to_prop validSSA_true.
destruct H; set_tac; [apply IHf1 | destruct H; [apply IHf2 | apply IHf3]]; auto.
Qed.
*)
Admitted.
Lemma validSSA_eq_set s s' f :
NatSet.Equal s' s -> validSSA f s = true -> validSSA f s' = true.
Proof.
(*
induction f in s, s' |- *; intros sub ?.
induction f in s, s' |- *; cbn; intros sub ?; auto.
- set_tac. now apply sub.
- eapply IHf; eauto.
- andb_to_prop H.
erewrite IHf1, IHf2; eauto.
- andb_to_prop H.
erewrite IHf1, IHf2, IHf3; eauto.
- eapply IHf; eauto.
- andb_to_prop H.
apply andb_true_iff; split.
apply andb_true_iff; split.
+ apply negb_true_iff.
apply negb_true_iff in L0.
set_tac.
apply NatSetProps.FM.not_mem_iff.
apply NatSetProps.FM.not_mem_iff in L0.
apply NatSetProps.subset_equal in sub.
intros ?. auto.
intros ?. apply L0. now apply sub.
+ eapply IHf1; eauto.
(*
+ apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in R0.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
set_tac.
+ fold validSSA in *.
eapply IHf2; eauto.
*)
+ eapply IHf2; eauto.
assert (NatSet.Subset s' s) by now apply NatSetProps.subset_equal in sub.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
split; set_tac; intuition.
- apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in H.
apply NatSetProps.equal_sym in sub.
apply NatSetProps.subset_equal in sub.
set_tac.
- andb_to_prop H.
erewrite IHf1, IHf2, IHf3; eauto.
Qed.
*)
Admitted.
Lemma validSSA_downward_closed S S' f :
NatSet.Subset (freeVars f) S' ->
......@@ -253,27 +279,34 @@ Lemma validSSA_downward_closed S S' f :
validSSA f S = true ->
validSSA f S' = true.
Proof.
(*
induction f in S, S' |- *.
- intros sub1 sub2 H. andb_to_prop H.
induction f in S, S' |- *; cbn; set_tac.
- eauto.
- andb_to_prop H1.
erewrite IHf1, IHf2; eauto; set_tac.
- andb_to_prop H1.
erewrite IHf1, IHf2, IHf3; eauto; set_tac.
- eauto.
- andb_to_prop H1.
apply andb_true_intro; split.
apply andb_true_intro; split.
+ apply negb_true_iff.
apply NatSetProps.FM.not_mem_iff.
apply negb_true_iff in L0.
apply NatSetProps.FM.not_mem_iff in L0.
intros ?. apply L0. now apply sub2.
set_tac.
apply NatSetProps.FM.not_mem_iff.
intros ?. apply L0. now apply H0.
+ eapply IHf1; eauto. set_tac.
(*
+ apply NatSetProps.FM.subset_1.
apply NatSetProps.FM.subset_2 in R0.
set_tac.
+ fold validSSA in *. eapply IHf2; eauto.
*)
+ eapply IHf2; eauto.
* set_tac.
destruct (dec_eq_nat a n); [now left | right; set_tac].
* set_tac. intuition.
- intros. now apply NatSetProps.FM.subset_1.
- andb_to_prop H1.
erewrite IHf1, IHf2, IHf3; eauto; set_tac.
Qed.
*)
Admitted.
Lemma ssa_shadowing_free m x y v v' e f inVars outVars E Gamma DeltaMap:
ssa (Let m x (toREval (toRExp e)) (toREval (toRExp f))) inVars outVars ->
......@@ -281,7 +314,6 @@ Lemma ssa_shadowing_free m x y v v' e f inVars outVars E Gamma DeltaMap:
eval_expr E Gamma DeltaMap (toREval (toRExp e)) v REAL ->
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.
......@@ -294,24 +326,22 @@ Proof.
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 H6. inversion H6.
congruence.
- intros n_neq_x.
case_eq (n =? y); auto.
Qed.
*)
Admitted.
Lemma ssa_inv_let V (e: expr V) m x g inVars outVars:
ssa (Let m x e g) inVars outVars ->
~ NatSet.In x inVars /\ ~ NatSet.In x (freeVars e).
Proof.
(*
intros ssa_let.
inversion ssa_let; subst.
set_tac.
split; auto.
intros x_free.
eapply ssa_subset_freeVars in x_free; eauto.
Qed.
*)
Admitted.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma DeltaMap
vR vR' m m__e n c fVars dVars outVars:
......@@ -320,14 +350,11 @@ Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma DeltaMap
~ (n fVars dVars) ->
eval_expr E Gamma DeltaMap e vR m__e ->
eval_expr (updEnv n vR' E) Gamma DeltaMap e vR m__e.
(*
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
Qed.
*)
Admitted.
Lemma eval_expr_ssa_extension2 (e: expr R) (e' : expr Q) E Gamma DeltaMap
v v' m__e m n c fVars dVars outVars:
......@@ -336,14 +363,11 @@ Lemma eval_expr_ssa_extension2 (e: expr R) (e' : expr Q) E Gamma DeltaMap
~ (n fVars dVars) ->
eval_expr (updEnv n v' E) Gamma DeltaMap e v m ->
eval_expr E Gamma DeltaMap e v m.
(*
Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_det_ignore_bind2; [eauto |].
edestruct ssa_inv_let; eauto.
Qed.
*)
Admitted.
(*
Lemma shadowing_free_rewriting_expr e v E1 E2 defVars:
......
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