From 3adaf93a90e1dcdc3c38b2c4197e62a843e8ad3e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 26 Mar 2019 17:04:51 +0100 Subject: Update the proofs after rebase --- x86/Asmgenproof1.v | 103 ++++++++++------------------------------------------- 1 file changed, 19 insertions(+), 84 deletions(-) diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index c638cdcf..c994b9eb 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -769,41 +769,25 @@ Transparent Float.cmp Float.ordered. - (* ne *) unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. - (* lt *) - rewrite <- (Float.cmp_swap Clt n2 n1). simpl. unfold Float.ordered. + rewrite <- (Float.cmp_swap FClt n2 n1). simpl. unfold Float.ordered. destruct (Float.compare n2 n1) as [[]|]; reflexivity. - (* le *) - rewrite <- (Float.cmp_swap Cge n1 n2). simpl. + rewrite <- (Float.cmp_swap FCge n1 n2). simpl. destruct (Float.compare n1 n2) as [[]|]; auto. - (* gt *) - unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. - (* ge *) - destruct (Float.cmp Cge n1 n2); auto. + destruct (Float.cmp FCge n1 n2); auto. - (* notlt *) - replace (Float.cmp FCnotlt n1 n2) with (negb (Float.cmp FClt n1 n2)) by (symmetry; apply (Float.cmp_negate FClt)). - rewrite <- (Float.cmp_swap FCge n1 n2). - rewrite <- (Float.cmp_swap FCne n1 n2). - simpl. - rewrite Float.cmp_ne_eq. rewrite Float.cmp_le_lt_eq. - destruct (Float.cmp FClt n1 n2) eqn:LT; simpl. - destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl. - exfalso. eapply Float.cmp_lt_eq_false; eauto. - auto. - destruct (Float.cmp FCeq n1 n2); auto. + rewrite <- (Float.cmp_swap FCnotlt n2 n1). simpl. unfold Float.ordered. + destruct (Float.compare n2 n1) as [[]|]; reflexivity. - (* notle *) - replace (Float.cmp FCnotle n1 n2) with (negb (Float.cmp FCle n1 n2)) by (symmetry; apply (Float.cmp_negate FCle)). - rewrite <- (Float.cmp_swap FCge n1 n2). simpl. - destruct (Float.cmp FCle n1 n2); auto. + rewrite <- (Float.cmp_swap FCnotle n2 n1). simpl. + destruct (Float.compare n2 n1) as [[]|]; reflexivity. - (* notgt *) - replace (Float.cmp FCnotgt n1 n2) with (negb (Float.cmp FCgt n1 n2)) by (symmetry; apply (Float.cmp_negate FCgt)). - rewrite Float.cmp_ne_eq. rewrite Float.cmp_ge_gt_eq. - destruct (Float.cmp FCgt n1 n2) eqn:GT; simpl. - destruct (Float.cmp FCeq n1 n2) eqn:EQ; simpl. - exfalso. eapply Float.cmp_gt_eq_false; eauto. - auto. - destruct (Float.cmp FCeq n1 n2); auto. + unfold Float.ordered, Float.cmp; destruct (Float.compare n1 n2) as [[]|]; reflexivity. - (* notge *) - replace (Float.cmp FCnotge n1 n2) with (negb (Float.cmp FCge n1 n2)) by (symmetry; apply (Float.cmp_negate FCge)). - destruct (Float.cmp FCge n1 n2); auto. + unfold Float.cmp; destruct (Float.compare n1 n2) as [[]|]; auto. Opaque Float.cmp Float.ordered. Qed. @@ -827,77 +811,28 @@ Transparent Float32.cmp Float32.ordered. - (* ne *) unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. - (* lt *) - rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. - destruct (Float32.compare n2 n1) as [[]|]; reflexivity. -- (* le *) - rewrite <- (Float32.cmp_swap Cge n1 n2). simpl. - destruct (Float32.compare n1 n2) as [[]|]; auto. -- (* gt *) - unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. -- (* ge *) - destruct (Float32.cmp Cge n1 n2); auto. -Opaque Float32.cmp Float32.ordered. -Qed. - -Lemma testcond_for_neg_float32_comparison_correct: - forall c n1 n2 rs, - eval_extcond (testcond_for_condition (Cnotcompfs c)) - (nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2)) - (Vsingle (swap_floats c n2 n1)) rs)) = - Some(negb(Float32.cmp c n1 n2)). -Proof. - intros. - generalize (compare_floats32_spec rs (swap_floats c n1 n2) (swap_floats c n2 n1)). - set (rs' := nextinstr (compare_floats32 (Vsingle (swap_floats c n1 n2)) - (Vsingle (swap_floats c n2 n1)) rs)). - intros [A [B [C D]]]. - unfold eval_extcond, eval_testcond. rewrite A; rewrite B; rewrite C. - destruct c; simpl. -- (* eq *) -Transparent Float32.cmp Float32.ordered. - unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. -- (* ne *) - unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. -- (* lt *) - rewrite <- (Float32.cmp_swap Clt n2 n1). simpl. unfold Float32.ordered. + rewrite <- (Float32.cmp_swap FClt n2 n1). simpl. unfold Float32.ordered. destruct (Float32.compare n2 n1) as [[]|]; reflexivity. - (* le *) - rewrite <- (Float32.cmp_swap Cge n1 n2). simpl. + rewrite <- (Float32.cmp_swap FCge n1 n2). simpl. destruct (Float32.compare n1 n2) as [[]|]; auto. - (* gt *) unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. - (* ge *) - destruct (Float32.cmp Cge n1 n2); auto. + destruct (Float32.cmp FCge n1 n2); auto. - (* notlt *) - replace (Float32.cmp FCnotlt n1 n2) with (negb (Float32.cmp FClt n1 n2)) by (symmetry; apply (Float32.cmp_negate FClt)). - rewrite <- (Float32.cmp_swap FCge n1 n2). - rewrite <- (Float32.cmp_swap FCne n1 n2). - simpl. - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_le_lt_eq. - destruct (Float32.cmp FClt n1 n2) eqn:LT; simpl. - destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl. - exfalso. eapply Float32.cmp_lt_eq_false; eauto. - auto. - destruct (Float32.cmp FCeq n1 n2); auto. + rewrite <- (Float32.cmp_swap FCnotlt n2 n1). simpl. unfold Float32.ordered. + destruct (Float32.compare n2 n1) as [[]|]; reflexivity. - (* notle *) - replace (Float32.cmp FCnotle n1 n2) with (negb (Float32.cmp FCle n1 n2)) by (symmetry; apply (Float32.cmp_negate FCle)). - rewrite <- (Float32.cmp_swap FCge n1 n2). simpl. - destruct (Float32.cmp FCle n1 n2); auto. + rewrite <- (Float32.cmp_swap FCnotle n2 n1). simpl. + destruct (Float32.compare n2 n1) as [[]|]; reflexivity. - (* notgt *) - replace (Float32.cmp FCnotgt n1 n2) with (negb (Float32.cmp FCgt n1 n2)) by (symmetry; apply (Float32.cmp_negate FCgt)). - rewrite Float32.cmp_ne_eq. rewrite Float32.cmp_ge_gt_eq. - destruct (Float32.cmp FCgt n1 n2) eqn:GT; simpl. - destruct (Float32.cmp FCeq n1 n2) eqn:EQ; simpl. - exfalso. eapply Float32.cmp_gt_eq_false; eauto. - auto. - destruct (Float32.cmp FCeq n1 n2); auto. + unfold Float32.ordered, Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; reflexivity. - (* notge *) - replace (Float32.cmp FCnotge n1 n2) with (negb (Float32.cmp FCge n1 n2)) by (symmetry; apply (Float32.cmp_negate FCge)). - destruct (Float32.cmp FCge n1 n2); auto. + unfold Float32.cmp; destruct (Float32.compare n1 n2) as [[]|]; auto. Opaque Float32.cmp Float32.ordered. Qed. - Remark swap_floats_commut: forall (A B: Type) c (f: A -> B) x y, swap_floats c (f x) (f y) = f (swap_floats c x y). Proof. -- cgit