Fix postfreezeW_correct_and_bounded

2 files changed, 14 insertions, 7 deletions

diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 3936d70c2..eed6cc020 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -150,7 +150,8 @@ Proof.
   { match goal with
     |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end.
 
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+    preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
@@ -169,12 +170,13 @@ Proof.
   end. }
 
 
-  unfold_is_bounded.
-  change ZToWord64 with Interpretations64.WordW.ZToWordW in *.
+  change ZToWord64 with Interpretations64.WordW.ZToWordW in *;
+  preunfold_is_bounded.
   rewrite !Interpretations64.WordW.wordWToZ_sub;
   rewrite !Interpretations64.WordW.wordWToZ_land;
   rewrite !Interpretations64.WordW.wordWToZ_ZToWordW;
   repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end;
+  Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt;
   try match goal with
          | |- 0 <=  ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega
          | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity]
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 9184d0dc8..7b47a8509 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H :=
        unfold_is_bounded_in' H2
   | _ => idtac
   end.
-Ltac unfold_is_bounded_in H :=
+Ltac preunfold_is_bounded_in H :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519WToZ, wire_digitsWToZ in H;
-  cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519 List.length wire_widths] in H;
+  cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519 List.length wire_widths] in H.
+Ltac unfold_is_bounded_in H :=
+  preunfold_is_bounded_in H;
   unfold_is_bounded_in' H.
 
-Ltac unfold_is_bounded :=
+Ltac preunfold_is_bounded :=
   unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519WToZ, wire_digitsWToZ;
-  cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519 List.length wire_widths];
+  cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519 List.length wire_widths].
+
+Ltac unfold_is_bounded :=
+  preunfold_is_bounded;
   repeat match goal with
          | [ |- andb _ _ = true ] => apply andb_true_intro
          | [ |- and _ _ ] => split