Commit 8a65a53f authored by Joachim Bard's avatar Joachim Bard

handling FMA and donwcast properly

parent 65eea069
......@@ -134,14 +134,17 @@ Proof.
Qed.
Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
match e, e' with
| ConstQ r, Expressions.Const _ r' => Qeq_bool r r'
| VarQ x, Var _ x' => beq_nat x x'
| UMinusQ e, Unop Neg e' => smt_expr_eq e e'
| PlusQ e1 e2, Binop Plus e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| MinusQ e1 e2, Binop Sub e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| TimesQ e1 e2, Binop Mult e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| DivQ e1 e2, Binop Div e1' e2' => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
match e', e with
| Expressions.Const _ r', ConstQ r => Qeq_bool r r'
| Var _ x', VarQ x => beq_nat x x'
| Unop Neg e', UMinusQ e => smt_expr_eq e e'
| Binop Plus e1' e2', PlusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Binop Sub e1' e2', MinusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Binop Mult e1' e2', TimesQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Binop Div e1' e2', DivQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
| Fma e1' e2' e3', PlusQ e1 (TimesQ e2 e3) =>
smt_expr_eq e1 e1' && smt_expr_eq e2 e2' && smt_expr_eq e3 e3'
| Downcast _ e', _ => smt_expr_eq e e'
| _, _ => false
end.
......@@ -150,30 +153,44 @@ Proof.
induction e; cbn; auto using Qeq_bool_refl, beq_nat_refl; intuition.
Qed.
Lemma eval_smt_expr_complete e e' :
smt_expr_eq e e' = true -> toREval (toRExp e') = toRExp (SMTArith2Expr e).
Lemma eval_smt_expr_complete E Gamma v e e' :
smt_expr_eq e e' = true ->
eval_expr E (toRTMap Gamma) DeltaMapR (toREval (toRExp e')) v REAL ->
eval_expr E (toRTMap Gamma) DeltaMapR (toRExp (SMTArith2Expr e)) v REAL.
Proof.
induction e in e' |- *; destruct e'; cbn; try discriminate.
- intros H. apply Qeq_bool_eq in H. apply Qeq_eqR in H. now rewrite H.
- intros H. apply beq_nat_true in H. now rewrite H.
- destruct u; [intuition | discriminate].
now rewrite (IHe e').
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
- destruct b; try discriminate.
intros H. apply andb_prop in H as [H1 H2].
rewrite <- (IHe1 e'1); auto.
now rewrite <- (IHe2 e'2).
induction e' in e, v |- *.
- destruct e; try discriminate. intros H. apply beq_nat_true in H. now rewrite H.
- destruct e; try discriminate. intros H. apply Qeq_bool_eq in H.
apply Qeq_eqR in H. cbn. now rewrite H.
- destruct e, u; try discriminate.
intros Heq H.
inversion H; subst.
econstructor; eauto.
destruct m; try discriminate.
eapply IHe'; auto.
- intros Heq H.
inversion H; subst.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
destruct e, b; cbn; try discriminate; andb_to_prop Heq.
all: eapply (Binop_dist' (v1:=v1) (v2:=v2)); eauto.
- destruct e; try discriminate.
destruct e2; try discriminate.
intros Heq H. andb_to_prop Heq.
inversion H; subst.
assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m2 = REAL) by (eapply toRTMap_eval_REAL; eauto).
assert (m3 = REAL) by (eapply toRTMap_eval_REAL; eauto).
subst.
eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v1) (v2:= v2 * v3)); eauto.
2: discriminate.
eapply (Binop_dist' (m1:=REAL) (m2:=REAL) (v1:=v2) (v2:=v3)); eauto.
discriminate.
- cbn. intros Heq H.
inversion H; subst.
destruct m1; try discriminate.
now apply IHe'.
Qed.
Lemma eval_smt_expr E e v :
......
......@@ -57,7 +57,7 @@ Proof.
andb_to_prop Hchk.
rewrite <- Q2R_max. apply Rmax_lub; auto.
eapply RangeBound_low_sound; eauto.
erewrite eval_smt_expr_complete in H; eauto.
eapply eval_smt_expr_complete in H; eauto.
rewrite SMTArith2Expr_exact.
exact H.
Qed.
......@@ -84,7 +84,7 @@ Proof.
andb_to_prop Hchk.
rewrite <- Q2R_min. apply Rmin_glb; auto.
eapply RangeBound_high_sound; eauto.
erewrite eval_smt_expr_complete in H; eauto.
eapply eval_smt_expr_complete in H; eauto.
rewrite SMTArith2Expr_exact.
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