Skip to content

GitLab

Commit 96bc2e7e authored by Heiko Becker's avatar Heiko Becker
Browse files
Options

minor style changes in Coq dev and finish porting in HOL4

parent 858e91ae
Show whitespace changes
Inline Side-by-side
Showing with 495 additions and 459 deletions
coq/Environments.v
View file @ 96bc2e7e
......@@ -26,7 +26,7 @@ Inductive approxEnv : env -> (expr R -> option mType) -> analysisResult -> NatSe
(Rabs (v1 - v2) <= computeErrorR v1 m)%R ->
NatSet.mem x (NatSet.union fVars dVars) = false ->
approxEnv (updEnv x v1 E1)
(updDefVars (Var R x) m Gamma) A (NatSet.add x fVars) dVars
Gamma A (NatSet.add x fVars) dVars
(updEnv x v2 E2)
|approxUpdBound E1 E2 Gamma A v1 v2 x fVars dVars m iv err:
approxEnv E1 Gamma A fVars dVars E2 ->
......@@ -88,11 +88,7 @@ Section RelationProperties.
destruct x_free as [x_x0 | [x_neq x_free]]; subst.
+ unfold updEnv in *;
rewrite Nat.eqb_refl in *; simpl in *.
unfold updDefVars in x_typed.
cbn in x_typed.
rewrite Nat.compare_refl in x_typed.
inversion x_typed; subst.
inversion E1_def; inversion E2_def; subst; auto.
congruence.
+ unfold updEnv in *; simpl in *.
rewrite <- Nat.eqb_neq in x_neq.
rewrite x_neq in *; simpl in *.
......@@ -109,7 +105,6 @@ Section RelationProperties.
apply H2.
set_tac. }
unfold updEnv in *; rewrite x_x0_neq in *.
unfold updDefVars in x_typed.
cbn in x_typed.
apply Nat.eqb_neq in x_x0_neq.
destruct (x ?= x0)%nat eqn:?.
......
coq/ErrorValidation.v
View file @ 96bc2e7e
......@@ -249,12 +249,11 @@ Proof.
rewrite Rabs_R0. auto using mTypeToR_pos_R.
Qed.
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars exprTypes
Gamma:
Lemma validErrorboundCorrectConstant E1 E2 A m n nR nF e nlo nhi dVars Gamma:
eval_Real E1 Gamma (Const m n) nR ->
eval_Fin E2 Gamma (Const m n) nF m ->
validTypes (Const m n) Gamma ->
validErrorbound (Const m n) exprTypes A dVars = true ->
validErrorbound (Const m n) Gamma A dVars = true ->
(Q2R nlo <= nR <= Q2R nhi)%R ->
FloverMap.find (Const m n) A = Some ((nlo,nhi),e) ->
(Rabs (nR - nF) <= (Q2R e))%R.
......@@ -275,28 +274,6 @@ Proof.
simpl in *; auto.
Qed.
(*
Lemma isFixedPoint_lift m1 m2 e fBits f:
(isFixedPoint m1 -> isFixedPoint m2 -> FloverMap.find e fBits = Some f) ->
isFixedPoint m1 -> isFixedPoint m2 -> toRBMap fBits (toRExp e) = Some f.
Proof.
intros isvalid fixed_m1 fixed_m2.
apply toRBMap_some.
auto.
Qed.
Lemma isFixedPoint_lift3 m1 m2 m3 e fBits f:
(isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
FloverMap.find e fBits = Some f) ->
isFixedPoint m1 -> isFixedPoint m2 -> isFixedPoint m3 ->
toRBMap fBits (toRExp e) = Some f.
Proof.
intros isvalid fixed_m1 fixed_m2 fixed_m3.
apply toRBMap_some.
auto.
Qed.
*)
Lemma validErrorboundCorrectAddition E1 E2 A
(e1:expr Q) (e2:expr Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error)
(alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma:
......@@ -1994,7 +1971,7 @@ Qed.
(**
Soundness theorem for the error bound validator.
Proof is by induction on the exprression e.
Proof is by induction on the expression e.
Each case requires the application of one of the soundness lemmata proven before
**)
Theorem validErrorbound_sound (e:expr Q):
......@@ -2004,7 +1981,6 @@ Theorem validErrorbound_sound (e:expr Q):
NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars ->
eval_Real E1 Gamma e nR ->
validErrorbound e Gamma A dVars = true ->
validTypes e Gamma ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
FloverMap.find e A = Some ((elo,ehi),err) ->
(exists nF m,
......@@ -2014,8 +1990,8 @@ Theorem validErrorbound_sound (e:expr Q):
(Rabs (nR - nF) <= (Q2R err))%R).
Proof.
revert e; induction e;
intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_types
valid_intv A_eq.
intros * typing_ok approxCEnv fVars_subset eval_real valid_error valid_intv
A_eq.
- split.
+ eapply validErrorboundCorrectVariable_eval; eauto.
+ intros * eval_float. eapply validErrorboundCorrectVariable; eauto.
......@@ -2336,7 +2312,6 @@ Proof.
{ exists vF_res; exists m_res; try auto.
econstructor; eauto. }
+ destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto.
+ destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto.
+ destruct valid_intv as [[? ?] ?]; auto.
- inversion eval_real; subst.
unfold updEnv; simpl.
......@@ -2407,28 +2382,9 @@ Proof.
simpl.
rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec.
split; try auto.
(* + eapply swap_Gamma_bstep with (Gamma1 := updDefVars n REAL (toRTMap Gamma)); *)
(* eauto using Rmap_updVars_comm. *)
(* + apply validRangesCmd_swap with (Gamma1 := updDefVars n REAL Gamma). *)
(* * intros x. *)
(* unfold toRTMap, updDefVars. *)
(* destruct (x =? n) eqn:?; auto. *)
(* * destruct valid_intv as [[? valid_cont] ?]. *)
(* apply valid_cont. *)
(* apply swap_Gamma_eval_expr with (Gamma1 := toRTMap Gamma); try auto. *)
+ destruct valid_intv as [[? ?] ?]; auto.
+ destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto.
+ destruct valid_types as [[? [? [? [? [? ?]]]]] ?]; auto.
+ destruct valid_intv as [[? ?] ?]; auto.
(* + intros v1 v1_mem; set_tac. *)
(* unfold updDefVars. *)
(* case_eq (v1 =? n); intros case_v1; try rewrite case_v1 in *; try eauto. *)
(* apply types_defined. *)
(* rewrite NatSet.union_spec. *)
(* destruct v1_mem as [v_fVar | v_dVar]; try auto. *)
(* rewrite NatSet.add_spec in v_dVar. destruct v_dVar; try auto. *)
(* subst; rewrite Nat.eqb_refl in case_v1; congruence. *)
(* + destruct valid_intv as [[? ?] ?]; auto. *)
- inversion eval_real; subst.
inversion eval_float; subst.
unfold updEnv; simpl.
......
coq/ExpressionSemantics.v
View file @ 96bc2e7e
......@@ -380,7 +380,7 @@ Proof.
Qed.
Lemma swap_Gamma_eval_expr e E vR m Gamma1 Gamma2:
(forall n, Gamma1 n = Gamma2 n) ->
(forall e, Gamma1 e = Gamma2 e) ->
eval_expr E Gamma1 e vR m ->
eval_expr E Gamma2 e vR m.
Proof.
......
coq/Infra/ExpressionAbbrevs.v
View file @ 96bc2e7e
......@@ -219,6 +219,32 @@ Proof.
congruence.
Qed.
Lemma map_find_add e1 e2 m map1:
FloverMap.find e1 (FloverMap.add e2 m map1) =
match Q_orderedExps.compare e2 e1 with
|Eq => Some m
|_ => FloverMap.find (elt:=mType) e1 map1
end.
Proof.
rewrite FloverMapFacts.P.F.add_o.
unfold FloverMapFacts.P.F.eq_dec.
unfold Q_orderedExps.compare.
destruct (Q_orderedExps.exprCompare e2 e1) eqn:?; congruence.
Qed.
Lemma map_mem_add e1 e2 m map1:
FloverMap.mem e1 (FloverMap.add e2 m map1) =
match Q_orderedExps.compare e2 e1 with
|Eq => true
| _ => FloverMap.mem (elt:=mType) e1 map1
end.
Proof.
rewrite FloverMapFacts.P.F.mem_find_b.
rewrite map_find_add.
destruct (Q_orderedExps.compare e2 e1) eqn:?; try auto;
rewrite FloverMapFacts.P.F.mem_find_b; auto.
Qed.
Definition toRExpMap (tMap:FloverMap.t mType) : expr R -> option mType :=
let elements := FloverMap.elements (elt:=mType) tMap in
fun (e:expr R) =>
......@@ -378,6 +404,66 @@ Proof.
rewrite Pos.eqb_refl, N.eqb_refl in e5; simpl in *; congruence.
Qed.
Lemma no_cycle_unop e:
forall u, Q_orderedExps.exprCompare e (Unop u e) <> Eq.
induction e; intros *; cbn in *; try congruence.
destruct (unopEq u u0) eqn:?; try auto.
destruct (unopEq u Neg); congruence.
Qed.
Lemma no_cycle_cast e:
forall m, Q_orderedExps.exprCompare e (Downcast m e) <> Eq.
induction e; intros *; cbn in *; try congruence.
destruct (mTypeEq m m0) eqn:?; try auto.
destruct m; destruct m0; type_conv; try congruence;
cbn; hnf; intros; try congruence.
destruct (w ?= w0)%positive eqn:?; try congruence.
apply Pos.compare_eq in Heqc.
apply N.compare_eq in H; subst; congruence.
Qed.
Lemma no_cycle_binop_left e1:
forall b e2, Q_orderedExps.exprCompare e1 (Binop b e1 e2) <> Eq.
induction e1; intros *; cbn in *; try congruence.
pose (bOp := b);
destruct b; destruct b0;
try (hnf; intros; congruence);
destruct (Q_orderedExps.exprCompare e1_1 (Binop bOp e1_1 e1_2)) eqn:case_comp;
subst bOp; rewrite case_comp in *;
congruence.
Qed.
Lemma no_cycle_binop_right e2:
forall b e1, Q_orderedExps.exprCompare e2 (Binop b e1 e2) <> Eq.
induction e2; intros *; cbn in *; try congruence.
pose (bOp := b);
destruct b; destruct b0;
try (hnf; intros; congruence);
destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; congruence.
Qed.
Lemma no_cycle_fma_left e1:
forall e2 e3, Q_orderedExps.exprCompare e1 (Fma e1 e2 e3) <> Eq.
Proof.
induction e1; intros *; cbn in *; try congruence;
destruct (Q_orderedExps.exprCompare e1_1 (Fma e1_1 e1_2 e1_3)) eqn:?; congruence.
Qed.
Lemma no_cycle_fma_center e2:
forall e1 e3, Q_orderedExps.exprCompare e2 (Fma e1 e2 e3) <> Eq.
Proof.
induction e2; intros *; cbn in *; try congruence.
destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; try congruence.
destruct (Q_orderedExps.exprCompare e2_2 (Fma e2_1 e2_2 e2_3)) eqn:?; congruence.
Qed.
Lemma no_cycle_fma_right e3:
forall e1 e2, Q_orderedExps.exprCompare e3 (Fma e1 e2 e3) <> Eq.
Proof.
induction e3; intros *; cbn in *; try congruence.
destruct (Q_orderedExps.exprCompare e3_1 e1) eqn:?; try congruence.
destruct (Q_orderedExps.exprCompare e3_2 e2) eqn:?; try congruence.
Qed.
(*
Lemma toRExpMap_toRTMap e Gamma m:
toRExpMap Gamma (toRExp e) = Some m ->
......
coq/Infra/MachineType.v
View file @ 96bc2e7e
......@@ -57,11 +57,6 @@ Definition mTypeToR (m:mType) :R :=
| M32 => 1/ 2^24
| M64 => 1/ 2^53
| F w f => 1/ 2^(N.to_nat f)
(*
(* the epsilons below match what is used internally in Daisy,
although these value do not match the IEEE standard *)
| M128 => (Qpower (2#1) (Zneg 105))
| M256 => (Qpower (2#1) (Zneg 211)) *)
end.
Definition mTypeToQ (m:mType) :Q :=
......@@ -71,11 +66,6 @@ Definition mTypeToQ (m:mType) :Q :=
| M32 => (Qpower (2#1) (Zneg 24))
| M64 => (Qpower (2#1) (Zneg 53))
| F w f => Qpower (2#1) (- Z.of_N f)
(*
(* the epsilons below match what is used internally in Daisy,
although these value do not match the IEEE standard *)
| M128 => (Qpower (2#1) (Zneg 105))
| M256 => (Qpower (2#1) (Zneg 211)) *)
end.
Definition computeErrorR v m :R :=
......@@ -201,8 +191,6 @@ Definition mTypeEq (m1:mType) (m2:mType) :=
| M32, M32 => true
| M64, M64 => true
| F w1 f1, F w2 f2 => (w1 =? w2)%positive && (f1 =? f2)%N
(* | M128, M128 => true *)
(* | M256, M256 => true *)
| _, _ => false
end.
......@@ -273,8 +261,10 @@ Definition isMorePrecise (m1:mType) (m2:mType) :=
| _, _ => Qle_bool (mTypeToQ m1) (mTypeToQ m2)
end.
(* More efficient version for performance, unfortunately we cannot do better
for fixed-points *)
(**
More efficient version for performance, unfortunately we cannot do better
for fixed-points
**)
Definition morePrecise (m1:mType) (m2:mType) :=
match m1, m2 with
| REAL, _ => true
......@@ -302,10 +292,7 @@ Lemma morePrecise_trans m1 m2 m3:
Proof.
destruct m1; destruct m2; destruct m3; simpl; auto;
intros le1 le2; try congruence.
(* andb_to_prop le1; andb_to_prop le2. *)
apply Pos.leb_le in le1; apply Pos.leb_le in le2.
(* apply Pos.leb_le in L0; apply Pos.leb_le in R0. *)
(* split_bool; *)
apply Pos.leb_le;
eapply Pos.le_trans; eauto.
Qed.
......
coq/RealRangeArith.v
View file @ 96bc2e7e
......@@ -19,10 +19,6 @@ Definition fVars_P_sound (fVars:NatSet.t) (E:env) (P:precond) :Prop :=
exists vR, E v = Some vR /\
(Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R.
Definition vars_typed (S:NatSet.t) (Gamma: nat -> option mType) :=
forall v, NatSet.In v S ->
exists m :mType, Gamma v = Some m.
Ltac kill_trivial_exists :=
match goal with
| [ |- exists iv err v, Some (?i,?e) = Some (iv, err) /\ _ ] => exists i, e
......
coq/TypeValidator.v
View file @ 96bc2e7e
......@@ -29,13 +29,17 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType) :Prop :=
| Var _ x => True
| Const m v => m = mG
| Unop u e1 =>
validTypes e1 Gamma /\ exists me, FloverMap.find e1 Gamma = Some me /\ isCompat me mG = true
validTypes e1 Gamma /\
exists me, FloverMap.find e1 Gamma = Some me /\ isCompat me mG = true
| Binop b e1 e2 =>
validTypes e1 Gamma /\ validTypes e2 Gamma /\
exists m1 m2, FloverMap.find e1 Gamma = Some m1 /\ FloverMap.find e2 Gamma = Some m2 /\
validTypes e1 Gamma /\
validTypes e2 Gamma /\
exists m1 m2, FloverMap.find e1 Gamma = Some m1 /\
FloverMap.find e2 Gamma = Some m2 /\
isJoin m1 m2 mG = true
| Fma e1 e2 e3 =>
validTypes e1 Gamma /\ validTypes e2 Gamma /\
validTypes e1 Gamma /\
validTypes e2 Gamma /\
validTypes e3 Gamma /\
exists m1 m2 m3,
FloverMap.find e1 Gamma = Some m1 /\ FloverMap.find e2 Gamma = Some m2 /\
......@@ -47,7 +51,8 @@ Fixpoint validTypes e (Gamma:FloverMap.t mType) :Prop :=
(FloverMap.find e1 Gamma = Some m1 /\ isMorePrecise m1 mG = true)
end /\
(forall E Gamma2 v m,
(forall e m, FloverMap.find e Gamma = Some m -> FloverMap.find e Gamma2 = Some m) ->
(forall e m, FloverMap.find e Gamma = Some m ->
FloverMap.find e Gamma2 = Some m) ->
eval_expr E (toRExpMap Gamma2) (toRExp e) v m ->
m = mG).
......@@ -123,12 +128,6 @@ Ltac validTypes_simp :=
Open Scope string_scope.
Definition getTypeMap (r:result (FloverMap.t mType)) :FloverMap.t mType:=
match r with
|Succes m => m
| _ => FloverMap.empty mType
end.
Definition isMonotone mOldO mNew :=
match mOldO with
|None => true
......@@ -165,21 +164,21 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
| Unop u e1 =>
rlet akk_new := getValidMap Gamma e1 akk in
match FloverMap.find e1 akk_new with
| None => Fail _ "Cannot Typecheck unary operator"
| Some m_e1 =>
if (isFixedPointB m_e1)
then
match mOldO with
|None => Fail _ "Undefined fixed-point type"
|Some mFix =>
if (isCompat m_e1 mFix)
then addMono e mFix akk_new
else Fail _ "Incompatible type assignment"
|None => Fail _ "Undefined fixed-point type"
end
else
if (isMonotone mOldO m_e1)
then addMono e m_e1 akk_new
else Fail _ "Wrong type annotation for unary constant"
| None => Fail _ "Cannot Typecheck unary operator"
end
| Binop b e1 e2 =>
rlet akk1_map := getValidMap Gamma e1 akk in
......@@ -199,11 +198,11 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
end
else
match (join_fl t1 t2) with
| None => Fail _ "Could not compute join for arguments"
| Some m =>
if (isMonotone mOldO m)
then addMono e m akk2_map
else Fail _ "Wrong type annotation for binary operator"
| None => Fail _ "Could not compute join for arguments"
end
| _, _ => Fail _ "Could not compute type for arguments"
end
......@@ -239,20 +238,20 @@ Fixpoint getValidMap (Gamma:FloverMap.t mType) (e:expr Q)
rlet akk_new := getValidMap Gamma e1 akk in
let m1 := FloverMap.find e1 akk_new in
match m1 with
| None => Fail _ "Could not find cast argument type"
| Some t1 =>
if (isFixedPointB t1)
then
match mOldO with
|None => Fail _ "Could not find fixed-point type for cast"
|Some mFix => if (mTypeEq m mFix && morePrecise t1 mFix)
then addMono e mFix akk_new
else Fail _ "Incorrect fixed-point type"
|None => Fail _ "Could not find fixed-point type for cast"
end
else
if (morePrecise t1 m && isMonotone mOldO m)
then addMono e m akk_new
else Fail _ "Cannot cast down to lower precision"
| None => Fail _ "Could not find case argument type"
end
end.
......@@ -275,93 +274,6 @@ Proof.
eauto using tMap_def.
Qed.
Lemma no_cycle_unop e:
forall u, Q_orderedExps.exprCompare e (Unop u e) <> Eq.
induction e; intros *; cbn in *; try congruence.
destruct (unopEq u u0) eqn:?; try auto.
destruct (unopEq u Neg); congruence.
Qed.
Lemma no_cycle_cast e:
forall m, Q_orderedExps.exprCompare e (Downcast m e) <> Eq.
induction e; intros *; cbn in *; try congruence.
destruct (mTypeEq m m0) eqn:?; try auto.
destruct m; destruct m0; type_conv; try congruence;
cbn; hnf; intros; try congruence.
destruct (w ?= w0)%positive eqn:?; try congruence.
apply Pos.compare_eq in Heqc.
apply N.compare_eq in H; subst; congruence.
Qed.
Lemma no_cycle_binop_left e1:
forall b e2, Q_orderedExps.exprCompare e1 (Binop b e1 e2) <> Eq.
induction e1; intros *; cbn in *; try congruence.
pose (bOp := b);
destruct b; destruct b0;
try (hnf; intros; congruence);
destruct (Q_orderedExps.exprCompare e1_1 (Binop bOp e1_1 e1_2)) eqn:case_comp;
subst bOp; rewrite case_comp in *;
congruence.
Qed.
Lemma no_cycle_binop_right e2:
forall b e1, Q_orderedExps.exprCompare e2 (Binop b e1 e2) <> Eq.
induction e2; intros *; cbn in *; try congruence.
pose (bOp := b);
destruct b; destruct b0;
try (hnf; intros; congruence);
destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; congruence.
Qed.
Lemma no_cycle_fma_left e1:
forall e2 e3, Q_orderedExps.exprCompare e1 (Fma e1 e2 e3) <> Eq.
Proof.
induction e1; intros *; cbn in *; try congruence;
destruct (Q_orderedExps.exprCompare e1_1 (Fma e1_1 e1_2 e1_3)) eqn:?; congruence.
Qed.
Lemma no_cycle_fma_center e2:
forall e1 e3, Q_orderedExps.exprCompare e2 (Fma e1 e2 e3) <> Eq.
Proof.
induction e2; intros *; cbn in *; try congruence.
destruct (Q_orderedExps.exprCompare e2_1 e1) eqn:?; try congruence.
destruct (Q_orderedExps.exprCompare e2_2 (Fma e2_1 e2_2 e2_3)) eqn:?; congruence.
Qed.
Lemma no_cycle_fma_right e3:
forall e1 e2, Q_orderedExps.exprCompare e3 (Fma e1 e2 e3) <> Eq.
Proof.
induction e3; intros *; cbn in *; try congruence.
destruct (Q_orderedExps.exprCompare e3_1 e1) eqn:?; try congruence.
destruct (Q_orderedExps.exprCompare e3_2 e2) eqn:?; try congruence.
Qed.
Lemma map_find_add e1 e2 m map1:
FloverMap.find e1 (FloverMap.add e2 m map1) =
match Q_orderedExps.compare e2 e1 with
|Eq => Some m
|_ => FloverMap.find (elt:=mType) e1 map1
end.
Proof.
rewrite FloverMapFacts.P.F.add_o.
unfold FloverMapFacts.P.F.eq_dec.
unfold Q_orderedExps.compare.
destruct (Q_orderedExps.exprCompare e2 e1) eqn:?; congruence.
Qed.
Lemma map_mem_add e1 e2 m map1:
FloverMap.mem e1 (FloverMap.add e2 m map1) =
match Q_orderedExps.compare e2 e1 with
|Eq => true
| _ => FloverMap.mem (elt:=mType) e1 map1
end.
Proof.
rewrite FloverMapFacts.P.F.mem_find_b.
rewrite map_find_add.
destruct (Q_orderedExps.compare e2 e1) eqn:?; try auto;
rewrite FloverMapFacts.P.F.mem_find_b; auto.
Qed.
Ltac by_monotonicity find_akk mem_case:=
rewrite map_find_add;
match goal with
......@@ -670,13 +582,6 @@ Proof.
+ Flover_compute.
destruct (isCompat m m0) eqn:?; try congruence.
unfold addMono in *; Flover_compute.
(* { destruct (mTypeEq m0 m1) eqn:?; try congruence. *)
(* inversion validMap_succ; subst. *)
(* exists m1; repeat split; try auto. *)
(* intros * map_mono eval_unop. *)
(* specialize (map_mono (Unop u e) m1 Heqo1). *)
(* eapply toRExpMap_some in map_mono; simpl; eauto. *)
(* inversion eval_unop; subst; congruence. } *)
inversion validMap_succ; subst.
assert (FloverMap.mem (Unop u e) t = false)
by (rewrite FloverMapFacts.P.F.mem_find_b; rewrite Heqo1; eauto).
......
hol4/IEEE_connectionScript.sml
View file @ 96bc2e7e
......@@ -462,7 +462,7 @@ val is64BitEval_def = Define `
(is64BitEval (Unop _ e) = is64BitEval e) /\
(is64BitEval (Binop b e1 e2) = (is64BitEval e1 /\ is64BitEval e2)) /\
(is64BitEval (Fma e1 e2 e3) = (is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3)) /\
(is64BitEval (Downcast m e) = is64BitEval e) /\
(is64BitEval (Downcast m e) = ((m = M64) /\ is64BitEval e)) /\
(is64BitEval ((Var v):real expr) = T)`;
val is64BitBstep_def = Define `
......@@ -493,7 +493,7 @@ val typing_cmd_64bit = store_thm (
\\ res_tac);
val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
``!(e:word64 expr) E1 E2 E2_real Gamma vR A P fVars dVars.
``!(e:word64 expr) E1 E2 E2_real Gamma vR A fVars dVars.
(!x. (toREnv E2) x = E2_real x) /\
validTypes (toRExp e) Gamma /\
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2_real /\
......@@ -866,6 +866,35 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ fs[GSYM float_is_zero_to_real, float_is_zero_def,
mTypeToR_pos, perturb_def])
(* Division *)
>- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
\\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))) M64`
by (rw_thm_asm `validFloatValue (_ / _) _` validFloatValue_def
\\ fs[normal_def, denormal_def, evalBinop_def]
>- (`abs (float_to_real (fp64_to_float vF1) /
float_to_real (fp64_to_float vF2)) <
abs (float_to_real (fp64_to_float vF1) /
float_to_real (fp64_to_float vF2))`
suffices_by (fs[])
\\ irule REAL_LTE_TRANS
\\ asm_exists_tac \\ fs[])
\\ qpat_x_assum `_ = 0` (fn thm => fs[thm])
\\ fs[maxValue_def, maxExponent_def])
\\ Q.ISPECL_THEN [`(fp64_to_float vF1):(52,11) float`,
`(fp64_to_float vF2):(52,11) float`]
impl_subgoal_tac
float_div_relative
>- (rpt conj_tac
\\ fs[validFloatValue_def,
normalTranslatedValue_implies_finiteness,
denormalTranslatedValue_implies_finiteness,
normalValue_implies_normalization,
GSYM float_is_zero_to_real, float_is_finite, evalBinop_def])
\\ fs[dmode_def]
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `e`]
\\ fs[perturb_def, evalBinop_def]
\\ fs[mTypeToR_def])
>- (fs[fp64_div_def, fp64_to_float_float_to_fp64, evalBinop_def]
\\ `normal (evalBinop Div (float_to_real (fp64_to_float vF1))
(float_to_real (fp64_to_float vF2))) M64`
......@@ -978,41 +1007,11 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ rw_asm_star `FloverMapTree_find (Fma _ _ _) Gamma = _`)
\\ rw_thm_asm `domain (usedVars _) DIFF _ SUBSET _` usedVars_def
\\ fs[domain_union, DIFF_DEF, SUBSET_DEF])
\\ fs[]
\\ rename1 `eval_expr_float e1 _ = SOME vF1`
\\ rename1 `eval_expr_float e2 _ = SOME vF2`
\\ rename1 `eval_expr_float e3 _ = SOME vF3`
\\ IMP_RES_TAC validRanges_single
\\ rename1 `FloverMapTree_find (toRExp e3) A = SOME (iv3, err3)`
\\ rename1 `FloverMapTree_find (toRExp e2) A = SOME (iv2, err2)`
\\ rename1 `FloverMapTree_find (toRExp e1) A = SOME (iv1, err1)`
\\ rename1 `eval_expr E1 _ (toREval (toRExp e3)) nR3 REAL`
\\ rename1 `eval_expr E1 _ (toREval (toRExp e2)) nR2 REAL`
\\ rename1 `eval_expr E1 _ (toREval (toRExp e1)) nR1 REAL`
(* Obtain evaluation for E2_real*)