Require Import Reals.
Require Export VST.veric.base.
Require Import VST.veric.compcert_rmaps.
Require Import VST.veric.res_predicates.

(* This file contains lemmas regarding "superprecise",
and in principle, almost proving that "mapsto" is superprecise.

However, mapsto is not superprecise, because it's not quite true
that decode_val is injective.  The only reason is the treatment
of single-precision floating-point NaNs, where the conversion
from single-prec to double-prec loses one bit of information:
both quiet 32-bit NaNs and signalling 32-bit NaNs are quietly turned into
quite 64-bit NaNs.

If CompCert ever changes so that this does not happen, then
the lemmas in this file might become useful.

*)

Lemma int_of_bytes_uniq:
  forall i j, length i = length j -> int_of_bytes i = int_of_bytes j -> i = j.
Proof.
(* Goal: forall (i j : list Byte.int) (_ : @eq nat (@Datatypes.length Byte.int i) (@Datatypes.length Byte.int j)) (_ : @eq Z (int_of_bytes i) (int_of_bytes j)), @eq (list Byte.int) i j *)
  induction i; intros.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) j *)
 destruct j; inv H. auto.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) j *)
 destruct j; inv H.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int i0 j) *)
 specialize (IHi _ H2).
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int i0 j) *)
 simpl in H0.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int i0 j) *)
do 2 rewrite (Z.add_comm (Byte.unsigned _)) in H0.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int i0 j) *)
 remember (int_of_bytes j * 256 + Byte.unsigned i0) as v eqn:?H.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int i0 j) *)
 symmetry in H0.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int i0 j) *)
 rename i0 into b.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int b j) *)
 pose proof (Zmod_unique _ _ _ _ H (Byte.unsigned_range _)).
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int b j) *)
 pose proof (Zmod_unique _ _ _ _ H0 (Byte.unsigned_range _)).
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int b j) *)
 assert (Byte.repr (Byte.unsigned a) = Byte.repr (Byte.unsigned b)) by congruence.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int b j) *)
 repeat rewrite Byte.repr_unsigned in H4.
(* Goal: @eq (list Byte.int) (@Datatypes.cons Byte.int a i) (@Datatypes.cons Byte.int b j) *)
 subst b.
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
 f_equal. clear H1.
(* Goal: @eq (list Byte.int) i j *)
 apply IHi.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
 omega.
Qed.

Lemma decode_int_uniq:
  forall i j, length i = length j -> decode_int i = decode_int j -> i=j.
Proof.
(* Goal: forall (i j : list Byte.int) (_ : @eq nat (@Datatypes.length Byte.int i) (@Datatypes.length Byte.int j)) (_ : @eq Z (decode_int i) (decode_int j)), @eq (list Byte.int) i j *)
 unfold decode_int, rev_if_be.
(* Goal: forall (i j : list Byte.int) (_ : @eq nat (@Datatypes.length Byte.int i) (@Datatypes.length Byte.int j)) (_ : @eq Z (int_of_bytes (if Archi.big_endian then @rev Byte.int i else i)) (int_of_bytes (if Archi.big_endian then @rev Byte.int j else j))), @eq (list Byte.int) i j *)
 destruct Archi.big_endian.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
 intros. rewrite <- (rev_involutive i). rewrite <- (rev_involutive j).
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
 f_equal.
(* Goal: @eq (list Byte.int) (@rev Byte.int i) (@rev Byte.int j) *)
(* Goal: forall (i j : list Byte.int) (_ : @eq nat (@Datatypes.length Byte.int i) (@Datatypes.length Byte.int j)) (_ : @eq Z (int_of_bytes i) (int_of_bytes j)), @eq (list Byte.int) i j *)
 assert (length (rev i) = length (rev j)).
(* Goal: @app_pred rmap ag_rmap S w *)
 repeat rewrite rev_length; auto.
(* Goal: @app_pred rmap ag_rmap S w *)
 eapply int_of_bytes_uniq; eauto.
(* Goal: forall (i j : list Byte.int) (_ : @eq nat (@Datatypes.length Byte.int i) (@Datatypes.length Byte.int j)) (_ : @eq Z (int_of_bytes i) (int_of_bytes j)), @eq (list Byte.int) i j *)
 apply int_of_bytes_uniq.
Qed.

Lemma decode_int_range:
  forall l N, N = two_p (8 * Z.of_nat (length l)) -> 0 <= decode_int l < N.
Proof.
intros; subst; revert l.
unfold decode_int.
assert (forall l, 0 <= int_of_bytes l < two_p (8 * Z.of_nat (length l))).
(* Goal: @app_pred rmap ag_rmap S w *)
2: intros; rewrite <- rev_if_be_length; auto.
induction l.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
simpl; omega.
simpl int_of_bytes. simpl length.
rewrite Nat2Z.inj_succ.
unfold Z.succ.
rewrite Z.mul_add_distr_l.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
rewrite two_p_is_exp; try omega.
change (two_p (8*1)) with 256.
pose proof (Byte.unsigned_range a).
change Byte.modulus with 256 in H.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
omega.
Qed.

Lemma sign_ext_injective:
 forall n i j,
    0 < n < Int.zwordsize ->
    0 <= i < two_p n ->
    0 <= j < two_p n ->
    Int.sign_ext n (Int.repr i) = Int.sign_ext n (Int.repr j) ->
    i=j.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
pose proof (Int.eqmod_sign_ext n (Int.repr i) H).
pose proof (Int.eqmod_sign_ext n (Int.repr j) H).
rewrite H2 in H3.
apply Int.eqmod_sym in H3.
pose proof (Int.eqmod_trans _ _ _ _ H3 H4).
rewrite Int.unsigned_repr in H5.
2: pose proof (two_p_monotone_strict n Int.zwordsize);
   change Int.max_unsigned with (two_p Int.zwordsize - 1);
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
   omega.
rewrite Int.unsigned_repr in H5.
2: pose proof (two_p_monotone_strict n Int.zwordsize);
   change Int.max_unsigned with (two_p Int.zwordsize - 1);
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
   omega.
(* Goal: @app_pred rmap ag_rmap S w *)
apply Int.eqmod_small_eq in H5; auto.
Qed.


Lemma zero_ext_injective:
 forall n i j,
    0 <= n < Int.zwordsize ->
    0 <= i < two_p n ->
    0 <= j < two_p n ->
    Int.zero_ext n (Int.repr i) = Int.zero_ext n (Int.repr j) ->
    i=j.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
pose proof (Int.eqmod_zero_ext n (Int.repr i) H).
pose proof (Int.eqmod_zero_ext n (Int.repr j) H).
rewrite H2 in H3.
apply Int.eqmod_sym in H3.
pose proof (Int.eqmod_trans _ _ _ _ H3 H4).
rewrite Int.unsigned_repr in H5.
2: pose proof (two_p_monotone_strict n Int.zwordsize);
   change Int.max_unsigned with (two_p Int.zwordsize - 1);
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
   omega.
rewrite Int.unsigned_repr in H5.
2: pose proof (two_p_monotone_strict n Int.zwordsize);
   change Int.max_unsigned with (two_p Int.zwordsize - 1);
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
   omega.
(* Goal: @app_pred rmap ag_rmap S w *)
apply Int.eqmod_small_eq in H5; auto.
Qed.

Lemma repr_decode_int_inj:
  forall l1 l2, length l1 = 4%nat -> length l2 = 4%nat ->
    Int.repr (decode_int l1) = Int.repr (decode_int l2) ->
    l1=l2.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
apply decode_int_uniq; [congruence | ].
rewrite <- (Int.unsigned_repr (decode_int l1)).
2:{
pose proof (decode_int_range l1 _ (eq_refl _)).
rewrite H in H2.
change (two_p (8 * Z.of_nat 4)) with (Int.max_unsigned + 1) in H2.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
omega.
}
rewrite <- (Int.unsigned_repr (decode_int l2)).
2:{
pose proof (decode_int_range l2 _ (eq_refl _)).
rewrite H0 in H2.
change (two_p (8 * Z.of_nat 4)) with (Int.max_unsigned + 1) in H2.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
omega.
}
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
congruence.
Qed.

Lemma repr_decode_int64_inj:
  forall l1 l2, length l1 = 8%nat -> length l2 = 8%nat ->
    Int64.repr (decode_int l1) = Int64.repr (decode_int l2) ->
    l1=l2.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
apply decode_int_uniq; [congruence | ].
rewrite <- (Int64.unsigned_repr (decode_int l1)).
2:{
pose proof (decode_int_range l1 _ (eq_refl _)).
rewrite H in H2.
change (two_p (8 * Z.of_nat 8)) with (Int64.max_unsigned + 1) in H2.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
omega.
}
rewrite <- (Int64.unsigned_repr (decode_int l2)).
2:{
pose proof (decode_int_range l2 _ (eq_refl _)).
rewrite H0 in H2.
change (two_p (8 * Z.of_nat 8)) with (Int64.max_unsigned + 1) in H2.
(* Goal: @eq Z (int_of_bytes i) (int_of_bytes j) *)
omega.
}
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
congruence.
Qed.

Transparent Float.of_bits.
Transparent Float32.of_bits.

Lemma double_of_bits_inj:
  forall i j, Float.of_bits i = Float.of_bits j -> i=j.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
(* Goal: @eq Int64.int i j *)
unfold Float.of_bits in H.
(* Goal: @eq Int64.int i j *)
rewrite <- (Int64.repr_unsigned i).
(* Goal: @eq Int64.int (Int64.repr (Int64.unsigned i)) j *)
rewrite <- (Int64.repr_unsigned j).
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
f_equal.
(* Goal: @eq Z (Int64.unsigned i) (Int64.unsigned j) *)
unfold Fappli_IEEE_bits.b64_of_bits in H.
rewrite <- (Fappli_IEEE_bits.bits_of_binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _) (Int64.unsigned i))
  by (apply Int64.unsigned_range).
rewrite <- (Fappli_IEEE_bits.bits_of_binary_float_of_bits 52 11 (refl_equal _) (refl_equal _) (refl_equal _) (Int64.unsigned j))
  by (apply Int64.unsigned_range).
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xO (xO (xI (xO (xI xH)))))) (Zpos (xI (xI (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xO (xO (xI (xO (xI xH)))))) (Zpos (xI (xI (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xO (xO (xI (xO (xI xH)))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xI (xI (xO xH)))) (Zpos xH))))) (Int64.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xO (xO (xI (xO (xI xH)))))) (Zpos (xI (xI (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xO (xO (xI (xO (xI xH)))))) (Zpos (xI (xI (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xO (xO (xI (xO (xI xH)))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xI (xI (xO xH)))) (Zpos xH))))) (Int64.unsigned j))) *)
f_equal; apply H.
Qed.

Require Import ZArith.
From compcert Require Import Fappli_IEEE Fcore_Zaux Fcore_generic_fmt.

Lemma binary_normalize_inj:
  forall s1 m1 e1 (h1 : bounded 24 128 m1 e1 = true),
  forall s2 m2 e2 (h2 : bounded 24 128 m2 e2 = true),
   binary_normalize 53 1024 (eq_refl _) (eq_refl _) mode_NE (cond_Zopp s1 (Zpos m1)) e1 s1 =
   binary_normalize 53 1024 (eq_refl _) (eq_refl _) mode_NE (cond_Zopp s2 (Zpos m2)) e2 s2 ->
  B754_finite 24 128 s1 m1 e1 h1 = B754_finite 24 128 s2 m2 e2 h2.
Proof.
intros s1 m1 e1 h1 s2 m2 e2 h2 Hn.
apply B2R_inj ; try easy.
assert (H: forall s m e h,
  B2R 24 128 (B754_finite 24 128 s m e h) =
  B2R 53 1024 (binary_normalize 53 1024 (eq_refl _) (eq_refl _) mode_NE (cond_Zopp s (Zpos m)) e s)).
2: now rewrite 2!H, Hn.
clear.
(* Goal: forall (b : bool) (m : positive) (e : Z) (_ : @eq bool (bounded (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))) m e) true), match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp b (Zpos m)) e b with | @B754_zero _ _ b0 => False | @B754_infinity _ _ b0 => False | @B754_nan _ _ b0 n => False | @B754_finite _ _ b0 m0 e0 e1 => True end *)
intros s m e h.
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
generalize (binary_normalize_correct 53 1024 (eq_refl _) (eq_refl _) mode_NE (cond_Zopp s (Zpos m)) e s).
(* Goal: forall _ : if Fcore_Raux.Rlt_bool (Rabs (round radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (round_mode mode_NE) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) then and (@eq R (B2R (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (round radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (round_mode mode_NE) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)))) (and (@eq bool (is_finite (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) true) (@eq bool (Bsign (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) match Fcore_Raux.Rcompare (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0) with | Eq => s | Lt => true | Gt => false end)) else @eq full_float (B2FF (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (binary_overflow (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) mode_NE (Fcore_Raux.Rlt_bool (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0))), match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
rewrite round_generic ; auto with typeclass_instances.
rewrite  Fcore_Raux.Rlt_bool_true.
intros [-> _].
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
easy.
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
apply Raxioms.Rlt_trans with (1 := abs_B2R_lt_emax _ _ (B754_finite 24 128 s m e h)).
(* Goal: Rlt (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO xH))))))))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
now apply Fcore_Raux.bpow_lt.
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
apply Fcore_FLT.generic_format_FLT.
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
assert (h' := generic_format_B2R 24 128 (B754_finite 24 128 s m e h)).
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
apply Fcore_FLT.FLT_format_generic in h'.
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
destruct h' as [f [H1 [H2 H3]]].
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
exists f.
(* Goal: and (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (@Fcore_defs.F2R radix2 f)) (and (Z.lt (Z.abs (@Fcore_defs.Fnum radix2 f)) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH)))))))) (Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f))) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
rewrite <- H1.
(* Goal: and (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (B2R (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) (B754_finite (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) s m e h))) (and (Z.lt (Z.abs (@Fcore_defs.Fnum radix2 f)) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH)))))))) (Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f))) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
repeat split.
(* Goal: Z.lt (Z.abs (@Fcore_defs.Fnum radix2 f)) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH))))))) *)
(* Goal: Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
apply Z.lt_trans with (1 := H2).
(* Goal: Z.lt (Z.pow (radix_val radix2) (Zpos (xO (xO (xO (xI xH)))))) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH))))))) *)
(* Goal: Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
now apply Zpower_lt.
(* Goal: Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
now apply Z.le_trans with (2 := H3).
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
easy.
Qed.

Lemma binary_normalize_finite:
  forall b m e,
  bounded (23 + 1) (2 ^ (8 - 1)) m e = true ->
 match
     binary_normalize 53 1024 eq_refl eq_refl mode_NE
          (cond_Zopp b (Z.pos m)) e b
 with B754_finite _ _ _ _ => True | _ => False
 end.
Proof.
(* Goal: forall (b : bool) (m : positive) (e : Z) (_ : @eq bool (bounded (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))) m e) true), match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp b (Zpos m)) e b with | @B754_zero _ _ b0 => False | @B754_infinity _ _ b0 => False | @B754_nan _ _ b0 n => False | @B754_finite _ _ b0 m0 e0 e1 => True end *)
intros s m e h.
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
generalize (binary_normalize_correct 53 1024 (eq_refl _) (eq_refl _) mode_NE (cond_Zopp s (Zpos m)) e s).
(* Goal: forall _ : if Fcore_Raux.Rlt_bool (Rabs (round radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (round_mode mode_NE) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) then and (@eq R (B2R (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (round radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (round_mode mode_NE) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)))) (and (@eq bool (is_finite (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) true) (@eq bool (Bsign (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) match Fcore_Raux.Rcompare (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0) with | Eq => s | Lt => true | Gt => false end)) else @eq full_float (B2FF (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (binary_overflow (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) mode_NE (Fcore_Raux.Rlt_bool (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0))), match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
rewrite round_generic ; auto with typeclass_instances.
(* Goal: forall _ : if Fcore_Raux.Rlt_bool (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) then and (@eq R (B2R (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (and (@eq bool (is_finite (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) true) (@eq bool (Bsign (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) match Fcore_Raux.Rcompare (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0) with | Eq => s | Lt => true | Gt => false end)) else @eq full_float (B2FF (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (binary_overflow (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) mode_NE (Fcore_Raux.Rlt_bool (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0))), match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
rewrite Fcore_Raux.Rlt_bool_true.
(****)
(* Goal: forall _ : and (@eq R (B2R (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (and (@eq bool (is_finite (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) true) (@eq bool (Bsign (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) match Fcore_Raux.Rcompare (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (IZR Z0) with | Eq => s | Lt => true | Gt => false end)), match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
intros [H _].
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
assert (H': B2R 53 1024 (binary_normalize 53 1024 eq_refl eq_refl mode_NE (cond_Zopp s (Z.pos m)) e s) <> 0%R).
(* Goal: not (@eq R (B2R (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s)) (IZR Z0)) *)
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
  rewrite H, <- (Fcore_float_prop.F2R_0 radix2 e).
(* Goal: not (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 Z0 e))) *)
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
  case s.
(* Goal: not (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp true (Zpos m)) e)) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 Z0 e))) *)
(* Goal: not (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp false (Zpos m)) e)) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 Z0 e))) *)
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
  now apply RIneq.Rlt_not_eq, Fcore_float_prop.F2R_lt_compat.
(* Goal: not (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp false (Zpos m)) e)) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 Z0 e))) *)
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
  now apply RIneq.Rgt_not_eq, Fcore_float_prop.F2R_lt_compat.
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
clear H.
(* Goal: match binary_normalize (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xO (xI (xO (xI xH)))))))) (@eq_refl Datatypes.comparison (Z.compare (Zpos (xI (xO (xI (xO (xI xH)))))) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))) mode_NE (cond_Zopp s (Zpos m)) e s with | @B754_zero _ _ b => False | @B754_infinity _ _ b => False | @B754_nan _ _ b n => False | @B754_finite _ _ b m e e0 => True end *)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
destruct binary_normalize ; try easy ; now elim H'.
(****)
(* Goal: Rlt (Rabs (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
apply Raxioms.Rlt_trans with (1 := abs_B2R_lt_emax _ _ (B754_finite 24 128 s m e h)).
(* Goal: Rlt (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO xH))))))))) (Fcore_Raux.bpow radix2 (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) *)
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
now apply Fcore_Raux.bpow_lt.
(* Goal: generic_format radix2 (Fcore_FLT.FLT_exp (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
apply Fcore_FLT.generic_format_FLT.
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
assert (h' := generic_format_B2R 24 128 (B754_finite 24 128 s m e h)).
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
apply Fcore_FLT.FLT_format_generic in h'.
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
destruct h' as [f [H1 [H2 H3]]].
(* Goal: Fcore_FLT.FLT_format radix2 (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (Zpos (xI (xO (xI (xO (xI xH)))))) (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
exists f.
(* Goal: and (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (@Fcore_defs.F2R radix2 f)) (and (Z.lt (Z.abs (@Fcore_defs.Fnum radix2 f)) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH)))))))) (Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f))) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
rewrite <- H1.
(* Goal: and (@eq R (@Fcore_defs.F2R radix2 (Fcore_defs.Float radix2 (cond_Zopp s (Zpos m)) e)) (B2R (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) (B754_finite (Zpos (xO (xO (xO (xI xH))))) (Zpos (xO (xO (xO (xO (xO (xO (xO xH)))))))) s m e h))) (and (Z.lt (Z.abs (@Fcore_defs.Fnum radix2 f)) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH)))))))) (Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f))) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
repeat split.
(* Goal: Z.lt (Z.abs (@Fcore_defs.Fnum radix2 f)) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH))))))) *)
(* Goal: Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
apply Z.lt_trans with (1 := H2).
(* Goal: Z.lt (Z.pow (radix_val radix2) (Zpos (xO (xO (xO (xI xH)))))) (Z.pow (radix_val radix2) (Zpos (xI (xO (xI (xO (xI xH))))))) *)
(* Goal: Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
now apply Zpower_lt.
(* Goal: Z.le (Z.sub (Z.sub (Zpos (xI xH)) (Zpos (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))) (Zpos (xI (xO (xI (xO (xI xH))))))) (@Fcore_defs.Fexp radix2 f) *)
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
now apply Z.le_trans with (2 := H3).
(* Goal: Fcore_FLX.Prec_gt_0 (Zpos (xO (xO (xO (xI xH))))) *)
easy.
Qed.

Lemma float32_preserves_payload:
 forall s pl,
    let '(s1,pl1) := Float.of_single_pl s pl in
      (s=s1 /\ (536870912 * (Pos.lor (proj1_sig pl) 4194304))%positive = proj1_sig pl1).
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
 intros.
(* Goal: let 'pair s1 pl1 := Float.of_single_pl s pl in and (@eq bool s s1) (@eq positive (Pos.mul (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH))))))))))))))))))))))))))))) (Pos.lor (@proj1_sig positive (fun pl : positive => @eq bool (Z.ltb (Zpos (Fcore_digits.digits2_pos pl)) (Zpos (xO (xO (xO (xI xH)))))) true) pl) (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO (xO xH)))))))))))))))))))))))) (@proj1_sig positive (fun pl : positive => @eq bool (Z.ltb (Zpos (Fcore_digits.digits2_pos pl)) (Zpos (xI (xO (xI (xO (xI xH))))))) true) pl1)) *)
 unfold Float.of_single_pl.
(* Goal: @app_pred rmap ag_rmap S w *)
 split; auto.
Qed.

Lemma pos_lor_inj:  (* not true *)
  forall k N (a b: nan_pl k),
     Zpower_nat 2 (Z.to_nat (k-2)) = Zpos N ->
     Pos.lor (proj1_sig a) N =  Pos.lor (proj1_sig b) N ->
    a=b.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
 destruct a as [a Ha]. destruct b as [b Hb].
 simpl in *.
 assert (a=b); [ | subst a; f_equal; apply Axioms.proof_irr].
Abort.

Inductive wishes_eq_horses := .

Lemma float32_payload_inj:
  wishes_eq_horses ->
  forall s1 pl1 s2 pl2,
    Float.of_single_pl s1 pl1= Float.of_single_pl s2 pl2 ->
    (s1,pl1) = (s2,pl2).
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intro WH; intros.
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
 pose proof (float32_preserves_payload s1 pl1).
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
 pose proof (float32_preserves_payload s2 pl2).
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
 rewrite H in H0. clear H.
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
 destruct (Float.of_single_pl s2 pl2).
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
 destruct H0,H1. subst.
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
 f_equal.
(* Goal: @eq (nan_pl (Zpos (xO (xO (xO (xI xH)))))) pl1 pl2 *)
 rewrite <- H2 in H0; clear - WH H0.
(* Goal: @eq (nan_pl (Zpos (xO (xO (xO (xI xH)))))) pl1 pl2 *)
 apply Pos.mul_reg_l in H0.
(* Goal: @eq (nan_pl (Zpos (xO (xO (xO (xI xH)))))) pl1 pl2 *)
 contradiction WH.
Qed.

Lemma single_of_bits_inj:
  forall i j : Int.int, Float32.of_bits i = Float32.of_bits j -> i=j.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
(* Goal: @eq Int.int i j *)
unfold Float32.of_bits in H.
(* Goal: @eq Int.int i j *)
rewrite <- (Int.repr_unsigned i).
(* Goal: @eq Int.int (Int.repr (Int.unsigned i)) j *)
rewrite <- (Int.repr_unsigned j).
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
f_equal.
rewrite <- (Fappli_IEEE_bits.bits_of_binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _) (Int.unsigned i))
  by (apply Int.unsigned_range).
rewrite <- (Fappli_IEEE_bits.bits_of_binary_float_of_bits 23 8 (refl_equal _) (refl_equal _) (refl_equal _) (Int.unsigned j))
  by (apply Int.unsigned_range).
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
f_equal.
(* Goal: @eq (binary_float (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i)) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j)) *)
unfold Fappli_IEEE_bits.b32_of_bits in H.
match goal with |- ?A = ?B => remember A as u eqn:H9; remember B as v eqn:H10;
   clear H9 H10 end.
(* Goal: @eq (binary_float (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH)))) u v *)
clear i j.

(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct u,v; auto; try congruence.
Qed.

Lemma Vint_inj: forall i j, Vint i = Vint j -> i=j.
Proof. congruence. Qed.

Lemma decode_val_uniq:
   (* Just not true any more, with Fragments *)
  forall ch b1 b2 v,
    v <> Vundef ->
    length b1 = size_chunk_nat ch ->
    length b2 = size_chunk_nat ch ->
    decode_val ch b1 = v ->
    decode_val ch b2 = v ->
    b1=b2.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
 intros.
 unfold size_chunk_nat in *.
 unfold decode_val in *.
 destruct (proj_bytes b1) eqn:B1.
subst v.
(*
unfold proj_pointer in H3.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct b1; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct m; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
if_tac in H3; try congruence.
clear - H2 H3 H.
subst v.
unfold proj_pointer in *.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct b1; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct m; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct b2; try congruence. destruct m; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct (check_pointer 4 b i (Pointer b i n :: b1)) eqn:?; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct (check_pointer 4 b0 i0 (Pointer b0 i0 n0 :: b2)) eqn:?; try congruence.
inv H3.
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
clear H.
unfold check_pointer in *; simpl in *.
repeat match goal with
| H: ?A = true |- _ =>
  match A with
  | context [eq_block ?a ?b]  =>
     destruct (eq_block a b); simpl in *; try congruence
  | context [Int.eq_dec ?i ?j] =>
     destruct (Int.eq_dec i j); simpl in *; try congruence
  | context [match ?n with _ => _ end] =>
     destruct n; simpl in *; try congruence
  end
end.
} Unfocus.
destruct (proj_bytes b2) eqn:B2.
2:{
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct ch; try congruence.
unfold proj_pointer in H3.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct b2; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct m; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
if_tac in H3; try congruence.
}
pose proof (length_proj_bytes _ _ B1).
pose proof (length_proj_bytes _ _ B2).
rewrite <- H4 in *; rewrite <- H5 in *.
assert (l=l0).
2:{
clear - H6 B1 B2.
revert l0 b1 b2 B1 B2 H6; induction l; destruct l0; intros; inv H6.
(* Goal: @app_pred rmap ag_rmap S w *)
destruct b1; inv B1. destruct b2; inv B2; auto.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct m; try congruence.
destruct (proj_bytes b2);  inv H0.
destruct m; inv H0.
destruct (proj_bytes b1);  inv H1.
destruct b1; inv B1.
destruct m; inv H0.
destruct (proj_bytes b1) eqn:?; inv H1.
destruct b2; inv B2.
destruct m; inv H0.
destruct (proj_bytes b2) eqn:?; inv H1.
specialize (IHl _ _ _ Heqo Heqo0).
(* Goal: @app_pred rmap ag_rmap S w *)
f_equal; auto.
}
clear b1 b2 H4 H5 B1 B2.
(* Goal: @eq (prod bool (nan_pl (Zpos (xO (xO (xO (xI xH))))))) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s1 pl1) (@pair bool (nan_pl (Zpos (xO (xO (xO (xI xH)))))) s2 pl2) *)
clear H.
subst v.
destruct ch; try apply Vint_inj in H3;
simpl in H0,H1; unfold Pos.to_nat in H0,H1; simpl in H0,H1;
 (* this "try" takes care of all signed and unsigned bytes and shorts *)
try (apply decode_int_uniq; [ congruence | ];
(apply sign_ext_injective in H3 || apply zero_ext_injective in H3);
 [ congruence |  compute; split; congruence
 | apply decode_int_range; rewrite H1; reflexivity
 | apply decode_int_range; rewrite H0; reflexivity
 ]).

(* Goal: @app_pred rmap ag_rmap S w *)
* (* Mint32 *)  apply repr_decode_int_inj; auto.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
* (* Mint64 *) apply repr_decode_int64_inj; congruence.
* (* Mfloat32 *)
  inv H3.
  apply decode_int_uniq; [congruence | ].
  apply single_of_bits_inj in H2.
(* Goal: @app_pred rmap ag_rmap S w *)
  apply repr_decode_int_inj in H2; auto.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
  congruence.
  apply WH.
* (* Mfloat64 *)
  inv H3.
  apply decode_int_uniq; [congruence | ].
  apply double_of_bits_inj in H2.
(* Goal: @app_pred rmap ag_rmap S w *)
  apply repr_decode_int64_inj in H2; auto.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
  congruence.
Qed.
*)
Abort.


Lemma superprecise_ewand_lem1:
  forall S P: pred rmap, superprecise P ->
          S |-- P * TT ->
          S = (P * (ewand P S))%pred.
Proof.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
(* Goal: @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
apply pred_ext.
(* Goal: @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) S *)
intros w ?. specialize (H0 w H1).
(* Goal: @app_pred rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) w *)
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) S *)
destruct H0 as [w1 [w2 [? [? _]]]].
(* Goal: @app_pred rmap ag_rmap S w *)
exists w1; exists w2; split3; auto.
(* Goal: @app_pred rmap ag_rmap S w *)
exists w1; exists w; split3; auto.
(* Goal: @derives rmap ag_rmap (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) S *)
intros w [w1 [w2 [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap S w *)
destruct H3 as [w3 [w4 [? [? ?]]]].
(* Goal: @app_pred rmap ag_rmap S w *)
assert (w1=w3). eapply H; eauto.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
apply join_core2 in H1; apply join_core2 in H3; unfold comparable; congruence.
(* Goal: @app_pred rmap ag_rmap S w *)
subst w3.
(* Goal: @app_pred rmap ag_rmap S w *)
pose proof (join_eq H1 H3); subst w4.
(* Goal: @app_pred rmap ag_rmap S w *)
auto.
Qed.

(*Lemma superprecise_address_mapsto:
  wishes_eq_horses -> 
  forall ch v sh loc, 
   v<>Vundef -> superprecise (address_mapsto ch v sh loc).
Proof.
intro WH.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
hnf; intros.
unfold address_mapsto in *.
destruct H0 as [b1 [[? [? ?]] ?]]; destruct H1 as [b2 [[? [? ?]] ?]].
(* just not true anymore, with Fragments *)
(*
assert (b1=b2) by (eapply decode_val_uniq; eauto).
subst b2.
assert (level w1 = level w2).
clear - H2; unfold comparable in H2.
rewrite <- level_core. rewrite <- (level_core w2).
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
congruence.
apply rmap_ext.
(* Goal: @app_pred rmap ag_rmap S w *)
auto.
intro.
clear - H5 H8 H9 H2.
specialize (H5 l); specialize (H8 l).
hnf in H5,H8.
if_tac in H5.
destruct H5 as [p ?]. destruct H8 as [p' ?].
hnf in H0,H1.
rewrite H0,H1.
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
f_equal.
(* Goal: @eq Z (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned i))) (Fappli_IEEE_bits.bits_of_binary_float (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (Fappli_IEEE_bits.binary_float_of_bits (Zpos (xI (xI (xI (xO xH))))) (Zpos (xO (xO (xO xH)))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xI (xI (xI (xO xH))))))) (@eq_refl Datatypes.comparison (Z.compare Z0 (Zpos (xO (xO (xO xH)))))) (@eq_refl Datatypes.comparison (Z.compare (Z.add (Zpos (xI (xI (xI (xO xH))))) (Zpos xH)) (Z.pow (Zpos (xO xH)) (Z.sub (Zpos (xO (xO (xO xH)))) (Zpos xH))))) (Int.unsigned j))) *)
f_equal.
apply proof_irr.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
congruence.
do 3 red in H5, H8.
unfold comparable in H2; clear - H5 H8 H2.
assert (core (w1 @ l) = core (w2 @ l)).
repeat rewrite core_resource_at.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
congruence.
clear H2.
transitivity (core (w1 @ l)).
apply unit_core.
apply  identity_unit_equiv.
(* Goal: @app_pred rmap ag_rmap S w *)
auto.
rewrite H.
symmetry.
apply unit_core.
apply  identity_unit_equiv.
(* Goal: @app_pred rmap ag_rmap S w *)
auto.
Qed.

Require Import VST.veric.extend_tc. (-this line is in a comment-)
Require Import VST.veric.seplog. (-this line is in a comment-)

Lemma superprecise_mapsto:
 wishes_eq_horses ->
  forall sh t v1 v2,
    v2 <> Vundef ->
   superprecise (mapsto sh t v1 v2).
Proof.
intro WH.
assert (WH' := superprecise_address_mapsto WH); clear WH.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
intros. rename H into Hv2.
(* Goal: forall (S P : @pred rmap ag_rmap) (_ : @superprecise rmap Join_rmap Perm_rmap Sep_rmap ag_rmap Age_rmap P) (_ : @derives rmap ag_rmap S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@TT rmap ag_rmap))), @eq (@pred rmap ag_rmap) S (@sepcon rmap Join_rmap Perm_rmap ag_rmap Age_rmap P (@ewand rmap Join_rmap Perm_rmap ag_rmap Age_rmap P S)) *)
hnf; intros.
unfold mapsto in *;
simpl in H,H0.
destruct (access_mode t); try contradiction.
destruct (type_is_volatile t); try contradiction.
destruct v1; try contradiction.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct H as [[_ H]|[Hz [u1 H]]]; try congruence.
(* Goal: forall (i j : Int.int) (_ : @eq val (Vint i) (Vint j)), @eq Int.int i j *)
destruct H0 as [[_ H0]|[Hz [u2 H0]]]; try congruence.
(* Goal: @app_pred rmap ag_rmap S w *)
eapply WH'; eauto.
Qed.
*)
Abort.
*)
