From 6290759de7aec8ec914c16eac6882b353ad980f1 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 24 Jan 2022 21:07:29 +0100
Subject: rm spurious function

---
 kvx/FPDivision64.v | 115 -----------------------------------------------------
 1 file changed, 115 deletions(-)

(limited to 'kvx/FPDivision64.v')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 580f4dd9..1e5d8478 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1542,118 +1542,3 @@ Proof.
   unfold approx_inv_rel_thresh in *.
   gappa.
 Qed.
-
-Lemma step2_real_div_long_bigb_correct :
-    forall (a b : int64)
-           (b_BIG : ((Int64.unsigned b) > smallb_thresh)%Z),
-    exists (q : float),
-      (step2_real_div_long (Vlong a) (Vlong b)) = Vfloat q /\
-        (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (32767/65536))%R /\
-      is_finite _ _ q = true.
-Proof.
-  intros.
-  pose proof (Int64.unsigned_range b) as b_RANGE.
-  change Int64.modulus with 18446744073709551616%Z in b_RANGE.
-  set (a' := (Int64.signed a)) in *.
-  set (b' := (Int64.unsigned b)) in *.
-  assert (IZR (1 + smallb_thresh) <= IZR b' <= 18446744073709551615)%R as b_RANGE'.
-  { split; apply IZR_le; lia.
-  } 
-  destruct (step2_real_div_long_smalla_correct a b a_SMALL b_NOT0) as (q & C1R & C1E & C1F).
-  fold a' b' in C1E.
-  assert ((Int64.min_signed <=? ZnearestE (B2R 53 1024 q))=true)%Z as q_LOW.
-  { apply Zle_imp_le_bool.
-    change Int64.min_signed with (-9223372036854775808)%Z.
-    apply Znearest_lub.
-    set (q' :=  B2R 53 1024 q) in *.
-    replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
-    unfold smalla_thresh in a_RANGE'.
-    gappa.
-  }
-  assert ((ZnearestE (B2R 53 1024 q) <=? Int64.max_signed)=true)%Z as q_HIGH.
-  { apply Zle_imp_le_bool.
-    change Int64.max_signed with (9223372036854775807)%Z.
-    apply Znearest_glb.
-    set (q' :=  B2R 53 1024 q) in *.
-    replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
-    unfold smalla_thresh in a_RANGE'.
-    gappa.
-  }
-  unfold step2_div_long, step2_div_long'.
-  rewrite C1R.
-  cbn.
-  unfold Float.to_long_ne.
-  rewrite (ZofB_ne_range_correct _ _ q Int64.min_signed Int64.max_signed).
-  rewrite C1F.
-  rewrite q_LOW.
-  rewrite q_HIGH.
-  cbn.
-  rewrite normalize_ite.
-  cbn.
-  rewrite <- (function_ite Vlong).
-  f_equal.
-  unfold Int64.lt.
-  set (q' :=  B2R 53 1024 q) in *.
-  fold a'.
-  assert (Int64.signed (Int64.repr (ZnearestE q')) = ZnearestE q') as q_SIGNED.
-  { apply Int64.signed_repr.
-    split; lia.
-  }
-  rewrite Int64.add_signed.
-  rewrite q_SIGNED.
-  rewrite Int64.signed_mone.
-  rewrite Int64.signed_zero.
-  rewrite <- (function_ite Int64.repr).
-  f_equal.
-  replace  (ZnearestE q' + -1)%Z with (ZnearestE q' - 1)%Z by ring.
-  
-  set (q'' :=  (ZnearestE q')) in *.
-  Check Int64.sub_signed.
-  fold a'.
-  rewrite int64_mul_signed_unsigned.
-  rewrite q_SIGNED.
-  fold b'.
-
-  rewrite Int64.sub_signed.
-  fold a'.
-  rewrite signed_repr_sub.
-
-  assert ((Rabs (IZR a' / IZR b' - q') < / 2)%R) as HALF.
-  { replace (IZR a' / IZR b' - q')%R with
-      (-(q' - IZR a' / IZR b'))%R by ring.
-    rewrite Rabs_Ropp.
-    lra.
-  }
-  pose proof (find_quotient a' b' b_NOT0 q' HALF) as QUOTIENT.
-  fold q'' in QUOTIENT.
-  cbn zeta in QUOTIENT.
-
-  assert (b' <> 0)%Z as NONZ by lia.
-  pose proof (Zmod_eq_full a' b' NONZ) as MOD.
-  assert (b' > 0)%Z as b_GT0 by lia.
-  pose proof (Z_mod_lt a' b' b_GT0) as MOD_LT.
-  destruct (Z_lt_dec a' (b' * q'')) as [LT | GE].
-  { replace (b' * q'' >? a')%Z with true in QUOTIENT by lia.
-    replace q'' with (1 + (a' / b'))%Z by lia.
-    replace ((1 + a' / b') * b' - a')%Z
-      with (-(a' - a' / b' * b')+b')%Z by ring.
-    rewrite <- MOD.
-    rewrite Int64.signed_repr; cycle 1.
-    { change Int64.min_signed with (-9223372036854775808)%Z in *.
-      change Int64.max_signed with (9223372036854775807)%Z in *.
-      lia.
-    }
-    rewrite zlt_true by lia.
-    ring.
-  }
-  replace (b' * q'' >? a')%Z with false in QUOTIENT by lia.
-  rewrite <- QUOTIENT.
-  replace (a' / b' * b' - a')%Z with (-(a' - a' / b' * b'))%Z by ring.
-  rewrite <- MOD.
-  rewrite Int64.signed_repr ; cycle 1.
-  { change Int64.min_signed with (-9223372036854775808)%Z in *.
-    change Int64.max_signed with (9223372036854775807)%Z in *.
-    lia.
-  }
-  rewrite zlt_false by lia.
-  reflexivity.
-- 
cgit