Drop CSE from Fancy Machine

By being careful about building the expressions in the first place, we
no longer need it, and can rely on dead code elimination.

1 files changed, 16 insertions, 3 deletions

diff --git a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
index a7d5242b6..aca1753b7 100644
--- a/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
+++ b/src/BoundedArithmetic/ArchitectureToZLikeProofs.v
@@ -38,7 +38,7 @@ Section fancy_machine_p256_montgomery_foundation.
            pose proof (decode_range x)
     end.
   Local Ltac unfolder_t :=
-    progress unfold LargeT, SmallT, modulus_digits, decode_large, decode_small, Mod_SmallBound, DivBy_SmallBound, DivBy_SmallerBound, Mul, CarryAdd, CarrySubSmall, ConditionalSubtract, ConditionalSubtractModulus, ZLikeOps_of_ArchitectureBoundedOps in *.
+    progress unfold LargeT, SmallT, modulus_digits, decode_large, decode_small, Mod_SmallBound, DivBy_SmallBound, DivBy_SmallerBound, Mul, CarryAdd, CarrySubSmall, ConditionalSubtract, ConditionalSubtractModulus, ZLikeOps_of_ArchitectureBoundedOps, ZLikeOps_of_ArchitectureBoundedOps_Factored in *.
   Local Ltac saturate_context_step :=
     match goal with
     | _ => unique assert (0 <= 2 * n_over_two) by solve [ eauto using decode_exponent_nonnegative with typeclass_instances | omega ]
@@ -54,6 +54,7 @@ Section fancy_machine_p256_montgomery_foundation.
   Local Ltac post_t_step :=
     match goal with
     | _ => reflexivity
+    | _ => progress subst
     | _ => progress unfold Let_In
     | _ => progress autorewrite with zsimplify_const
     | [ |- fst ?x = (?a <=? ?b) :> bool ]
@@ -71,13 +72,16 @@ Section fancy_machine_p256_montgomery_foundation.
   Local Ltac post_t := repeat post_t_step.
   Local Ltac t := pre_t; post_t.
 
-  Global Instance ZLikeProperties_of_ArchitectureBoundedOps
+  Global Instance ZLikeProperties_of_ArchitectureBoundedOps_Factored
          {arith : fancy_machine.arithmetic ops}
+         ldi_modulus ldi_0
+         (Hldi_modulus : ldi_modulus = ldi modulus)
+         (Hldi_0 : ldi_0 = ldi 0)
          (modulus_in_range : 0 <= modulus < 2^n)
          (smaller_bound_exp : Z)
          (smaller_bound_smaller : 0 <= smaller_bound_exp <= n)
          (n_pos : 0 < n)
-    : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps ops modulus smaller_bound_exp)
+    : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps_Factored ops modulus smaller_bound_exp ldi_modulus ldi_0)
     := { large_valid v := True;
          medium_valid v := 0 <= decode_large v < 2^n * 2^smaller_bound_exp;
          small_valid v := True }.
@@ -109,4 +113,13 @@ Section fancy_machine_p256_montgomery_foundation.
     { abstract t. }
     { abstract t. }
   Defined.
+
+  Global Instance ZLikeProperties_of_ArchitectureBoundedOps
+         {arith : fancy_machine.arithmetic ops}
+         (modulus_in_range : 0 <= modulus < 2^n)
+         (smaller_bound_exp : Z)
+         (smaller_bound_smaller : 0 <= smaller_bound_exp <= n)
+         (n_pos : 0 < n)
+    : ZLikeProperties (ZLikeOps_of_ArchitectureBoundedOps ops modulus smaller_bound_exp)
+    := ZLikeProperties_of_ArchitectureBoundedOps_Factored _ _ eq_refl eq_refl modulus_in_range _ smaller_bound_smaller n_pos.
 End fancy_machine_p256_montgomery_foundation.