diff options
| -rw-r--r-- | cfrontend/Csem.v | 7 | ||||
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 12 | ||||
| -rw-r--r-- | lib/Floats.v | 3 |
3 files changed, 8 insertions, 14 deletions
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 6e35c2f..5f8bbf1 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -40,8 +40,9 @@ Inductive is_false: val -> type -> Prop := is_false (Vint Int.zero) (Tint sz sg) | is_false_pointer: forall t, is_false (Vint Int.zero) (Tpointer t) - | is_false_float: forall sz, - is_false (Vfloat Float.zero) (Tfloat sz). + | is_false_float: forall sz f, + Float.cmp Ceq f Float.zero = true -> + is_false (Vfloat f) (Tfloat sz). Inductive is_true: val -> type -> Prop := | is_true_int_int: forall n sz sg, @@ -55,7 +56,7 @@ Inductive is_true: val -> type -> Prop := | is_true_pointer_pointer: forall b ofs t, is_true (Vptr b ofs) (Tpointer t) | is_true_float: forall f sz, - f <> Float.zero -> + Float.cmp Ceq f Float.zero = false -> is_true (Vfloat f) (Tfloat sz). Inductive bool_of_val : val -> type -> val -> Prop := diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 3f0f4b3..e58570b 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -78,10 +78,8 @@ Proof. try (exists v; intuition; inversion VTRUE; simpl; auto; fail). exists Vtrue; split. eapply eval_Ebinop; eauto with cshm. - inversion VTRUE; simpl. - replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)). - rewrite Float.eq_zero_false. reflexivity. auto. - rewrite Float.cmp_ne_eq. auto. + inversion VTRUE; simpl. + rewrite Float.cmp_ne_eq. rewrite H1. auto. apply Vtrue_is_true. Qed. @@ -98,10 +96,8 @@ Proof. try (exists v; intuition; inversion VFALSE; simpl; auto; fail). exists Vfalse; split. eapply eval_Ebinop; eauto with cshm. - inversion VFALSE; simpl. - replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)). - rewrite Float.eq_zero_true. reflexivity. - rewrite Float.cmp_ne_eq. auto. + inversion VFALSE; simpl. + rewrite Float.cmp_ne_eq. rewrite H1. auto. apply Vfalse_is_false. Qed. diff --git a/lib/Floats.v b/lib/Floats.v index 50298f7..5c20cdd 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -70,9 +70,6 @@ Axiom cmp_le_lt_eq: Axiom cmp_ge_gt_eq: forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2. -Axiom eq_zero_true: cmp Ceq zero zero = true. -Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false. - Axiom bits_of_double_of_bits: forall n, bits_of_double (double_of_bits n) = n. Axiom double_of_bits_of_double: |