Fix up Montgomery

4 files changed, 287 insertions, 430 deletions

diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v
index 8d3319519..fc9ed5d45 100644
--- a/src/Fancy/Barrett256.v
+++ b/src/Fancy/Barrett256.v
@@ -46,7 +46,6 @@ Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZRange.BasicLemmas.
 Require Import Crypto.Util.ZRange.Show.
 Require Import Crypto.Arithmetic.
-Require Import Crypto.Fancy.PrintingNotations.
 Require Import Crypto.Fancy.Prod.
 Require Import Crypto.Fancy.Spec.
 Require Import Crypto.Fancy.Translation.
@@ -86,10 +85,9 @@ Local Coercion Z.of_nat : nat >-> Z.
 Local Coercion QArith_base.inject_Z : Z >-> Q.
 
 Import Spec.Fancy.
-Import ProdEquiv.
+Import LanguageWf.Compilers.
 
 Module Barrett256.
-  Import LanguageWf.Compilers.
 
   Definition M := Eval lazy in (2^256-2^224+2^192+2^96-1).
   Definition machine_wordsize := 256.
@@ -115,44 +113,6 @@ Module Barrett256.
           end; lazy; try split; congruence.
   Qed.
 
-  (*
-  (* TODO: delete if unneeded *)
-  (* Note: If this is not factored out, then for some reason Qed takes forever in barrett_red256_correct_full. *)
-  Lemma barrett_red256_correct_proj2 :
-    forall x y,
-      ZRange.type.option.is_bounded_by
-        (t:=base.type.prod base.type.Z base.type.Z)
-        (Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange, Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange)
-        (x, y) = true ->
-      type.app_curried
-          (expr.Interp (@ident.gen_interp ident.cast_outside_of_range)
-             barrett_red256) (x, (y, tt)) =
-        BarrettReduction.barrett_reduce machine_wordsize M
-             ((2 ^ (2 * machine_wordsize) / M)
-              mod 2 ^ machine_wordsize) 2 2 x y.
-  Proof.
-    intros.
-    destruct ((proj1 barrett_red256_correct) (x, (y, tt)) (x, (y, tt))).
-    { cbn; tauto. }
-    { cbn in *. rewrite andb_true_r. auto. }
-    { auto. }
-  Qed.
-  Lemma barrett_red256_correct_proj2' :
-    forall x y,
-      ZRange.type.option.is_bounded_by
-        (t:=base.type.prod base.type.Z base.type.Z)
-        (Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange, Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange)
-        (x, y) = true ->
-      expr.Interp (@ident.interp) barrett_red256 x y =
-        BarrettReduction.barrett_reduce machine_wordsize M
-             ((2 ^ (2 * machine_wordsize) / M)
-              mod 2 ^ machine_wordsize) 2 2 x y.
-  Proof.
-    intros.
-    erewrite <-barrett_red256_correct_proj2 by assumption.
-    unfold type.app_curried. exact eq_refl.
-  Qed.
-*)
   Strategy -100 [type.app_curried].
   Local Arguments is_bounded_by_bool / .
   Lemma barrett_red256_correct_full  :
@@ -302,14 +262,52 @@ Module Barrett256.
     | H : ?a = ?b mod ?c |- 0 <= ?a < ?c => rewrite H; apply Z.mod_pos_bound; omega
     | _ => assumption
     end.
+  Local Ltac results_equiv :=
+    match goal with
+      |- ?lhs = ?rhs =>
+      match lhs with
+        context [spec ?li ?largs ?lcc] =>
+        match rhs with
+          context [spec ?ri ?rargs ?rcc] =>
+          replace (spec li largs lcc) with (spec ri rargs rcc)
+        end
+      end
+    end.
+  Local Ltac simplify_cc :=
+    match goal with
+      |- context [CC.update ?to_write ?result ?cc_spec ?old_state] =>
+      let e := eval cbv -[spec cc_spec CC.cc_l CC.cc_m CC.cc_z CC.cc_c] in
+      (CC.update to_write result cc_spec old_state) in
+          change (CC.update to_write result cc_spec old_state) with e
+    end.
+  Ltac remember_single_result :=
+    match goal with |- context [(Fancy.spec ?i ?args ?cc) mod ?w] =>
+                    let x := fresh "x" in
+                    let y := fresh "y" in
+                    let Heqx := fresh "Heqx" in
+                    remember (Fancy.spec i args cc) as x eqn:Heqx;
+                    remember (x mod w) as y
+    end.
+  Local Ltac step :=
+    match goal with
+      |- interp _ _ _ (Instr ?i ?rd1 ?args1 ?cont1) ?cc1 ?ctx1 =
+         interp _ _ _ (Instr ?i ?rd2 ?args2 ?cont2) ?cc2 ?ctx2 =>
+      rewrite (interp_step _ _ i rd1 args1 cont1);
+      rewrite (interp_step _ _ i rd2 args2 cont2)
+    end;
+    cbn - [Fancy.interp Fancy.spec cc_spec];
+    repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence;
+    results_equiv; [ remember_single_result; repeat simplify_cc | try reflexivity ].
 
+  Local Notation interp := (interp reg_eqb wordmax cc_spec).
   Lemma barrett_red256_alloc_equivalent errorP errorR cc_start_state start_context :
     forall x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5 extra_reg,
       NoDup [x; xHigh; RegMuLow; scratchp1; scratchp2; scratchp3; scratchp4; scratchp5; extra_reg; RegMod; RegZero] ->
       0 <= start_context x < 2^machine_wordsize ->
       0 <= start_context xHigh < 2^machine_wordsize ->
       0 <= start_context RegMuLow < 2^machine_wordsize ->
-      ProdEquiv.interp256 (barrett_red256_alloc r0 r1 r30 errorP errorR) cc_start_state
+      interp
+        (barrett_red256_alloc r0 r1 r30 errorP errorR) cc_start_state
                           (fun r => if reg_eqb r r0
                                     then start_context x
                                     else if reg_eqb r r1
@@ -317,7 +315,7 @@ Module Barrett256.
                                          else if reg_eqb r r30
                                               then start_context RegMuLow
                                               else start_context r)
-    = ProdEquiv.interp256 (Prod.MulMod x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5) cc_start_state start_context.
+    = interp (Prod.MulMod x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5) cc_start_state start_context.
   Proof.
     intros.
     let r := eval compute in (2^machine_wordsize) in
@@ -332,42 +330,13 @@ Module Barrett256.
            | H : ~ False |- _ => clear H
            end.
 
-    step_both_sides.
+    step.
+    step.
 
     (* TODO: To prove equivalence between these two, we need to either relocate the RSHI instructions so they're in the same places or use instruction commutativity to push them down. *)
 
   Admitted.
 
-  Local Ltac results_equiv :=
-    match goal with
-      |- ?lhs = ?rhs =>
-      match lhs with
-        context [spec ?li ?largs ?lcc] =>
-        match rhs with
-          context [spec ?ri ?rargs ?rcc] =>
-          replace (spec li largs lcc) with (spec ri rargs rcc)
-        end
-      end
-    end.
-  Local Ltac simplify_cc :=
-    match goal with
-      |- context [CC.update ?to_write ?result ?cc_spec ?old_state] =>
-      let e := eval cbv -[spec cc_spec CC.cc_l CC.cc_m CC.cc_z CC.cc_c] in
-      (CC.update to_write result cc_spec old_state) in
-          change (CC.update to_write result cc_spec old_state) with e
-    end.
-
-  Local Ltac step :=
-    match goal with
-      |- interp _ _ _ (Instr ?i ?rd1 ?args1 ?cont1) ?cc1 ?ctx1 =
-         interp _ _ _ (Instr ?i ?rd2 ?args2 ?cont2) ?cc2 ?ctx2 =>
-      rewrite (interp_step _ _ i rd1 args1 cont1);
-      rewrite (interp_step _ _ i rd2 args2 cont2)
-    end;
-    cbn - [Fancy.interp Fancy.spec cc_spec];
-    repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence;
-    results_equiv; [ remember_single_result; repeat simplify_cc | try reflexivity ].
-
   Lemma prod_barrett_red256_correct :
     forall (cc_start_state : Fancy.CC.state) (* starting carry flags *)
            (start_context : register -> Z)   (* starting register values *)
@@ -380,7 +349,7 @@ Module Barrett256.
              start_context RegZero = 0 ->
              cc_start_state.(Fancy.CC.cc_m) = cc_spec CC.M (start_context xHigh) ->
              let X := start_context x + 2^machine_wordsize * start_context xHigh in
-             ProdEquiv.interp256 (Prod.MulMod x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5) cc_start_state start_context = X mod M.
+             interp (Prod.MulMod x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5) cc_start_state start_context = X mod M.
   Proof.
     intros. subst X.
     assert (0 <= start_context xHigh < 2^machine_wordsize) by (cbv [M] in *; cbn; omega).
@@ -391,7 +360,6 @@ Module Barrett256.
     rewrite <-barrett_red256_alloc_equivalent with (errorR := RegZero) (errorP := 1%positive) (extra_reg:=extra_reg)
       by (auto; cbv [M muLow] in *; cbn; auto with omega).
 
-    cbv [interp256 Translation.wordmax].
     match goal with
       |- context [make_cc ?last_wrote ?ctx ?carry] =>
       let e := fresh in
diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v
index 7e635e96f..d7b00ceb9 100644
--- a/src/Fancy/Montgomery256.v
+++ b/src/Fancy/Montgomery256.v
@@ -87,8 +87,9 @@ Local Coercion QArith_base.inject_Z : Z >-> Q.
 
 Import UnsaturatedSolinas.
 
-(* TODO : once Barrett is updated & working, fix Montgomery to match *)
-(*
+Import Spec.Fancy.
+Import LanguageWf.Compilers.
+
 Module Montgomery256.
 
   Definition N := Eval lazy in (2^256-2^224+2^192+2^96-1).
@@ -105,7 +106,7 @@ Module Montgomery256.
   Lemma montred'_correct_specialized R' (R'_correct : Z.equiv_modulo N (R * R') 1) :
     forall (lo hi : Z),
       0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N ->
-      MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2 (lo, hi) = ((lo + R * hi) * R') mod N.
+      MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2 lo hi = ((lo + R * hi) * R') mod N.
   Proof.
     intros.
     apply MontgomeryReduction.montred'_correct with (T:=lo + R * hi) (R':=R');
@@ -116,34 +117,18 @@ Module Montgomery256.
           end; lazy; try split; congruence.
   Qed.
 
-  (*
-  (* Note: If this is not factored out, then for some reason Qed takes forever in montred256_correct_full. *)
-  Lemma montred256_correct_proj2 :
-    forall xy : type.interp (type.prod type.Z type.Z),
-      ZRange.type.option.is_bounded_by
-        (t:=type.prod type.Z type.Z)
-        (Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange, Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange)
-        xy = true ->
-       expr.Interp (@ident.interp) montred256 xy = app_curried (t:=type.arrow (type.prod type.Z type.Z) type.Z) (MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2) xy.
-  Proof. intros; destruct (montred256_correct xy); assumption. Qed.
-  Lemma montred256_correct_proj2' :
-    forall xy : type.interp (type.prod type.Z type.Z),
-      ZRange.type.option.is_bounded_by
-        (t:=type.prod type.Z type.Z)
-        (Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange, Some r[0 ~> 2 ^ machine_wordsize - 1]%zrange)
-        xy = true ->
-       expr.Interp (@ident.interp) montred256 xy = MontgomeryReduction.montred' N R N' (Z.log2 R) 2 2 xy.
-  Proof. intros; rewrite montred256_correct_proj2 by assumption; unfold app_curried; exact eq_refl. Qed.
-   *)
+  Strategy -100 [type.app_curried].
   Local Arguments is_bounded_by_bool / .
   Lemma montred256_correct_full  R' (R'_correct : Z.equiv_modulo N (R * R') 1) :
     forall (lo hi : Z),
-      0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N ->
-      PreFancy.Interp 256 montred256 (lo, hi) = ((lo + R * hi) * R') mod N.
+      0 <= lo < R ->
+      0 <= hi < R ->
+      0 <= lo + R * hi < R * N ->
+      expr.Interp (@ident.interp) montred256 lo hi = ((lo + R * hi) * R') mod N.
   Proof.
     intros.
     rewrite <-montred'_correct_specialized by assumption.
-    destruct (proj1 montred256_correct ((lo, hi), tt) ((lo, hi), tt)) as [H2 H3].
+    destruct (proj1 montred256_correct (lo, (hi, tt)) (lo, (hi, tt))) as [H2 H3].
     { repeat split. }
     { cbn -[Z.pow].
       rewrite !andb_true_iff.
@@ -152,102 +137,114 @@ Module Montgomery256.
       generalize MontgomeryReduction.montred'; vm_compute; reflexivity. }
   Qed.
 
-  (*
-  (* TODO : maybe move these ok_expr tactics somewhere else *)
-  Ltac ok_expr_step' :=
-    match goal with
-    | _ => assumption
-    | |- _ <= _ <= _ \/ @eq zrange _ _ =>
-      right; lazy; try split; congruence
-    | |- _ <= _ <= _ \/ @eq zrange _ _ =>
-      left; lazy; try split; congruence
-    | |- lower r[0~>_]%zrange = 0 => reflexivity
-    | |- context [PreFancy.ok_ident] => constructor
-    | |- context [PreFancy.ok_scalar] => constructor; try omega
-    | |- context [PreFancy.is_halved] => eapply PreFancy.is_halved_constant; [lazy; reflexivity | ]
-    | |- context [PreFancy.is_halved] => constructor
-    | |- context [PreFancy.in_word_range] => lazy; reflexivity
-    | |- context [PreFancy.in_flag_range] => lazy; reflexivity
-    | |- context [PreFancy.get_range] =>
-      cbn [PreFancy.get_range lower upper fst snd ZRange.map]
-    | x : type.interp (type.prod _ _) |- _ => destruct x
-    | |- (_ <=? _)%zrange = true =>
-      match goal with
-      | |- context [PreFancy.get_range_var] =>
-        cbv [is_tighter_than_bool PreFancy.has_range fst snd upper lower R N] in *; cbn;
-        apply andb_true_iff; split; apply Z.leb_le
-      | _ => lazy
-      end; omega || reflexivity
-    | |- @eq zrange _ _ => lazy; reflexivity
-    | |- _ <= _ => cbv [machine_wordsize]; omega
-    | |- _ <= _ <= _ => cbv [machine_wordsize]; omega
-    end; intros.
-
-  (* TODO : maybe move these ok_expr tactics somewhere else *)
-  Ltac ok_expr_step :=
-    match goal with
-    | |- context [PreFancy.ok_expr] => constructor; cbn [fst snd]; repeat ok_expr_step'
-    end; intros; cbn [Nat.max].*)
-
-  (*
-  Lemma montred256_prefancy_correct :
-    forall (lo hi : Z),
-      0 <= lo < R -> 0 <= hi < R -> 0 <= lo + R * hi < R * N ->
-      @PreFancy.interp machine_wordsize base.type.Z (montred256 _ @ (##lo,##hi)) = ((lo + R * hi) * R') mod N.
-  Proof.
-    intros.
-
-    rewrite montred256_prefancy_eq; cbv [montred256_prefancy'].
-    erewrite PreFancy.of_Expr_correct.
-    { apply montred256_correct_full; try assumption; reflexivity. }
-    { reflexivity. }
-    { lazy; reflexivity. }
-    { lazy; reflexivity. }
-    { repeat constructor. }
-    { cbv [In N N']; intros; intuition; subst; cbv; congruence. }
-    { assert (340282366920938463463374607431768211455 * 2 ^ 128 <= 2 ^ machine_wordsize - 1) as shiftl_128_ok by (lazy; congruence).
-      repeat (ok_expr_step; [ ]).
-      ok_expr_step.
-      lazy; congruence.
-      constructor.
-      constructor. }
-    { lazy. omega. }
-   Qed.
-*)
-
-  Definition montred256_fancy' (lo hi RegMod RegPInv RegZero error : positive) :=
-    Fancy.of_Expr 3%positive
-                  (fun z => if z =? N then Some RegMod else if z =? N' then Some RegPInv else if z =? 0 then Some RegZero else None)
-                  [N;N']
-                  montred256
-                  ((lo, hi)%positive, tt)
-                  error.
+  Definition montred256_fancy' (RegMod RegPInv RegZero lo hi error : positive) :=
+    of_Expr 6%positive
+            (make_consts [(RegMod, N); (RegZero, 0); (RegPInv, N')])
+            montred256
+            (lo, (hi, tt))
+            error.
   Derive montred256_fancy
          SuchThat (forall RegMod RegPInv RegZero,
                       montred256_fancy RegMod RegPInv RegZero = montred256_fancy' RegMod RegPInv RegZero)
          As montred256_fancy_eq.
   Proof.
     intros.
+    cbv [montred256_fancy'].
     lazy - [Fancy.ADD Fancy.ADDC Fancy.SUB
                       Fancy.MUL128LL Fancy.MUL128LU Fancy.MUL128UL Fancy.MUL128UU
                       Fancy.RSHI Fancy.SELC Fancy.SELM Fancy.SELL Fancy.ADDM].
     reflexivity.
   Qed.
 
+  (* TODO: these tactics are duplicated; move them elsewhere (probably translation *)
+  Local Ltac wf_subgoal :=
+    repeat match goal with
+           | _ => progress cbn [fst snd]
+           | |- LanguageWf.Compilers.expr.wf _ _ _ =>
+             econstructor; try solve [econstructor]; [ ]
+           | |- LanguageWf.Compilers.expr.wf _ _ _ =>
+             solve [econstructor]
+           | |- In _ _ => auto 50 using in_eq, in_cons
+           end.
+  Local Ltac valid_expr_subgoal :=
+    repeat match goal with
+           | _ => progress intros
+           | |- context [valid_ident] => econstructor
+           | |- context[valid_scalar] => econstructor
+           | |- context [valid_carry] => econstructor
+           | _ => reflexivity
+           | |- _ <> None => cbn; congruence
+           | |- of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto]
+           end.
+
+  Lemma montred256_fancy_correct :
+    forall lo hi error,
+      0 <= lo < R ->
+      0 <= hi < R ->
+      0 <= lo + R * hi < R * N ->
+      let RegZero := 1%positive in
+      let RegMod := 2%positive in
+      let RegPInv := 3%positive in
+      let RegHi := 4%positive in
+      let RegLo := 5%positive in
+      let consts_list := [(RegMod, N); (RegZero, 0); (RegPInv, N')] in
+      let arg_list := [(RegHi, hi); (RegLo, lo)] in
+      let ctx := make_ctx (consts_list ++ arg_list) in
+      let carry_flag := false in
+      let last_wrote := (fun x : Fancy.CC.code => RegZero) in
+      let cc := make_cc last_wrote ctx carry_flag in
+      interp Pos.eqb wordmax Fancy.cc_spec (montred256_fancy RegMod RegPInv RegZero RegLo RegHi error) cc ctx = ((lo + R * hi) * R') mod N.
+  Proof.
+    intros.
+    rewrite montred256_fancy_eq.
+    cbv [montred256_fancy'].
+    rewrite <-montred256_correct_full by (auto; reflexivity).
+    eapply of_Expr_correct with (x2 := (lo, (hi, tt))).
+    { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
+      intuition; Prod.inversion_prod; subst; cbv. break_innermost_match; congruence. }
+    { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
+      intuition; Prod.inversion_prod; subst; cbv; congruence. }
+    { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo. tauto. }
+    { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
+      intuition; Prod.inversion_prod; subst; cbv; congruence. }
+    { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
+      match goal with |- context [_ mod ?m] => change m with (2 ^ machine_wordsize) end.
+      intuition; Prod.inversion_prod; subst; apply Z.mod_small; cbv; try split; congruence. }
+    { cbn; intros; subst RegZero RegMod RegPInv RegHi RegLo.
+      match goal with |- context [_ mod ?m] => change m with (2 ^ machine_wordsize) end.
+      assert (R <= 2 ^ machine_wordsize) by (cbv; congruence).
+      intuition; Prod.inversion_prod; subst; apply Z.mod_small; omega. }
+    { cbn.
+      repeat match goal with
+             | _ => apply expr.WfLetIn
+             | _ => progress wf_subgoal 
+             | _ => econstructor
+             end. }
+    { cbn. cbv [N' N].
+      repeat (econstructor; [ solve [valid_expr_subgoal] | intros ]).
+      econstructor. valid_expr_subgoal. }
+    { cbn - [montred256]. cbv [id].
+      f_equal.
+      (* TODO(jgross): switch out casts *)
+      (* might need to use CheckCasts.interp_eqv_without_casts? *)
+      replace (@ident.gen_interp cast_oor) with (@ident.interp) by admit.
+      reflexivity. }
+  Admitted.
+
   Import Fancy.Registers.
 
   Definition montred256_alloc' lo hi RegPInv :=
     fun errorP errorR =>
-    Fancy.allocate register
-                   positive Pos.eqb
-                   errorR
-                   (montred256_fancy 1000%positive 1001%positive 1002%positive 1003%positive 1004%positive errorP)
-                   [r2;r3;r4;r5;r6;r7;r8;r9;r10;r11;r12;r13;r14;r15;r16;r17;r18;r19;r20]
-                   (fun n => if n =? 1000 then lo
-                             else if n =? 1001 then hi
-                                  else if n =? 1002 then RegMod
-                                       else if n =? 1003 then RegPInv
-                                            else if n =? 1004 then RegZero
+      allocate register
+               positive Pos.eqb
+               errorR
+               (montred256_fancy 1000%positive 1001%positive 1002%positive 1003%positive 1004%positive errorP)
+               [r2;r3;r4;r5;r6;r7;r8;r9;r10;r11;r12;r13;r14;r15;r16;r17;r18;r19;r20]
+               (fun n => if n =? 1000 then RegMod
+                         else if n =? 1001 then RegPInv
+                              else if n =? 1002 then RegZero
+                                   else if n =? 1003 then lo
+                                        else if n =? 1004 then hi
                                                  else errorR).
   Derive montred256_alloc
          SuchThat (montred256_alloc = montred256_alloc')
@@ -259,21 +256,58 @@ Module Montgomery256.
     reflexivity.
   Qed.
 
-  Import ProdEquiv.
-
+  (* TODO: also factor out these tactics *)
   Local Ltac solve_bounds :=
     match goal with
     | H : ?a = ?b mod ?c |- 0 <= ?a < ?c => rewrite H; apply Z.mod_pos_bound; omega
     | _ => assumption
     end.
-
+  Local Ltac results_equiv :=
+    match goal with
+      |- ?lhs = ?rhs =>
+      match lhs with
+        context [spec ?li ?largs ?lcc] =>
+        match rhs with
+          context [spec ?ri ?rargs ?rcc] =>
+          replace (spec li largs lcc) with (spec ri rargs rcc)
+        end
+      end
+    end.
+  Local Ltac simplify_cc :=
+    match goal with
+      |- context [CC.update ?to_write ?result ?cc_spec ?old_state] =>
+      let e := eval cbv -[spec cc_spec CC.cc_l CC.cc_m CC.cc_z CC.cc_c] in
+      (CC.update to_write result cc_spec old_state) in
+          change (CC.update to_write result cc_spec old_state) with e
+    end.
+  Ltac remember_single_result :=
+    match goal with |- context [(Fancy.spec ?i ?args ?cc) mod ?w] =>
+                    let x := fresh "x" in
+                    let y := fresh "y" in
+                    let Heqx := fresh "Heqx" in
+                    remember (Fancy.spec i args cc) as x eqn:Heqx;
+                    remember (x mod w) as y
+    end.
+  Local Ltac step :=
+    match goal with
+      |- interp _ _ _ (Instr ?i ?rd1 ?args1 ?cont1) ?cc1 ?ctx1 =
+         interp _ _ _ (Instr ?i ?rd2 ?args2 ?cont2) ?cc2 ?ctx2 =>
+      rewrite (interp_step _ _ i rd1 args1 cont1);
+      rewrite (interp_step _ _ i rd2 args2 cont2)
+    end;
+    cbn - [Fancy.interp Fancy.spec cc_spec];
+    repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence;
+    results_equiv; [ remember_single_result; repeat simplify_cc | try reflexivity ].
+
+  Local Notation interp := (interp reg_eqb wordmax cc_spec).
   Lemma montred256_alloc_equivalent errorP errorR cc_start_state start_context :
     forall lo hi y t1 t2 scratch RegPInv extra_reg,
       NoDup [lo; hi; y; t1; t2; scratch; RegPInv; extra_reg; RegMod; RegZero] ->
       0 <= start_context lo < R ->
       0 <= start_context hi < R ->
       0 <= start_context RegPInv < R ->
-      ProdEquiv.interp256 (montred256_alloc r0 r1 r30 errorP errorR) cc_start_state
+      interp
+        (montred256_alloc r0 r1 r30 errorP errorR) cc_start_state
                           (fun r => if reg_eqb r r0
                                     then start_context lo
                                     else if reg_eqb r r1
@@ -281,7 +315,7 @@ Module Montgomery256.
                                          else if reg_eqb r r30
                                               then start_context RegPInv
                                               else start_context r)
-    = ProdEquiv.interp256 (Prod.MontRed256 lo hi y t1 t2 scratch RegPInv) cc_start_state start_context.
+    = interp (Prod.MontRed256 lo hi y t1 t2 scratch RegPInv) cc_start_state start_context.
   Proof.
     intros. cbv [R] in *.
     cbv [Prod.MontRed256 montred256_alloc].
@@ -294,95 +328,33 @@ Module Montgomery256.
            | H : ~ False |- _ => clear H
            end.
 
-    rewrite ProdEquiv.interp_Mul256 with (tmp2:=extra_reg) by (congruence || push_value_unused).
+    rewrite interp_Mul256 with (tmp2:=extra_reg) by (congruence || push_value_unused).
 
-    rewrite mullh_mulhl. step_both_sides.
-    rewrite mullh_mulhl. step_both_sides.
-    (*
-    step_both_sides.
-    step_both_sides.
+    rewrite mullh_mulhl.
+    step.
+    rewrite mullh_mulhl.
+    step. step. step. step.
 
-    rewrite ProdEquiv.interp_Mul256x256 with (tmp2:=extra_reg) by (congruence || push_value_unused).
 
-    rewrite mulll_comm. step_both_sides.
-    step_both_sides.
-    step_both_sides.
-    rewrite mulhh_comm. step_both_sides.
-    step_both_sides.
-    step_both_sides.
-    step_both_sides.
-    step_both_sides.
+    rewrite interp_Mul256x256 with (tmp2:=extra_reg) by
+        (match goal with
+         | |- _ <> _ => congruence
+         | _ => push_value_unused
+         end).
 
-
-    rewrite add_comm by (cbn; solve_bounds). step_both_sides.
-    rewrite addc_comm by (cbn; solve_bounds). step_both_sides.
-    step_both_sides.
-    step_both_sides.
-    step_both_sides.
+    rewrite mulll_comm.
+    step. step. step.
+    rewrite mulhh_comm.
+    step. step. step. step. step.
+    rewrite add_comm by (cbn; solve_bounds).
+    step.
+    rewrite addc_comm by (cbn; solve_bounds).
+    step. step. step. step.
 
     cbn; repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence.
-    reflexivity.*)
-  Admitted.
-
-  Import Fancy_PreFancy_Equiv.
-
-  Definition interp_equivZZ_256 {s} :=
-    @interp_equivZZ s 256 ltac:(cbv; congruence) 115792089237316195423570985008687907853269984665640564039457584007913129639935 ltac:(reflexivity).
-  Definition interp_equivZ_256 {s} :=
-    @interp_equivZ s 256 115792089237316195423570985008687907853269984665640564039457584007913129639935 ltac:(lia) ltac:(reflexivity).
-
-  Local Ltac simplify_op_equiv start_ctx :=
-    cbn - [Fancy.spec ident.gen_interp Fancy.cc_spec];
-    repeat match goal with H : start_ctx _ = _ |- _ => rewrite H end;
-    cbv - [
-      Z.add_with_get_carry_full
-        Z.add_get_carry_full Z.sub_get_borrow_full
-        Z.le Z.ltb Z.leb Z.geb Z.eqb Z.land Z.shiftr Z.shiftl
-        Z.add Z.mul Z.div Z.sub Z.modulo Z.testbit Z.pow Z.ones
-        fst snd]; cbn [fst snd];
-    try (replace (2 ^ (256 / 2) - 1) with (Z.ones 128) by reflexivity; rewrite !Z.land_ones by omega);
-    autorewrite with to_div_mod; rewrite ?Z.mod_mod, <-?Z.testbit_spec' by omega;
-    repeat match goal with
-           | H : 0 <= ?x < ?m |- context [?x mod ?m] => rewrite (Z.mod_small x m) by apply H
-           | |- context [?x <? 0] => rewrite (proj2 (Z.ltb_ge x 0)) by (break_match; Z.zero_bounds)
-           | _ => rewrite Z.mod_small with (b:=2) by (break_match; omega)
-           | |- context [ (if Z.testbit ?a ?n then 1 else 0) + ?b + ?c] =>
-             replace ((if Z.testbit a n then 1 else 0) + b + c) with (b + c + (if Z.testbit a n then 1 else 0)) by ring
-           end.
-
-  Local Ltac solve_nonneg ctx :=
-    match goal with x := (Fancy.spec _ _ _) |- _ => subst x end;
-    simplify_op_equiv ctx; Z.zero_bounds.
-
-  Local Ltac generalize_result :=
-    let v := fresh "v" in intro v; generalize v; clear v; intro v.
-
-  Local Ltac generalize_result_nonneg ctx :=
-    let v := fresh "v" in
-    let v_nonneg := fresh "v_nonneg" in
-    intro v; assert (0 <= v) as v_nonneg; [solve_nonneg ctx |generalize v v_nonneg; clear v v_nonneg; intros v v_nonneg].
-
-  Local Ltac step_abs :=
-    match goal with
-    | [ |- context G[expr.interp ?ident_interp (expr.Abs ?f) ?x] ]
-      => let G' := context G[expr.interp ident_interp (f x)] in
-         change G'; cbv beta
-    end.
-  Local Ltac step ctx :=
-    repeat step_abs;
-    match goal with
-    | |- Fancy.interp _ _ _ (Fancy.Instr (Fancy.ADD _) _ _ (Fancy.Instr (Fancy.ADDC _) _ _ _)) _ _ = _ =>
-      apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result_nonneg ctx]
-    | [ |- _ = expr.interp _ (PreFancy.LetInAppIdentZ _ _ _ _ _ _) ]
-      => apply interp_equivZ_256; [simplify_op_equiv ctx | generalize_result]
-    | [ |- _ = expr.interp _ (PreFancy.LetInAppIdentZZ _ _ _ _ _ _) ]
-      => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result]
-    end.
-
-  Local Ltac break_ifs :=
-    repeat (break_innermost_match_step; Z.ltb_to_lt; try (exfalso; omega); []).
+    reflexivity.
+  Qed.
 
-  Local Opaque PreFancy.interp_cast_mod.
 
   Lemma prod_montred256_correct :
     forall (cc_start_state : Fancy.CC.state) (* starting carry flags can be anything *)
@@ -396,113 +368,28 @@ Module Montgomery256.
       (0 <= start_context hi < R) -> (* high half of the input is in bounds (R=2^256) *)
       let x := (start_context lo) + R * (start_context hi) in (* x is the input (split into two registers) *)
       (0 <= x < R * N) -> (* input precondition *)
-      (ProdEquiv.interp256 (Prod.MontRed256 lo hi y t1 t2 scratch RegPInv) cc_start_state start_context = (x * R') mod N).
+      (interp (Prod.MontRed256 lo hi y t1 t2 scratch RegPInv) cc_start_state start_context = (x * R') mod N).
   Proof.
-    intros. subst x. cbv [N R N'] in *.
-    rewrite <-montred256_correct_full by (auto; vm_compute; reflexivity).
+    intros. subst x.
+    erewrite <-montred256_fancy_correct with (error:=100000%positive) by eauto.
     rewrite <-montred256_alloc_equivalent with (errorR := RegZero) (errorP := 1%positive) (extra_reg:=extra_reg)
-      by (cbv [R]; auto with omega).
-    cbv [ProdEquiv.interp256].
-    cbv [montred256_alloc montred256 expr.Interp].
-
-    (*step start_context; [ break_ifs; reflexivity | ].
-    step start_context; [ break_ifs; reflexivity | ].
-    step start_context; [ break_ifs; reflexivity | ].*)
-    (*step start_context; [ break_ifs; reflexivity | ].
-    step start_context; [ break_ifs; reflexivity | break_ifs; reflexivity | ].
-    step start_context; [ break_ifs; reflexivity | break_ifs; reflexivity | ].
-    step start_context; [ reflexivity | ].
-    step start_context; [ reflexivity | ].
-    step start_context; [ reflexivity | ].
-    step start_context; [ reflexivity | ].
-    step start_context; [ reflexivity | reflexivity | ].
-    step start_context; [ reflexivity | reflexivity | ].
-    step start_context; [ reflexivity | reflexivity | ].
-    step start_context; [ reflexivity | reflexivity | ].
+      by (cbv [R N N'] in *; auto with omega).
 
-    step start_context; [ reflexivity | reflexivity | ].
-    step start_context; [ reflexivity | reflexivity | ].
-    step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ].
-    step start_context; [ reflexivity | | ].
-    {
-      let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity.
-      rewrite !Z.shiftl_0_r, !Z.mod_mod by omega.
-      apply Z.testbit_neg_eq_if;
-        let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity;
-        auto using Z.mod_pos_bound with omega. }
-    step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ].
+    (* TODO: factor out this tactic *)
+    match goal with
+      |- context [make_cc ?last_wrote ?ctx ?carry] =>
+      let e := fresh in
+      let He := fresh in
+      remember (make_cc last_wrote ctx carry) as e eqn:He;
+        cbv [make_ctx app make_cc] in He;
+        cbn [Pos.eqb] in He; autorewrite with zsimplify in He;
+          subst e
+    end.
+    cbv [montred256_alloc montred256_fancy].
+    repeat match goal with
+             H : context [start_context] |- _ =>
+             rewrite <-H end.
+    repeat step.
     reflexivity.
-     *)
-  Admitted.
-
-  Import PrintingNotations.
-  Set Printing Width 10000.
-
-  Print montred256.
-(*
-montred256 = fun var : type -> Type => (λ x : var (type.type_primitive type.Z * type.type_primitive type.Z)%ctype,
-    expr_let x0 := 79228162514264337593543950337 *₂₅₆ (uint128)(x₁ >> 128) in
-    expr_let x1 := 340282366841710300986003757985643364352 *₂₅₆ ((uint128)(x₁) & 340282366920938463463374607431768211455) in
-    expr_let x2 := 79228162514264337593543950337 *₂₅₆ ((uint128)(x₁) & 340282366920938463463374607431768211455) in
-    expr_let x3 := ADD_256 ((uint256)(((uint128)(x1) & 340282366920938463463374607431768211455) << 128), x2) in
-    expr_let x4 := ADD_256 ((uint256)(((uint128)(x0) & 340282366920938463463374607431768211455) << 128), x3₁) in
-    expr_let x5 := 79228162514264337593543950335 *₂₅₆ ((uint128)(x4₁) & 340282366920938463463374607431768211455) in
-    expr_let x6 := 79228162514264337593543950335 *₂₅₆ (uint128)(x4₁ >> 128) in
-    expr_let x7 := 340282366841710300967557013911933812736 *₂₅₆ ((uint128)(x4₁) & 340282366920938463463374607431768211455) in
-    expr_let x8 := 340282366841710300967557013911933812736 *₂₅₆ (uint128)(x4₁ >> 128) in
-    expr_let x9 := ADD_256 ((uint256)(((uint128)(x7) & 340282366920938463463374607431768211455) << 128), x5) in
-    expr_let x10 := ADDC_256 (x9₂, (uint128)(x7 >> 128), x8) in
-    expr_let x11 := ADD_256 ((uint256)(((uint128)(x6) & 340282366920938463463374607431768211455) << 128), x9₁) in
-    expr_let x12 := ADDC_256 (x11₂, (uint128)(x6 >> 128), x10₁) in
-    expr_let x13 := ADD_256 (x11₁, x₁) in
-    expr_let x14 := ADDC_256 (x13₂, x12₁, x₂) in
-    expr_let x15 := SELC (x14₂, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951) in
-    expr_let x16 := SUB_256 (x14₁, x15) in
-    ADDM (x16₁, 0, 115792089210356248762697446949407573530086143415290314195533631308867097853951))%expr
-     : Expr (type.uncurry (type.type_primitive type.Z * type.type_primitive type.Z -> type.type_primitive type.Z))
-*)
-
-  Import PreFancy.
-  Import PreFancy.Notations.
-  Local Notation "'RegMod'" := (expr.Ident (ident.Literal 115792089210356248762697446949407573530086143415290314195533631308867097853951)).
-  Local Notation "'RegPInv'" := (expr.Ident (ident.Literal 115792089210356248768974548684794254293921932838497980611635986753331132366849)).
-  Local Open Scope expr_scope.
-  Local Notation mulhl := (#(fancy_mulhl 256)).
-  Local Notation mulhh := (#(fancy_mulhh 256)).
-  Local Notation mulll := (#(fancy_mulll 256)).
-  Local Notation mullh := (#(fancy_mullh 256)).
-  Local Notation selc := (#(fancy_selc)).
-  Local Notation addm := (#(fancy_addm)).
-  Notation add n := (#(fancy_add 256 n)).
-  Notation addc n := (#(fancy_addc 256 n)).
-
-  Print montred256.
-  (*
-montred256 =
-fun var : type -> Type =>
-λ x : var (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%etype),
-mulhl@(x0, x₁, RegPInv);
-mullh@(x1, x₁, RegPInv);
-mulll@(x2, x₁, RegPInv);
-(add 128)@(x3, x2, Lower{x1});
-(add 128)@(x4, x3₁, Lower{x0});
-mulll@(x5, RegMod, x4₁);
-mullh@(x6, RegMod, x4₁);
-mulhl@(x7, RegMod, x4₁);
-mulhh@(x8, RegMod, x4₁);
-(add 128)@(x9, x5, Lower{x7});
-(addc (-128))@(x10, carry{$x9}, x8, x7);
-(add 128)@(x11, x9₁, Lower{x6});
-(addc (-128))@(x12, carry{$x11}, x10₁, x6);
-(add 0)@(x13, x11₁, x₁);
-(addc 0)@(x14, carry{$x13}, x12₁, x₂);
-selc@(x15, (carry{$x14}, RegZero), RegMod);
-#(fancy_sub 256 0)@(x16, x14₁, x15);
-addm@(x17, (x16₁, RegZero), RegMod);
-x17
-     : Expr
-         (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%etype ->
-          type.base (base.type.type_base base.type.Z))%ptype
-  *)
-
+  Qed.
 End Montgomery256.
diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v
index bba41fa62..52ee97e11 100644
--- a/src/Fancy/Prod.v
+++ b/src/Fancy/Prod.v
@@ -163,12 +163,53 @@ Section interp_proofs.
       [reflexivity|].
     intros; break_match; auto.
   Qed.
+  
+  Local Ltac prove_comm H :=
+    rewrite !interp_step; cbn - [Fancy.interp];
+    intros; rewrite H; try reflexivity.
+
+  Lemma mulll_comm rd x y cont cc ctx :
+    interp (Fancy.Instr Fancy.MUL128LL rd (x, y) cont) cc ctx =
+    interp (Fancy.Instr Fancy.MUL128LL rd (y, x) cont) cc ctx.
+  Proof. prove_comm Z.mul_comm. Qed.
+
+  Lemma mulhh_comm rd x y cont cc ctx :
+    interp (Fancy.Instr Fancy.MUL128UU rd (x, y) cont) cc ctx =
+    interp (Fancy.Instr Fancy.MUL128UU rd (y, x) cont) cc ctx.
+  Proof. prove_comm Z.mul_comm. Qed.
+
+  Lemma mullh_mulhl rd x y cont cc ctx :
+    interp (Fancy.Instr Fancy.MUL128LU rd (x, y) cont) cc ctx =
+    interp (Fancy.Instr Fancy.MUL128UL rd (y, x) cont) cc ctx.
+  Proof. prove_comm Z.mul_comm. Qed.
+
+  Lemma add_comm rd x y cont cc ctx :
+    0 <= ctx x < 2^256 ->
+    0 <= ctx y < 2^256 ->
+    interp (Fancy.Instr (Fancy.ADD 0) rd (x, y) cont) cc ctx =
+    interp (Fancy.Instr (Fancy.ADD 0) rd (y, x) cont) cc ctx.
+  Proof.
+    prove_comm Z.add_comm.
+    rewrite !(Z.mod_small (ctx _)) by omega.
+    reflexivity.
+  Qed.
+
+  Lemma addc_comm rd x y cont cc ctx :
+    0 <= ctx x < 2^256 ->
+    0 <= ctx y < 2^256 ->
+    interp (Fancy.Instr (Fancy.ADDC 0) rd (x, y) cont) cc ctx =
+    interp (Fancy.Instr (Fancy.ADDC 0) rd (y, x) cont) cc ctx.
+  Proof.
+    prove_comm (Z.add_comm (ctx x)).
+    rewrite !(Z.mod_small (ctx _)) by omega.
+    reflexivity.
+  Qed.
 End interp_proofs.
 
-Module ProdEquiv.
+Section ProdEquiv.
+  Context (wordmax : Z).
 
-  Definition wordmax := 2^256.
-  Definition interp256 := Fancy.interp reg_eqb (2^256) cc_spec.
+  Let interp256 := Fancy.interp reg_eqb wordmax cc_spec.
   Lemma cc_overwrite_full x1 x2 l1 cc :
     CC.update [CC.C; CC.M; CC.L; CC.Z] x2 cc_spec (CC.update l1 x1 cc_spec cc) = CC.update [CC.C; CC.M; CC.L; CC.Z] x2 cc_spec cc.
   Proof.
@@ -219,6 +260,7 @@ Module ProdEquiv.
     break_match; congruence.
   Qed.
 
+  (* TODO: these tactics seem redundant; see if they can be replaced by [step] and [remember_single_result] *)
   Ltac remember_results :=
     repeat match goal with |- context [(spec ?i ?args ?flags) mod ?w] =>
                     let x := fresh "x" in
@@ -311,57 +353,8 @@ Module ProdEquiv.
       lia. }
   Qed.
 
-  Local Ltac prove_comm H :=
-    cbv [interp256]; rewrite !interp_step; cbn - [Fancy.interp];
-    intros; rewrite H; try reflexivity.
-
-  Lemma mulll_comm rd x y cont cc ctx :
-    interp256 (Fancy.Instr Fancy.MUL128LL rd (x, y) cont) cc ctx =
-    interp256 (Fancy.Instr Fancy.MUL128LL rd (y, x) cont) cc ctx.
-  Proof. prove_comm Z.mul_comm. Qed.
-
-  Lemma mulhh_comm rd x y cont cc ctx :
-    interp256 (Fancy.Instr Fancy.MUL128UU rd (x, y) cont) cc ctx =
-    interp256 (Fancy.Instr Fancy.MUL128UU rd (y, x) cont) cc ctx.
-  Proof. prove_comm Z.mul_comm. Qed.
-
-  Lemma mullh_mulhl rd x y cont cc ctx :
-    interp256 (Fancy.Instr Fancy.MUL128LU rd (x, y) cont) cc ctx =
-    interp256 (Fancy.Instr Fancy.MUL128UL rd (y, x) cont) cc ctx.
-  Proof. prove_comm Z.mul_comm. Qed.
-
-  Lemma add_comm rd x y cont cc ctx :
-    0 <= ctx x < 2^256 ->
-    0 <= ctx y < 2^256 ->
-    interp256 (Fancy.Instr (Fancy.ADD 0) rd (x, y) cont) cc ctx =
-    interp256 (Fancy.Instr (Fancy.ADD 0) rd (y, x) cont) cc ctx.
-  Proof.
-    prove_comm Z.add_comm.
-    rewrite !(Z.mod_small (ctx _)) by (cbn in *; omega).
-    reflexivity.
-  Qed.
-
-  Lemma addc_comm rd x y cont cc ctx :
-    0 <= ctx x < 2^256 ->
-    0 <= ctx y < 2^256 ->
-    interp256 (Fancy.Instr (Fancy.ADDC 0) rd (x, y) cont) cc ctx =
-    interp256 (Fancy.Instr (Fancy.ADDC 0) rd (y, x) cont) cc ctx.
-  Proof.
-    intros;
-    prove_comm (Z.add_comm (ctx x)).
-    rewrite !(Z.mod_small (ctx _)) by (cbn in *; omega).
-    reflexivity.
-  Qed.
-
-  (* Tactics to help prove that something in Fancy is line-by-line equivalent to something in PreFancy *)
-  Ltac push_value_unused :=
-    repeat match goal with
-           | |- ~ In _ _ => cbn; intuition; congruence
-           | _ => apply ProdEquiv.value_unused_overwrite
-           | _ => apply ProdEquiv.value_unused_skip; [ | congruence | ]
-           | _ => apply ProdEquiv.value_unused_ret; congruence
-           end.
-
+  (*
+  (* TODO: remove these tactics *)
   Ltac remember_single_result :=
     match goal with |- context [(Fancy.spec ?i ?args ?cc) mod ?w] =>
                     let x := fresh "x" in
@@ -391,5 +384,13 @@ Module ProdEquiv.
                     | _ => idtac
                     end
     end.
+*)
 End ProdEquiv.
 
+Ltac push_value_unused :=
+  repeat match goal with
+         | |- ~ In _ _ => cbn; intuition; congruence
+         | _ => apply value_unused_overwrite
+         | _ => apply value_unused_skip; [ | congruence | ]
+         | _ => apply value_unused_ret; congruence
+         end.
\ No newline at end of file
diff --git a/src/Fancy/Translation.v b/src/Fancy/Translation.v
index 96817a8be..45c6421a5 100644
--- a/src/Fancy/Translation.v
+++ b/src/Fancy/Translation.v
@@ -14,6 +14,7 @@ Require Import Crypto.Algebra.SubsetoidRing.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ListUtil.FoldBool.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Prod.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
@@ -495,7 +496,7 @@ Section of_prefancy.
                   | exfalso; assumption
                   | progress inversion_sigma
                   | progress inversion_option
-                  | progress Prod.inversion_prod
+                  | progress inversion_prod
                   | progress LanguageInversion.Compilers.expr.inversion_expr
                   | progress LanguageInversion.Compilers.expr.invert_subst
                   | progress LanguageWf.Compilers.expr.inversion_wf_one_constr
@@ -591,7 +592,7 @@ Section of_prefancy.
                   | progress inversion_sigma
                   | progress inversion_option
                   | progress inversion_of_prefancy_ident
-                  | progress Prod.inversion_prod
+                  | progress inversion_prod
                   | progress cbv [id]
                   | progress cbn [eq_rect projT1 projT2 expr.interp ident.interp ident.gen_interp interp_base interp invert_expr.invert_Ident interp_if_Z option_map] in *
                   | progress LanguageInversion.Compilers.type_beq_to_eq
@@ -1108,7 +1109,7 @@ Section Proofs.
            | _ => progress break_match_hyps
            | _ => progress inversion_sigma
            | _ => progress inversion_option
-           | _ => progress Prod.inversion_prod
+           | _ => progress inversion_prod
            | _ => progress HProp.eliminate_hprop_eq
            | _ => progress Z.ltb_to_lt
            | _ => reflexivity