Skip to content

GitLab

Commit 12993b6d authored by Joachim Bard's avatar Joachim Bard
Browse files
Options

more work on admits

parent bf5f1fb2
Hide whitespace changes
Inline Side-by-side
Showing with 58 additions and 34 deletions
coq/RealRangeArith.v
View file @ 12993b6d
...@@ -380,18 +380,15 @@ Proof. ...@@ -380,18 +380,15 @@ Proof.
rewrite Heq, e3, e4; auto. rewrite Heq, e3, e4; auto.
Qed. Qed.
Lemma validRanges_ssa_extension (e: expr Q) (e' : expr Q) A E Gamma Lemma validRanges_ssa_extension (e: expr Q) A E Gamma
vR' m n c fVars dVars outVars: vR' n fVars:
ssa (Let m n e' c) (fVars ∪ dVars) outVars -> (* maybe not needed *) NatSet.Subset (freeVars e) fVars ->
NatSet.Subset (freeVars e) (fVars ∪ dVars) -> ~ (n ∈ fVars) ->
~ (n ∈ fVars ∪ dVars) ->
validRanges e A E Gamma -> validRanges e A E Gamma ->
validRanges e A (updEnv n vR' E) Gamma. validRanges e A (updEnv n vR' E) Gamma.
(*(updDefVars (Var R n) REAL Gamma). *)
Proof. Proof.
(* induction e in E, fVars |- *;
intros Hssa Hsub Hnotin Hranges. intros Hsub Hnotin Hranges.
induction e.
- split; auto. - split; auto.
destruct Hranges as [_ [iv [err [vR Hranges]]]]. destruct Hranges as [_ [iv [err [vR Hranges]]]].
exists iv, err, vR; intuition. exists iv, err, vR; intuition.
...@@ -408,7 +405,7 @@ Proof. ...@@ -408,7 +405,7 @@ Proof.
eapply eval_expr_ssa_extension; try eassumption. *) eapply eval_expr_ssa_extension; try eassumption. *)
- simpl in Hsub. - simpl in Hsub.
destruct Hranges as [Hunopranges Hranges]. destruct Hranges as [Hunopranges Hranges].
specialize (IHe Hsub Hunopranges). specialize (IHe _ _ Hsub Hnotin Hunopranges).
split; auto. split; auto.
destruct Hranges as [iv [err [vR Hranges]]]. destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition. exists iv, err, vR; intuition.
...@@ -416,13 +413,13 @@ Proof. ...@@ -416,13 +413,13 @@ Proof.
(* eapply swap_Gamma_eval_expr. (* eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm. eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *) eapply eval_expr_ssa_extension; try eassumption. *)
rewrite usedVars_toREval_toRExp_compat; auto. rewrite freeVars_toREval_toRExp_compat; auto.
- simpl in Hsub. - simpl in Hsub.
assert (NatSet.Subset (usedVars e1) (fVars ∪ dVars)) as Hsub1 by set_tac. assert (NatSet.Subset (freeVars e1) fVars) as Hsub1 by set_tac.
assert (NatSet.Subset (usedVars e2) (fVars ∪ dVars)) as Hsub2 by (clear Hsub1; set_tac). assert (NatSet.Subset (freeVars e2) fVars) as Hsub2 by (clear Hsub1; set_tac).
destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges]. destruct Hranges as [[Hdiv [Hranges1 Hranges2]] Hranges].
specialize (IHe1 Hsub1 Hranges1). specialize (IHe1 _ _ Hsub1 Hnotin Hranges1).
specialize (IHe2 Hsub2 Hranges2). specialize (IHe2 _ _ Hsub2 Hnotin Hranges2).
simpl. simpl.
repeat split; auto. repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]]. destruct Hranges as [iv [err [vR Hranges]]].
...@@ -432,15 +429,15 @@ Proof. ...@@ -432,15 +429,15 @@ Proof.
eapply Rmap_updVars_comm. eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *) eapply eval_expr_ssa_extension; try eassumption. *)
simpl. simpl.
repeat rewrite usedVars_toREval_toRExp_compat; auto. rewrite !freeVars_toREval_toRExp_compat; auto.
- simpl in Hsub. - simpl in Hsub.
assert (NatSet.Subset (usedVars e1) (fVars ∪ dVars)) as Hsub1 by set_tac. assert (NatSet.Subset (freeVars e1) fVars) as Hsub1 by set_tac.
assert (NatSet.Subset (usedVars e2) (fVars ∪ dVars)) as Hsub2 by (clear Hsub1; set_tac). assert (NatSet.Subset (freeVars e2) fVars) as Hsub2 by (clear Hsub1; set_tac).
assert (NatSet.Subset (usedVars e3) (fVars ∪ dVars)) as Hsub3 by (clear Hsub1 Hsub2; set_tac). assert (NatSet.Subset (freeVars e3) fVars) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges]. destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
specialize (IHe1 Hsub1 Hranges1). specialize (IHe1 _ _ Hsub1 Hnotin Hranges1).
specialize (IHe2 Hsub2 Hranges2). specialize (IHe2 _ _ Hsub2 Hnotin Hranges2).
specialize (IHe3 Hsub3 Hranges3). specialize (IHe3 _ _ Hsub3 Hnotin Hranges3).
simpl. simpl.
repeat split; auto. repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]]. destruct Hranges as [iv [err [vR Hranges]]].
...@@ -450,10 +447,10 @@ Proof. ...@@ -450,10 +447,10 @@ Proof.
eapply Rmap_updVars_comm. eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *) eapply eval_expr_ssa_extension; try eassumption. *)
simpl. simpl.
repeat rewrite usedVars_toREval_toRExp_compat; auto. rewrite !freeVars_toREval_toRExp_compat; auto.
- simpl in Hsub. - simpl in Hsub.
destruct Hranges as [Hranges' Hranges]. destruct Hranges as [Hranges' Hranges].
specialize (IHe Hsub Hranges'). specialize (IHe _ _ Hsub Hnotin Hranges').
split; auto. split; auto.
destruct Hranges as [iv [err [vR Hranges]]]. destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition. exists iv, err, vR; intuition.
...@@ -461,7 +458,35 @@ Proof. ...@@ -461,7 +458,35 @@ Proof.
(* eapply swap_Gamma_eval_expr. (* eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm. eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *) eapply eval_expr_ssa_extension; try eassumption. *)
rewrite usedVars_toREval_toRExp_compat; auto. rewrite freeVars_toREval_toRExp_compat; auto.
Qed. - simpl in Hsub.
*) assert (NatSet.Subset (freeVars e1) fVars) as Hsub1 by set_tac.
destruct Hranges as [[Hranges1 Hranges2] Hranges].
specialize (IHe1 _ _ Hsub1 Hnotin Hranges1).
destruct Hranges as [iv [err [vR Hranges]]].
repeat split; auto.
+ intros.
admit.
+ exists iv, err, vR; intuition.
eapply eval_expr_ssa_extension; eauto.
cbn.
rewrite !freeVars_toREval_toRExp_compat; auto.
- simpl in Hsub.
assert (NatSet.Subset (freeVars e1) fVars) as Hsub1 by set_tac.
assert (NatSet.Subset (freeVars e2) fVars) as Hsub2 by (clear Hsub1; set_tac).
assert (NatSet.Subset (freeVars e3) fVars) as Hsub3 by (clear Hsub1 Hsub2; set_tac).
destruct Hranges as [[Hranges1 [Hranges2 Hranges3]] Hranges].
specialize (IHe1 _ _ Hsub1 Hnotin Hranges1).
specialize (IHe2 _ _ Hsub2 Hnotin Hranges2).
specialize (IHe3 _ _ Hsub3 Hnotin Hranges3).
simpl.
repeat split; auto.
destruct Hranges as [iv [err [vR Hranges]]].
exists iv, err, vR; intuition.
eapply eval_expr_ssa_extension; eauto.
(* eapply swap_Gamma_eval_expr.
eapply Rmap_updVars_comm.
eapply eval_expr_ssa_extension; try eassumption. *)
simpl.
rewrite !freeVars_toREval_toRExp_compat; auto.
Admitted. Admitted.
coq/ssaPrgs.v
View file @ 12993b6d
...@@ -343,17 +343,16 @@ Proof. ...@@ -343,17 +343,16 @@ Proof.
eapply ssa_subset_freeVars in x_free; eauto. eapply ssa_subset_freeVars in x_free; eauto.
Qed. Qed.
Lemma eval_expr_ssa_extension (e: expr R) (e' : expr Q) E Gamma DeltaMap Lemma eval_expr_ssa_extension (e: expr R) E Gamma DeltaMap
vR vR' m m__e n c fVars dVars outVars: vR vR' m__e n fVars:
ssa (Let m n e' c) (fVars ∪ dVars) outVars -> NatSet.Subset (freeVars e) fVars ->
NatSet.Subset (freeVars e) (fVars ∪ dVars) -> ~ (n ∈ fVars) ->
~ (n ∈ fVars ∪ dVars) ->
eval_expr E Gamma DeltaMap e vR m__e -> eval_expr E Gamma DeltaMap e vR m__e ->
eval_expr (updEnv n vR' E) Gamma DeltaMap e vR m__e. eval_expr (updEnv n vR' E) Gamma DeltaMap e vR m__e.
Proof. Proof.
intros Hssa Hsub Hnotin Heval. intros Hsub Hnotin Heval.
eapply eval_expr_ignore_bind; [auto |]. eapply eval_expr_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto. intros ?. apply Hnotin. set_tac.
Qed. Qed.
Lemma eval_expr_ssa_extension2 (e: expr R) (e' : expr Q) E Gamma DeltaMap Lemma eval_expr_ssa_extension2 (e: expr R) (e' : expr Q) E Gamma DeltaMap
......
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