Commit 4eff33b2 authored by Heiko Becker's avatar Heiko Becker

Add missing invariant on inversion to Error Analysis

parent bcf202bf
......@@ -6,7 +6,8 @@ From Flover
Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
(match e with
| Unop u e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Unop Inv e => False
| Unop Neg e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Downcast m e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Binop b e1 e2 =>
validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
......
......@@ -3122,7 +3122,8 @@ Proof.
specialize (IHe Hchecked).
specialize Hsubexpr as (Hsubexpr & Hin).
unfold validErrorBounds in IHe.
split; auto.
split.
{ admit. (* FIXME! Invariant from checker *) }
intros * Heval__R Hcert.
specialize Hchecked as (Hex & Hall); eauto.
intuition.
......
......@@ -54,7 +54,9 @@ Proof.
intuition.
}
clear IHe'.
split; auto.
split.
{ destruct u; cbn in *; Flover_compute; try congruence. auto. }
auto.
intros nR (elo, ehi) err eval_real A_eq.
simpl in *.
rewrite A_eq in valid_error.
......@@ -346,7 +348,6 @@ Proof.
* cbn; instantiate (1:=dVars); Flover_compute.
rewrite L, L0; auto.
* eapply toRExpMap_find_map; eauto.
- inversion ssa_f; subst.
assert (NatSet.Subset (freeVars e1 -- dVars) fVars) as valid_varset.
{ set_tac.
......
......@@ -777,7 +777,7 @@ Proof.
split; [ auto | ].
rewrite B2R_Bopp. congruence.
- (* No Inv allowed *)
admit.
simpl in *. destruct valid_roundoffs; contradiction.
- repeat (match goal with
|H: _ /\ _ |- _ => destruct H
end).
......
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