Handle both kinds of sqrt

1 files changed, 33 insertions, 25 deletions

diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v
index 6839160c5..3f7087446 100644
--- a/src/Specific/GF25519Bounded.v
+++ b/src/Specific/GF25519Bounded.v
@@ -294,7 +294,6 @@ Definition sqrt_m1W := Eval cbv [sqrt_m1W' fe25519W_word64ize word64ize andb opt
 
 Definition GF25519sqrt (x : GF25519.fe25519) : GF25519.fe25519.
 Proof.
-Print GF25519.sqrt.
   lazymatch (eval cbv delta [GF25519.sqrt] in GF25519.sqrt) with
   | (fun powf powf_squared f => dlet a := powf in _)
     => exact (dlet powx := powW (fe25519ZToW x) (chain GF25519.sqrt_ec) in
@@ -314,39 +313,48 @@ Proof.
   split.
   { etransitivity.
     Focus 2. {
-      apply Proper_Let_In_nd_changebody_eq; intros;
-        set_evars;
-        match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
-        | [ |- ?x = dlet y := fe25519WToZ ?z in ?f ]
-          => is_var z; change (x = match fe25519WToZ z with y => f end)
-        end;
-        change sqrt_m1 with (fe25519WToZ sqrt_m1W);
-        rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519WToZ)
-          by repeat match goal with
-                    | _ => progress subst
-                    | [ |- is_bounded (fe25519WToZ ?op) = true ]
-                      => lazymatch op with
-                         | mulW _ _ => apply mulW_correct_and_bounded
-                         | mulW_noinline _ _ => apply mulW_correct_and_bounded
-                         | powW _ _ => apply powW_correct_and_bounded
-                         | sqrt_m1W => vm_compute; reflexivity
-                         | _ => assumption
-                         end
-                    end;
-        subst_evars; reflexivity.
+      lazymatch goal with
+      | [ |- _ = pow _ _ ]
+        => apply powW_correct_and_bounded; assumption
+      | [ |- _ = (dlet powx := _ in _) ]
+        => apply Proper_Let_In_nd_changebody_eq; intros;
+             set_evars;
+             match goal with (* unfold the first dlet ... in, but only if it's binding a var *)
+             | [ |- ?x = dlet y := fe25519WToZ ?z in ?f ]
+               => is_var z; change (x = match fe25519WToZ z with y => f end)
+             end;
+             change sqrt_m1 with (fe25519WToZ sqrt_m1W);
+             rewrite <- (fun X Y => proj1 (mulW_correct_and_bounded sqrt_m1W a X Y)), <- eqbW_correct, (pull_bool_if fe25519WToZ)
+               by repeat match goal with
+                         | _ => progress subst
+                         | [ |- is_bounded (fe25519WToZ ?op) = true ]
+                           => lazymatch op with
+                              | mulW _ _ => apply mulW_correct_and_bounded
+                              | mulW_noinline _ _ => apply mulW_correct_and_bounded
+                              | powW _ _ => apply powW_correct_and_bounded
+                              | sqrt_m1W => vm_compute; reflexivity
+                              | _ => assumption
+                              end
+                         end;
+             subst_evars; reflexivity
+      end.
     } Unfocus.
     lazymatch goal with
     | [ |- context G[dlet x := ?v in fe25519WToZ (@?f x)] ]
       => let G' := context G[fe25519WToZ (dlet x := v in f x)] in
          cut G'; cbv beta;
            [ cbv [Let_In]; exact (fun x => x) | apply f_equal ]
+    | _ => idtac
     end;
       reflexivity. }
   { cbv [Let_In];
-      break_if;
-      [ apply powW_correct_and_bounded; assumption
-      |  apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ];
-         apply powW_correct_and_bounded; assumption ]. }
+      try break_if;
+      repeat lazymatch goal with
+             | [ |- is_bounded (?WToZ (powW _ _)) = true ]
+               => apply powW_correct_and_bounded; assumption
+             | [ |- is_bounded (?WToZ (mulW _ _)) = true ]
+               => apply mulW_correct_and_bounded; [ vm_compute; reflexivity | ]
+             end. }
 Defined.
 
 Definition sqrtW (f : fe25519W) : fe25519W :=