From 3655c4ff2306b3fbc7a8a91f5781faa35b637218 Mon Sep 17 00:00:00 2001 From: Nikita Zyuzin Date: Thu, 27 Sep 2018 19:23:46 +0200 Subject: [PATCH] Progress cmd proof --- coq/ErrorValidationAA.v | 135 ++++++++++++++++++++++++- coq/ExpressionSemanticsDeterministic.v | 17 +++- 2 files changed, 148 insertions(+), 4 deletions(-) diff --git a/coq/ErrorValidationAA.v b/coq/ErrorValidationAA.v index f41ae59..f2aa279 100644 --- a/coq/ErrorValidationAA.v +++ b/coq/ErrorValidationAA.v @@ -236,8 +236,11 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *) match FloverMap.find e A, FloverMap.find (Var Q x) A with | Some (iv_e, err_e), Some (iv_x, err_x) => if Qeq_bool err_e err_x then - validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1 - (FloverMap.add (Var Q x) afPolye errMap1) + match FloverMap.find (Var Q x) errMap1 with + | Some _ => None + | None => validErrorboundAACmd g typeMap A (NatSet.add x dVars) maxNoise1 + (FloverMap.add (Var Q x) afPolye errMap1) + end else None | _,_ => None @@ -4172,6 +4175,134 @@ Proof. destruct p as (variv, varerr). destruct (Qeq_bool suberr varerr) eqn: Heqerr; cbn in Hvalidbounds; [|congruence]. + destruct (FloverMap.find (Var Q n) subexpr_map) eqn: Hvarnew; + cbn in Hvalidbounds; [congruence|]. + inversion Hssa; subst. + cbn in Hsubset. + assert (NatSet.Subset (usedVars e -- dVars) fVars) as Hsubs. + { set_tac. repeat split; auto. + hnf; intros; subst. + set_tac. } + pose proof (validErrorboundAA_sound e) as Hvalid__e. + inversion Heval__R; subst. + destruct Htypes as ((? & ? & ? & ? & ? & ?) & ?). + destruct Hrange as ((? & ?) & ?). + specialize Hvalid__e as (((v__FP & m__FP & Heval__e) & Hcheckedex__e) & Hvalidall__e); eauto. + assert (NatSet.Equal (NatSet.add n (NatSet.union fVars dVars)) + (NatSet.union fVars (NatSet.add n dVars))) as Hseteq. + { + hnf. intros ?; split; intros in_set; set_tac. + - destruct in_set as [ ? | [? ?]]; try auto; set_tac. + destruct H14; auto. + - destruct in_set as [? | ?]; try auto; set_tac. + destruct H13 as [? | [? ?]]; auto. + } + assert (ssa c (fVars ∪ (NatSet.add n dVars)) outVars) as Hssa'. + { + eapply ssa_equal_set; symmetry in Hseteq. + exact Hseteq. + assumption. + } + assert (NatSet.Subset (freeVars c -- NatSet.add n dVars) fVars) as Hsubset'. + { + hnf. intros ? a_freeVar. + rewrite NatSet.diff_spec in a_freeVar. + destruct a_freeVar as [a_freeVar a_no_dVar]. + apply Hsubset. + simpl. + rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. + repeat split; try auto. + { hnf; intros; subst. + apply a_no_dVar. + rewrite NatSet.add_spec; auto. } + { hnf; intros a_dVar. + apply a_no_dVar. + rewrite NatSet.add_spec; auto. } + } + specialize (Hvalidall__e v__FP m__FP Heval__e) as (af__e & err__e & noise_map2 & ? & ? & ? & ? & ? & ? & + ? & Hiv & ? & Hevals & Hcheckedall__e). + rewrite Qeq_bool_iff in Heqerr. + apply Qeq_eqR in Heqerr. + assert (approxEnv (updEnv n v E1) (toRExpMap Gamma) A fVars + (NatSet.add n dVars) (updEnv n v__FP E2)). + { + eapply approxUpdBound; eauto. + - eapply toRExpMap_some; eauto. + simpl; auto. + - apply Rle_trans with (r2:= err__e); try lra. + apply to_interval_containment in Hevals. + rewrite Hiv in Hevals. + cbn in Hevals. + now apply Rabs_le. + } + specialize (H9 v (eval_det_eval_nondet H10)). + assert (affine_dVars_error_valid (updEnv n v E1) (updEnv n v__FP E2) A Gamma DeltaMap + (NatSet.add n dVars) noise_map2 subnoise + (FloverMap.add (Var Q n) a subexpr_map)). + { + unfold affine_dVars_error_valid. + intros v' Hinv'. + destruct (v' =? n) eqn:Heq. + - unfold checked_error_expressions, updEnv. + intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'. + rewrite Nat.eqb_eq in Heq; subst. + inversion Heval__R'; subst. + inversion Heval__FP'; subst. + unfold updEnv in H24, H26. + rewrite Nat.eqb_refl in H24, H26. + inversion H24; inversion H26; subst. + exists af__e, err__e. + intuition. + + rewrite FloverMapFacts.P.F.add_eq_o; [congruence|]. + apply Q_orderedExps.exprCompare_refl. + + replace err__A' with varerr by congruence. + now rewrite <- Heqerr. + - pose proof Heq as Heq'. + rewrite Nat.eqb_neq in Heq. + apply NatSetProps.FM.add_3 in Hinv'; auto. + move Hdvars at bottom. + specialize (Hdvars v' Hinv'). + unfold checked_error_expressions in Hdvars |-*. + intros v__R' v__FP' m__FP' iv__A' err__A' Heval__R' Heval__FP' Hcert'. + specialize Hdvars as (af' & err__af' & Hfresh' & Hnoisemap1' & Hcertvar' & Herr' & + Hiv' & Herrvar' & Hevals'); eauto. + + inversion Heval__R'; subst. + unfold updEnv in H24. + rewrite Heq' in H24. + constructor; eauto. + + inversion Heval__FP'; subst. + unfold updEnv in H24. + rewrite Heq' in H24. + constructor; eauto. + + exists af', err__af'. + repeat split; eauto using fresh_monotonic, af_evals_map_extension. + rewrite FloverMapFacts.P.F.add_neq_o; [now apply H13|]. + cbn; intros Heq''. + apply nat_compare_eq in Heq''. + 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. + destruct (q_expr_eq_dec (Var Q n) e') as [Heqe'|Hneqe']. + * rewrite FloverMapFacts.P.F.In_iff in Hvarnew; eauto. + specialize (flover_map_el_eq_extension Hvarnew Hin) as [Heq Heqexp]. + rewrite Heqexp. + 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 (vfp & mfp & Hevalfp). + exists vfp, mfp. + eapply eval_expr_det_ssa_extension; eauto. + } admit. - inversion Heval__R; subst. edestruct (validErrorboundAA_sound e) as (((v__FP & m__FP & Hex) & Hcheckedex') & _); eauto; diff --git a/coq/ExpressionSemanticsDeterministic.v b/coq/ExpressionSemanticsDeterministic.v index 1711c5a..afb77f4 100644 --- a/coq/ExpressionSemanticsDeterministic.v +++ b/coq/ExpressionSemanticsDeterministic.v @@ -5,7 +5,7 @@ From Flover.Infra Require Import RealRationalProps RationalSimps Ltacs. From Flover - Require Import ExpressionSemantics. + Require Import ExpressionSemantics ssaPrgs. From Flover.Infra Require Export ExpressionAbbrevs. @@ -344,7 +344,7 @@ Proof. rewrite <- (H n); auto. Qed. -Lemma eval_expr_det_ignore_bind_det e: +Lemma eval_expr_det_ignore_bind e: forall x v m Gamma E DeltaMap, eval_expr_det E Gamma DeltaMap e v m -> ~ NatSet.In x (usedVars e) -> @@ -533,3 +533,16 @@ Proof. + trivial. + apply Rabs_0_impl_eq in H3; f_equal; now symmetry. Qed. + +Lemma eval_expr_det_ssa_extension (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 E Gamma DeltaMap e v m -> + eval_expr_det (updEnv n v' E) Gamma DeltaMap e v m. +Proof. + intros Hssa Hsub Hnotin Heval. + eapply eval_expr_det_ignore_bind; [auto |]. + edestruct ssa_inv_let; eauto. +Qed. -- GitLab