Commit eef0aa07 authored by Joachim Bard's avatar Joachim Bard

moving general results to SMTArith2.v

parent 4d3a9f47
......@@ -5,6 +5,7 @@
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import Flover.Expressions.
Require Import Flover.Infra.ExpressionAbbrevs.
Require Import Flover.ExpressionSemantics.
Open Scope R.
......@@ -39,6 +40,8 @@ Inductive SMTLogic :=
| AndQ (q1 q2: SMTLogic) : SMTLogic
| OrQ (q1 q2: SMTLogic) : SMTLogic.
Definition FalseQ := NotQ TrueQ.
(* TODO: broken (div by 0); remove it *)
Fixpoint evalArith (f: nat -> R) (e: SMTArith) : R :=
match e with
......@@ -88,14 +91,63 @@ Fixpoint eval_smt_logic (E: env) (q: SMTLogic) : Prop :=
Lemma andq_assoc E q1 q2 q3 :
eval_smt_logic E (AndQ q1 (AndQ q2 q3)) <-> eval_smt_logic E (AndQ (AndQ q1 q2) q3).
Proof.
cbn. tauto.
Qed.
Proof. cbn. tauto. Qed.
Lemma andq_comm E q1 q2 :
eval_smt_logic E (AndQ q1 q2) <-> eval_smt_logic E (AndQ q2 q1).
Proof. cbn. tauto. Qed.
Lemma not_eval_falseq E : ~ eval_smt_logic E FalseQ.
Proof. auto. Qed.
Fixpoint SMTArith2Expr (e: SMTArith) : expr Q :=
match e with
| ConstQ r => Expressions.Const REAL r
| VarQ x => Var Q x
| UMinusQ e0 => Unop Neg (SMTArith2Expr e0)
| PlusQ e1 e2 => Binop Plus (SMTArith2Expr e1) (SMTArith2Expr e2)
| MinusQ e1 e2 => Binop Sub (SMTArith2Expr e1) (SMTArith2Expr e2)
| TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Lemma eval_smt_expr E e v :
eval_smt E e v -> eval_expr E (fun _ => Some REAL) (toRExp (SMTArith2Expr e)) v REAL.
Proof with try (right; apply Rabs_R0).
induction 1.
- now constructor.
- rewrite <- (delta_0_deterministic _ REAL 0)... constructor...
- rewrite <- (delta_0_deterministic _ REAL 0)... apply (Unop_neg (m:= REAL)); auto.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
Qed.
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.
cbn. tauto.
induction e in v |- *; cbn; intros H.
- inversion H. cbn. constructor.
- inversion H. cbn. constructor; auto.
- inversion H. cbn. constructor. destruct m; try discriminate. auto.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor; auto.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
Qed.
Fixpoint varsSMT (e: SMTArith) :=
......@@ -136,17 +188,6 @@ Inductive eval_smt_logic (E: env) : SMTLogic -> Prop :=
| 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
| ConstQ r => Expressions.Const REAL r
| VarQ x => Var Q x
| UMinusQ e0 => Unop Neg (SMTArith2Expr e0)
| PlusQ e1 e2 => Binop Plus (SMTArith2Expr e1) (SMTArith2Expr e2)
| MinusQ e1 e2 => Binop Sub (SMTArith2Expr e1) (SMTArith2Expr e2)
| TimesQ e1 e2 => Binop Mult (SMTArith2Expr e1) (SMTArith2Expr e2)
| DivQ e1 e2 => Binop Div (SMTArith2Expr e1) (SMTArith2Expr e2)
end.
Definition eval_precond E (P: FloverMap.t intv) :=
forall x lo hi, (List.In (Var Q x, (lo, hi)) (FloverMap.elements P))
-> exists vR: R, E x = Some vR /\ Q2R lo <= vR <= Q2R hi.
......@@ -325,3 +366,42 @@ Proof with try discriminate.
+ apply andb_prop in chk. destruct chk as [chk chk0].
apply (IHl _ chk0); tauto.
Qed.
Lemma precond_bound_correct E P preQ bound :
eval_precond E P
-> checkPre P preQ = true
-> eval_smt_logic E bound
-> eval_smt_logic E (AndQ preQ bound).
Proof.
intros H1 H2 H3.
split; auto.
eapply checkPre_pre_smt; eauto.
Qed.
Lemma RangeBound_low_sound E P preQ e r Gamma v :
eval_precond E P
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (LessQ e (ConstQ r)))
-> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> Q2R r <= v.
Proof.
intros H1 H2 H3 H4.
apply eval_expr_smt in H4.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
Lemma RangeBound_high_sound E P preQ e r Gamma v :
eval_precond E P
-> checkPre P preQ = true
-> ~ eval_smt_logic E (AndQ preQ (LessQ (ConstQ r) e))
-> eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> v <= Q2R r.
Proof.
intros H1 H2 H3 H4.
apply eval_expr_smt in H4.
apply Rnot_lt_le. intros B.
apply H3. eapply precond_bound_correct; eauto.
do 2 eexists. repeat split; first [eassumption | constructor].
Qed.
\ No newline at end of file
......@@ -57,45 +57,6 @@ Proof.
cbn. tauto.
Qed.
Lemma eval_smt_expr E e v :
eval_smt E e v -> eval_expr E (fun _ => Some REAL) (toRExp (SMTArith2Expr e)) v REAL.
Proof with try (right; apply Rabs_R0).
induction 1.
- now constructor.
- rewrite <- (delta_0_deterministic _ REAL 0)... constructor...
- rewrite <- (delta_0_deterministic _ REAL 0)... apply (Unop_neg (m:= REAL)); auto.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
Qed.
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.
- inversion H. cbn. constructor.
- inversion H. cbn. constructor; auto.
- inversion H. cbn. constructor. destruct m; try discriminate. auto.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor; auto.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
Qed.
Definition bound_expr :=
match bound with
| LessQ e (ConstQ r) => e
......@@ -108,6 +69,7 @@ Proof.
reflexivity.
Qed.
(*
Lemma precond_bound_correct E :
eval_precond E thePrecondition_fnc1
-> eval_smt_logic E bound
......@@ -120,6 +82,7 @@ Proof.
reflexivity.
- exact B.
Qed.
*)
Theorem RangeBound_e2_sound E Gamma v :
eval_precond E thePrecondition_fnc1
......@@ -127,10 +90,10 @@ Theorem RangeBound_e2_sound E Gamma v :
-> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
-> v <= Q2R ((8201)#(2048)).
Proof.
intros P nQ e2v.
rewrite e2_to_smt in e2v.
apply eval_expr_smt in e2v.
apply Rnot_lt_le. intros B.
apply nQ. apply precond_bound_correct. assumption.
do 2 eexists. repeat split; first [eassumption | constructor].
intros H1 H2 H3.
rewrite e2_to_smt in H3.
eapply (RangeBound_high_sound (preQ:= prec) H1 _ _ H3).
Unshelve.
- reflexivity.
- intros H. apply H2. apply prec_bound_correct. exact H.
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