From f6e1cd79c17461d50f5119818e788d1e07451ef6 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Feb 2022 17:50:40 +0100
Subject: rm useless stuff

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

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index bbd94321..8cab70b8 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -2053,54 +2053,6 @@ Proof.
   reflexivity.
 Qed.
 
-Definition anystep_div_longu a b m :=
-  Val.select (Val.cmplu_bool (Mem.valid_pointer m) Cgt b (Vlong (Int64.repr smallb_thresh)))
-             (step2_div_longu a b)
-             (twostep_div_longu a b) Tlong.
-
-Lemma anystep_div_longu_correct :
-  forall a b m
-           (b_RANGE : (1 < Int64.unsigned b <= Int64.max_signed)%Z),
-      anystep_div_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr (Int64.unsigned a / Int64.unsigned b))%Z.
-Proof.
-  intros.
-  unfold anystep_div_longu.
-  set (a' := Int64.unsigned a).
-  set (b' := Int64.unsigned b).
-  assert (0 < b')%Z as b_NOT0 by lia.
-  cbn.
-  unfold Int64.ltu.
-  fold b'.
-  rewrite Int64.unsigned_repr; cycle 1.
-  { unfold smallb_thresh.
-    change Int64.max_unsigned with 18446744073709551615%Z.
-    lia.
-  }
-  destruct zlt.
-  { rewrite step2_div_longu_bigb_correct by lia.
-    reflexivity.
-  }
-  rewrite twostep_div_longu_smallb_correct by lia.
-  cbn.
-  rewrite Int64.eq_false ; cycle 1.
-  { intro Z. unfold b' in b_NOT0. rewrite Z in b_NOT0.
-    rewrite Int64.unsigned_zero in b_NOT0.
-    lia.
-  }
-  reflexivity.
-Qed.
-
-
-Definition full_div_longu a b m :=
-  let is_big := Val.cmpl_bool Clt b (Vlong Int64.zero) in
-  let is_one := Val.cmplu_bool (Mem.valid_pointer m) Cle b (Vlong Int64.one) in
-  let is_special := Val.or (Val.of_optbool is_big) (Val.of_optbool is_one) in
-  let if_big := Val.longofintu (Val.of_optbool (Val.cmplu_bool (Mem.valid_pointer m) Cge a b)) in
-  let if_special := Val.select is_big if_big a Tlong in
-  Val.select (Val.cmp_bool Cne is_special (Vint Int.zero))
-             if_special
-             (anystep_div_longu a b m) Tlong.
-
 Lemma one_bigb_div :
   forall a b
      (b_RANGE : (9223372036854775808 <= b < 18446744073709551616)%Z)
@@ -2117,81 +2069,6 @@ Proof.
   ring.
 Qed.
 
-Lemma full_div_longu_correct :
-  forall a b m
-           (b_NOT0 : (0 < Int64.unsigned b)%Z),
-      full_div_longu (Vlong a) (Vlong b) m = Vlong (Int64.repr (Int64.unsigned a / Int64.unsigned b))%Z.
-Proof.
-
-  Local Opaque anystep_div_longu.
-  intros.
-  unfold full_div_longu.
-  cbn.
-  unfold Int64.lt, Int64.ltu.
-  pose proof (Int64.unsigned_range a).
-  pose proof (Int64.unsigned_range b).
-  set (a' := Int64.unsigned a) in *.
-  set (b' := Int64.unsigned b) in *.
-  rewrite Int64.signed_zero.
-  rewrite Int64.unsigned_one.
-  destruct zlt.
-  { replace  (Val.cmp_bool Cne
-       (Val.or Vtrue
-          (if negb (if zlt 1 b' then true else false) then Vtrue else Vfalse))
-       (Vint Int.zero)) with (Some true) ; cycle 1.
-    { destruct zlt; reflexivity.
-    }
-    cbn.
-    destruct zlt; cbn.
-    { rewrite Zdiv_small by lia.
-      reflexivity.
-    }
-    rewrite one_bigb_div.
-    reflexivity.
-    {
-      change Int64.modulus with 18446744073709551616%Z in *.
-      split. 2: lia.
-      unfold b'.
-      rewrite Int64.unsigned_signed.
-      unfold Int64.lt.
-      rewrite Int64.signed_zero.
-      rewrite zlt_true by lia.
-      pose proof (Int64.signed_range b).
-      change Int64.min_signed with (-9223372036854775808)%Z in *.
-      change Int64.max_signed with (9223372036854775807)%Z in *.
-      change Int64.modulus with 18446744073709551616%Z in *.
-      lia.
-    }
-    change Int64.modulus with 18446744073709551616%Z in *.
-    lia.
-  }
-  destruct zlt; cbn.
-  { change (negb (Int.eq (Int.or Int.zero Int.zero) Int.zero)) with false.
-    cbn.
-    rewrite anystep_div_longu_correct.
-    reflexivity.
-    
-    change Int64.modulus with 18446744073709551616%Z in *.
-    split. lia.
-    rewrite Int64.unsigned_signed.
-    unfold Int64.lt.
-    rewrite Int64.signed_zero.
-    rewrite zlt_false by lia.
-    pose proof (Int64.signed_range b).
-    change Int64.min_signed with (-9223372036854775808)%Z in *.
-    change Int64.max_signed with (9223372036854775807)%Z in *.
-    change Int64.modulus with 18446744073709551616%Z in *.
-    lia.
-  }
-  change (negb (Int.eq (Int.or Int.zero Int.one) Int.zero)) with true.
-  cbn.
-  replace b' with 1%Z by lia.
-  rewrite Z.div_1_r.
-  unfold a'.
-  rewrite Int64.repr_unsigned.
-  reflexivity.
-Qed.
-
 Lemma repr_unsigned_sub2:
   forall a b,
     (Int64.repr (a - Int64.unsigned (Int64.repr b))) = Int64.repr (a - b).
-- 
cgit