From b08371d27fb5d04de8ef6cd2fa11fa7e5b973510 Mon Sep 17 00:00:00 2001 From: Joachim Bard Date: Thu, 18 Oct 2018 11:04:06 +0200 Subject: [PATCH] include NotQ in eval of queries, adjust testcase; no open proofs --- coq/SMTArith.v | 13 ++++++++++++ coq/smt_bottom_up.v | 50 ++++++++++++++++++++++++++++++--------------- 2 files changed, 47 insertions(+), 16 deletions(-) diff --git a/coq/SMTArith.v b/coq/SMTArith.v index d56c77c..8c25583 100644 --- a/coq/SMTArith.v +++ b/coq/SMTArith.v @@ -72,6 +72,18 @@ Inductive eval_smt (E: env) : SMTArith -> R -> Prop := | DivQ_eval e1 e2 v1 v2 : v2 <> 0 -> eval_smt E e1 v1 -> eval_smt E e2 v2 -> eval_smt E (DivQ e1 e2) (v1 / v2). +Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop := + match q with + | LessQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 < v2 + | LessEqQ e1 e2 => exists v1 v2, eval_smt E e1 v1 /\ eval_smt E e2 v2 /\ v1 <= v2 + | EqualsQ e1 e2 => exists v, eval_smt E e1 v /\ eval_smt E e2 v + | NotQ q => ~ (eval_smt_logic E q) + | AndQ q1 q2 => eval_smt_logic E q1 /\ eval_smt_logic E q2 + | OrQ q1 q2 => eval_smt_logic E q1 \/ eval_smt_logic E q2 + end. + +(* +(* Does not work for NotQ *) Inductive eval_smt_logic (E: env) : SMTLogic -> Prop := | LessQ_eval e1 e2 v1 v2 : eval_smt E e1 v1 -> eval_smt E e2 v2 -> v1 < v2 -> eval_smt_logic E (LessQ e1 e2) @@ -84,6 +96,7 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop := eval_smt_logic E q1 -> eval_smt_logic E q2 -> eval_smt_logic E (AndQ q1 q2) | OrQ_eval_l q1 q2 : eval_smt_logic E q1 -> eval_smt_logic E (OrQ q1 q2) | OrQ_eval_r q1 q2 : eval_smt_logic E q2 -> eval_smt_logic E (OrQ q1 q2). +*) Fixpoint SMTArith2Expr (e: SMTArith) : expr Q := match e with diff --git a/coq/smt_bottom_up.v b/coq/smt_bottom_up.v index 93ebf31..a0097d8 100644 --- a/coq/smt_bottom_up.v +++ b/coq/smt_bottom_up.v @@ -49,8 +49,8 @@ Proof with try (right; apply Rabs_R0). apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... Qed. -Lemma eval_expr_smt E e v : - eval_expr E (fun _ => Some REAL) (toREval (toRExp (SMTArith2Expr e))) v REAL +Lemma eval_expr_smt E Gamma e v : + eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL -> eval_smt E e v. Proof. induction e in v |- *; cbn; intros H. @@ -58,24 +58,25 @@ Proof. - inversion H. cbn. constructor; auto. - inversion H. cbn. constructor. destruct m; try discriminate. auto. - inversion H. cbn. constructor. - + apply IHe1. admit. - + apply IHe2. admit. + + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption. + + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption. - inversion H. cbn. constructor. - + apply IHe1. admit. - + apply IHe2. admit. + + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption. + + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption. - inversion H. cbn. constructor. - + apply IHe1. admit. - + apply IHe2. admit. + + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption. + + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption. - inversion H. cbn. constructor; auto. - + apply IHe1. admit. - + apply IHe2. admit. -Admitted. + + apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption. + + apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption. +Qed. Lemma e2_to_smt : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)). Proof. reflexivity. Qed. +(* Lemma refute_bound E : fVars_P_sound (usedVars e2) E thePrecondition_fnc1 -> ~ eval_smt_logic E query @@ -93,11 +94,30 @@ Proof. - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac. eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1. Qed. +*) -Theorem RangeBound_e2_sound E v : +Lemma refute_bound E : fVars_P_sound (usedVars e2) E thePrecondition_fnc1 -> ~ eval_smt_logic E query - -> eval_expr E (fun _ => Some REAL) (toREval (toRExp e2)) v REAL + -> ~ eval_smt_logic E (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))). +Proof. + intros P unsatQ B. + apply unsatQ. cbn. repeat split. + - exact B. + - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac. + exists v1. eexists. repeat split. 1-2: now constructor. apply H1. + - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac. + eexists. exists v1. repeat split. 1-2: now constructor. apply H1. + - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac. + eexists. exists v1. repeat split. 1-2: now constructor. apply H1. + - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac. + exists v1. eexists. repeat split. 1-2: now constructor. apply H1. +Qed. + +Theorem RangeBound_e2_sound E Gamma v : + fVars_P_sound (usedVars e2) E thePrecondition_fnc1 + -> ~ eval_smt_logic E query + -> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL -> v <= Q2R ((8201)#(2048)). Proof. intros Psound unsatQ e2v. @@ -105,7 +125,5 @@ Proof. apply eval_expr_smt in e2v. apply Rnot_lt_le. intros B. eapply refute_bound. 1-2: eassumption. - eapply LessQ_eval. 3: exact B. constructor. assumption. + eexists. exists v. repeat split. constructor. exact e2v. exact B. Qed. - -Print Assumptions RangeBound_e2_sound. -- GitLab