Commit f1e16644 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Progress cmd soundness

parent 21315d44
......@@ -4302,100 +4302,140 @@ Proof.
auto.
}
rewrite <- FloverMapFacts.P.F.not_find_in_iff in Hvarnew.
specialize IHc with (dVars := NatSet.add n dVars) as (IHex & _); eauto.
+ lia.
+ intros e' Hin.
specialize IHc with (dVars := NatSet.add n dVars) as (IHex & IHall); eauto; [lia|idtac|idtac|].
{
intros e' Hin.
destruct (q_expr_eq_dec (Var Q n) e') as [Heqe'|Hneqe'].
* rewrite FloverMapFacts.P.F.In_iff in Hvarnew; eauto.
- rewrite FloverMapFacts.P.F.In_iff in Hvarnew; eauto.
specialize (flover_map_el_eq_extension Hvarnew Hin) as [Heq Heqexp].
rewrite Heqexp.
split.
{
rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
+ rewrite usedVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
cbn; set_tac.
}
exists v__FP, m.
constructor; auto.
1: eapply toRExpMap_some with (e := Var Q n); eauto.
unfold updEnv.
now rewrite <- beq_nat_refl.
* rewrite FloverMapFacts.P.F.add_neq_in_iff in Hin; auto.
{
destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
- move Hcheckedex at bottom.
specialize (Hcheckedex _ Hin1).
destruct Hcheckedex as (Hsubsete' & vfp & mfp & Hevalfp).
split.
{
rewrite NatSetProps.union_sym.
rewrite NatSetProps.union_add.
apply NatSetProps.subset_add_2.
now rewrite NatSetProps.union_sym.
}
exists vfp, mfp.
+ exists v__FP, m.
constructor; auto.
1: eapply toRExpMap_some with (e := Var Q n); eauto.
unfold updEnv.
now rewrite <- beq_nat_refl.
- rewrite FloverMapFacts.P.F.add_neq_in_iff in Hin; auto.
destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
+ move Hcheckedex at bottom.
specialize (Hcheckedex _ Hin1).
destruct Hcheckedex as (Hsubsete' & vfp & mfp & Hevalfp).
split.
* rewrite NatSetProps.union_sym.
rewrite NatSetProps.union_add.
apply NatSetProps.subset_add_2.
now rewrite NatSetProps.union_sym.
* exists vfp, mfp.
eapply eval_expr_det_ssa_extension; eauto; [now rewrite usedVars_toRExp_compat|].
specialize ssa_inv_let as (? & ?); eauto.
- specialize (Hcheckedex__e _ Hnin1 Hin).
destruct Hcheckedex__e as (Hsubsete' & vfp & mfp & Hevalfp).
split.
{
rewrite NatSetProps.union_sym.
rewrite NatSetProps.union_add.
apply NatSetProps.subset_add_2.
now rewrite NatSetProps.union_sym.
}
exists vfp, mfp.
+ specialize (Hcheckedex__e _ Hnin1 Hin).
destruct Hcheckedex__e as (Hsubsete' & vfp & mfp & Hevalfp).
split.
* rewrite NatSetProps.union_sym.
rewrite NatSetProps.union_add.
apply NatSetProps.subset_add_2.
now rewrite NatSetProps.union_sym.
* exists vfp, mfp.
eapply eval_expr_det_ssa_extension; eauto; [now rewrite usedVars_toRExp_compat|].
specialize ssa_inv_let as (? & ?); eauto.
}
+ intros e' Hin.
}
{
intros e' Hin.
destruct (q_expr_eq_dec (Var Q n) e') as [Heqe'|Hneqe'].
* rewrite FloverMapFacts.P.F.In_iff in Hvarnew; eauto.
- rewrite FloverMapFacts.P.F.In_iff in Hvarnew; eauto.
specialize (flover_map_el_eq_extension Hvarnew Hin) as [Heq Heqexp].
unfold checked_error_expressions.
rewrite Heqexp.
intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'.
exists af__e, err__e.
{
repeat split; auto.
- replace af__e with a by congruence.
eapply FloverMapFacts.P.F.add_eq_o; auto.
- erewrite FloverMapFacts.P.F.find_o in Hvarcert; eauto.
replace err__A' with varerr by congruence.
now rewrite <- Heqerr.
- inversion Heval__R'; subst.
inversion Heval__FP'; subst.
unfold updEnv in H25, H27.
rewrite <- beq_nat_refl in H25.
rewrite <- beq_nat_refl in H27.
inversion H25; subst.
inversion H27; subst.
assumption.
}
* rewrite FloverMapFacts.P.F.add_neq_in_iff in Hin; auto.
{
destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
- move Hcheckedex at bottom.
unfold checked_error_expressions.
intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'.
move Hcheckedall at bottom.
specialize (Hcheckedall _ Hin1 v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert').
eapply eval_expr_det_ssa_extension; eauto; [now rewrite usedVars_toRExp_compat|].
repeat split; auto.
+ replace af__e with a by congruence.
eapply FloverMapFacts.P.F.add_eq_o; auto.
+ erewrite FloverMapFacts.P.F.find_o in Hvarcert; eauto.
replace err__A' with varerr by congruence.
now rewrite <- Heqerr.
+ inversion Heval__R'; subst.
inversion Heval__FP'; subst.
unfold updEnv in H25, H27.
rewrite <- beq_nat_refl in H25.
rewrite <- beq_nat_refl in H27.
inversion H25; subst.
inversion H27; subst.
assumption.
- rewrite FloverMapFacts.P.F.add_neq_in_iff in Hin; auto.
destruct (flover_map_in_dec e' expr_map1) as [Hin1|Hnin1].
+ move Hcheckedex at bottom.
unfold checked_error_expressions.
intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'.
move Hcheckedall at bottom.
move Hcheckedex at bottom.
specialize (Hcheckedex _ Hin1) as (Hsubset__e' & _).
specialize (Hcheckedall _ Hin1).
assert (contained_flover_map expr_map1 (FloverMap.add (Var Q n) a subexpr_map)).
{
etransitivity; eauto.
apply contained_flover_map_extension.
now apply FloverMapFacts.P.F.not_find_in_iff.
}
apply checked_error_expressions_extension with
(noise_map2 := noise_map2) (noise2 := subnoise)
(expr_map2 := FloverMap.add (Var Q n) a subexpr_map) in Hcheckedall; auto.
specialize (Hcheckedall v__R' v__FP' m__FP' iv__A' err__A').
apply Hcheckedall.
* eapply eval_expr_det_ssa_extension2; eauto;
[now rewrite usedVars_toREval_toRExp_compat|].
specialize ssa_inv_let as (? & ?); eauto.
- specialize (Hcheckedex__e _ Hnin1 Hin).
destruct Hcheckedex__e as (Hsubsete' & vfp & mfp & Hevalfp).
split.
{
rewrite NatSetProps.union_sym.
rewrite NatSetProps.union_add.
apply NatSetProps.subset_add_2.
now rewrite NatSetProps.union_sym.
}
exists vfp, mfp.
eapply eval_expr_det_ssa_extension; eauto; [now rewrite usedVars_toRExp_compat|].
* eapply eval_expr_det_ssa_extension2; eauto;
[now rewrite usedVars_toRExp_compat|].
specialize ssa_inv_let as (? & ?); eauto.
* congruence.
+ unfold checked_error_expressions.
intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'.
move Hcheckedall__e at bottom.
move Hcheckedex__e at bottom.
specialize (Hcheckedex__e _ Hnin1 Hin).
destruct Hcheckedex__e as (Hsubset__e' & _).
specialize (Hcheckedall__e _ Hnin1 Hin).
assert (contained_flover_map subexpr_map (FloverMap.add (Var Q n) a subexpr_map)).
{
apply contained_flover_map_extension.
now apply FloverMapFacts.P.F.not_find_in_iff.
}
apply checked_error_expressions_extension with
(noise_map2 := noise_map2) (noise2 := subnoise)
(expr_map2 := FloverMap.add (Var Q n) a subexpr_map) in Hcheckedall__e; auto; trivial.
unfold checked_error_expressions in Hcheckedall__e.
eapply Hcheckedall__e.
* eapply eval_expr_det_ssa_extension2; eauto;
[now rewrite usedVars_toREval_toRExp_compat|].
specialize ssa_inv_let as (? & ?); eauto.
* eapply eval_expr_det_ssa_extension2; eauto;
[now rewrite usedVars_toRExp_compat|].
specialize ssa_inv_let as (? & ?); eauto.
}
* instantiate (1 := iv__A'). congruence.
* reflexivity.
}
split.
+ clear IHall.
destruct IHex as (v__FP' & m__FP' & IHex).
exists v__FP', m__FP'.
assert (FloverMap.find (elt:=mType) e Gamma = Some m).
{
clear - H H0 H1.
rewrite H.
f_equal.
symmetry.
now rewrite <- mTypeEq_compat_eq.
}
econstructor; eauto.
replace m with m__FP; auto.
symmetry.
apply eval_det_eval_nondet in Heval__e.
eapply validTypes_exec; eauto.
+ admit.
- inversion Heval__R; subst.
edestruct (validErrorboundAA_sound e) as (((v__FP & m__FP & Hex) & Hcheckedex') & _); eauto;
[now destruct Hrange|now destruct Htypes|].
......
......@@ -375,6 +375,38 @@ Proof.
set_tac.
Qed.
Lemma eval_expr_det_ignore_bind2 e:
forall x v v_new m Gamma E DeltaMap,
eval_expr_det (updEnv x v_new E) Gamma DeltaMap e v m ->
~ NatSet.In x (usedVars e) ->
eval_expr_det E Gamma DeltaMap e v m.
Proof.
induction e; intros * eval_e no_usedVar *; cbn in *;
inversion eval_e; subst; try eauto.
- assert (n <> x).
{ hnf. intros. subst. apply no_usedVar; set_tac. }
rewrite <- Nat.eqb_neq in H.
eapply Var_load_det.
+ unfold updDefVars.
cbn.
apply beq_nat_false in H.
destruct (n ?= x)%nat eqn:?; try auto.
+ unfold updEnv.
rewrite <- H1.
unfold updEnv.
now rewrite H.
- eapply Binop_dist_det'; eauto;
[ eapply IHe1 | eapply IHe2];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
- eapply Fma_dist_det'; eauto;
[eapply IHe1 | eapply IHe2 | eapply IHe3];
eauto;
hnf; intros; eapply no_usedVar;
set_tac.
Qed.
Lemma swap_Gamma_eval_expr_det e E vR m Gamma1 Gamma2 DeltaMap:
(forall e, Gamma1 e = Gamma2 e) ->
eval_expr_det E Gamma1 DeltaMap e vR m ->
......@@ -546,3 +578,16 @@ Proof.
eapply eval_expr_det_ignore_bind; [auto |].
edestruct ssa_inv_let; eauto.
Qed.
Lemma eval_expr_det_ssa_extension2 (e: expr R) (e' : expr Q) E Gamma DeltaMap
v v' m__e m n c fVars dVars outVars:
ssa (Let m__e n e' c) (fVars dVars) outVars ->
NatSet.Subset (usedVars e) (fVars dVars) ->
~ (n fVars dVars) ->
eval_expr_det (updEnv n v' E) Gamma DeltaMap e v m ->
eval_expr_det 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.
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