Replace the python script with Ltac code

We now rely on Ltac rather than python to generate the raw identifiers.

After     | File Name                                       | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------
22m05.90s | Total                                           | 21m51.87s || +0m14.03s | +1.07%
-----------------------------------------------------------------------------------------------
0m49.25s  | GENERATEDIdentifiersWithoutTypesProofs.vo       | 0m55.23s  || -0m05.97s | -10.82%
0m19.14s  | GENERATEDIdentifiersWithoutTypes.vo             | 0m13.35s  || +0m05.79s | +43.37%
0m36.52s  | ExtractionHaskell/saturated_solinas             | 0m32.60s  || +0m03.92s | +12.02%
0m24.00s  | SlowPrimeSynthesisExamples.vo                   | 0m27.22s  || -0m03.21s | -11.82%
0m08.55s  | ExtractionOCaml/saturated_solinas.ml            | 0m05.49s  || +0m03.06s | +55.73%
3m24.98s  | p384_32.c                                       | 3m22.52s  || +0m02.45s | +1.21%
1m03.78s  | ExtractionHaskell/word_by_word_montgomery       | 1m01.13s  || +0m02.64s | +4.33%
0m47.85s  | p521_32.c                                       | 0m45.77s  || +0m02.07s | +4.54%
1m42.64s  | Fancy/Barrett256.vo                             | 1m41.49s  || +0m01.14s | +1.13%
0m40.30s  | p521_64.c                                       | 0m42.20s  || -0m01.90s | -4.50%
0m18.02s  | p256_32.c                                       | 0m19.03s  || -0m01.01s | -5.30%
0m14.70s  | ExtractionOCaml/unsaturated_solinas             | 0m13.33s  || +0m01.36s | +10.27%
0m14.28s  | p434_64.c                                       | 0m15.39s  || -0m01.11s | -7.21%
0m09.82s  | p224_32.c                                       | 0m08.77s  || +0m01.05s | +11.97%
0m08.59s  | p384_64.c                                       | 0m07.36s  || +0m01.22s | +16.71%
0m05.18s  | ExtractionHaskell/saturated_solinas.hs          | 0m06.59s  || -0m01.41s | -21.39%
1m34.02s  | RewriterWf2.vo                                  | 1m34.23s  || -0m00.20s | -0.22%
0m56.16s  | Rewriter/ToFancyWithCasts.vo                    | 0m55.41s  || +0m00.75s | +1.35%
0m45.85s  | Rewriter/NBE.vo                                 | 0m45.23s  || +0m00.62s | +1.37%
0m44.51s  | Rewriter/ArithWithCasts.vo                      | 0m44.12s  || +0m00.39s | +0.88%
0m44.10s  | RewriterInterpProofs1.vo                        | 0m43.89s  || +0m00.21s | +0.47%
0m43.66s  | ExtractionHaskell/unsaturated_solinas           | 0m43.25s  || +0m00.40s | +0.94%
0m36.46s  | PushButtonSynthesis/UnsaturatedSolinas.vo       | 0m36.36s  || +0m00.10s | +0.27%
0m36.09s  | RewriterWf1.vo                                  | 0m36.07s  || +0m00.02s | +0.05%
0m34.50s  | Fancy/Montgomery256.vo                          | 0m34.30s  || +0m00.20s | +0.58%
0m27.13s  | PushButtonSynthesis/WordByWordMontgomery.vo     | 0m26.99s  || +0m00.14s | +0.51%
0m24.70s  | Rewriter/Arith.vo                               | 0m24.26s  || +0m00.43s | +1.81%
0m22.75s  | ExtractionOCaml/word_by_word_montgomery         | 0m22.15s  || +0m00.60s | +2.70%
0m20.96s  | PushButtonSynthesis/BarrettReduction.vo         | 0m20.74s  || +0m00.22s | +1.06%
0m18.96s  | p448_solinas_64.c                               | 0m19.32s  || -0m00.35s | -1.86%
0m18.16s  | secp256k1_32.c                                  | 0m18.13s  || +0m00.03s | +0.16%
0m14.62s  | ExtractionOCaml/word_by_word_montgomery.ml      | 0m13.77s  || +0m00.84s | +6.17%
0m11.84s  | ExtractionOCaml/saturated_solinas               | 0m11.30s  || +0m00.53s | +4.77%
0m09.55s  | ExtractionOCaml/unsaturated_solinas.ml          | 0m09.14s  || +0m00.41s | +4.48%
0m08.42s  | ExtractionHaskell/word_by_word_montgomery.hs    | 0m08.16s  || +0m00.25s | +3.18%
0m06.96s  | BoundsPipeline.vo                               | 0m06.85s  || +0m00.11s | +1.60%
0m06.54s  | ExtractionHaskell/unsaturated_solinas.hs        | 0m07.17s  || -0m00.62s | -8.78%
0m03.57s  | PushButtonSynthesis/Primitives.vo               | 0m03.46s  || +0m00.10s | +3.17%
0m03.35s  | PushButtonSynthesis/SmallExamples.vo            | 0m03.34s  || +0m00.01s | +0.29%
0m03.30s  | PushButtonSynthesis/SaturatedSolinas.vo         | 0m03.22s  || +0m00.07s | +2.48%
0m02.83s  | curve25519_32.c                                 | 0m02.86s  || -0m00.02s | -1.04%
0m02.70s  | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.63s  || +0m00.07s | +2.66%
0m02.08s  | Rewriter.vo                                     | 0m02.02s  || +0m00.06s | +2.97%
0m01.60s  | curve25519_64.c                                 | 0m01.82s  || -0m00.21s | -12.08%
0m01.47s  | secp256k1_64.c                                  | 0m01.94s  || -0m00.47s | -24.22%
0m01.34s  | p224_64.c                                       | 0m01.71s  || -0m00.36s | -21.63%
0m01.33s  | CLI.vo                                          | 0m01.38s  || -0m00.04s | -3.62%
0m01.32s  | p256_64.c                                       | 0m01.77s  || -0m00.44s | -25.42%
0m01.28s  | Rewriter/ToFancy.vo                             | 0m01.36s  || -0m00.08s | -5.88%
0m01.23s  | Rewriter/StripLiteralCasts.vo                   | 0m01.08s  || +0m00.14s | +13.88%
0m01.16s  | StandaloneHaskellMain.vo                        | 0m01.18s  || -0m00.02s | -1.69%
0m01.13s  | CompilersTestCases.vo                           | 0m01.18s  || -0m00.05s | -4.23%
0m01.07s  | StandaloneOCamlMain.vo                          | 0m01.12s  || -0m00.05s | -4.46%
0m00.83s  | RewriterAll.vo                                  | 0m00.66s  || +0m00.16s | +25.75%
0m00.78s  | RewriterAllTactics.vo                           | 0m00.83s  || -0m00.04s | -6.02%

1 files changed, 37 insertions, 52 deletions

diff --git a/src/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v
index 9094a8a98..2bab688dc 100644
--- a/src/GENERATEDIdentifiersWithoutTypesProofs.v
+++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -84,7 +84,8 @@ Module Compilers.
         Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw.ident.
         Import Datatypes. (* for Some, None, option *)
 
-        Global Instance eq_ident_Decidable : DecidableRel (@eq ident) := ident_eq_dec.
+        Global Instance eq_ident_Decidable : DecidableRel (@eq ident)
+          := dec_rel_of_bool_dec_rel ident_beq ident_bl ident_lb.
 
         Lemma to_typed_invert_bind_args_gen t idc p f
           : @invert_bind_args t idc p = Some f
@@ -116,30 +117,45 @@ Module Compilers.
           exact (proj2_sig (@to_typed_invert_bind_args_gen t idc p f pf)).
         Defined.
 
+        Lemma invert_bind_args_to_typed p f
+          : invert_bind_args (to_typed p f) p = Some f.
+        Proof.
+          destruct p; cbn in *;
+            repeat first [ reflexivity
+                         | progress destruct_head'_unit
+                         | progress destruct_head'_prod
+                         | progress destruct_head' (@PrimitiveSigma.Primitive.sigT) ].
+        Qed.
+
+        Lemma is_simple_correct0 p
+          : is_simple p = true
+            <-> (forall f1 f2, type_of p f1 = type_of p f2).
+        Proof.
+          destruct p; cbn; split; intro H;
+            try solve [ reflexivity | exfalso; discriminate ].
+          all: repeat first [ match goal with
+                              | [ H : nat -> ?A |- _ ] => specialize (H O)
+                              | [ H : unit -> ?A |- _ ] => specialize (H tt)
+                              | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H
+                              | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H
+                              | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y))
+                              | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H
+                              end
+                            | congruence ].
+        Qed.
+
         Lemma is_simple_correct p
           : is_simple p = true
             <-> (forall t1 idc1 t2 idc2, @invert_bind_args t1 idc1 p <> None -> @invert_bind_args t2 idc2 p <> None -> t1 = t2).
         Proof.
-          split; intro H;
-            [ | specialize (fun f1 f2 => H _ (@to_typed p f1) _ (@to_typed p f2)) ];
-            destruct p; cbn in *; try solve [ reflexivity | exfalso; discriminate ];
-              repeat first [ progress intros *
-                           | match goal with
-                             | [ |- ?x = ?x ] => reflexivity
-                             | [ |- ?x = ?x -> _ ] => intros _
-                             | [ |- None <> None -> ?P ] => exact (@quick_invert_neq_option _ P None None)
-                             | [ |- Some _ <> None -> _ ] => intros _
-                             | [ |- None <> Some _ -> _ ] => intros _
-                             | [ H : forall x y, Some _ <> None -> _ |- _ ] => specialize (fun x y => H x y Some_neq_None)
-                             | [ H : nat -> ?A |- _ ] => specialize (H O)
-                             | [ H : unit -> ?A |- _ ] => specialize (H tt)
-                             | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H
-                             | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H
-                             | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y))
-                             | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H
-                             end
-                           | break_innermost_match_step
-                           | congruence ].
+          rewrite is_simple_correct0; split; intro H.
+          { intros t1 idc1 t2 idc2 H1 H2.
+            destruct (invert_bind_args idc1 p) eqn:?, (invert_bind_args idc2 p) eqn:?; try congruence.
+            erewrite (type_of_invert_bind_args t1), (type_of_invert_bind_args t2) by eassumption.
+            apply H. }
+          { intros f1 f2.
+            apply (H _ (to_typed p f1) _ (to_typed p f2));
+              rewrite invert_bind_args_to_typed; congruence. }
         Qed.
       End ident.
     End Raw.
@@ -152,13 +168,6 @@ Module Compilers.
         : @eta_ident_cps T t idc f = f t idc.
       Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed.
 
-(*
-      Lemma is_simple_strip_types_iff_type_vars_nil {t} idc
-        : Raw.ident.is_simple (@strip_types t idc) = true
-          <-> type_vars idc = List.nil.
-      Proof. destruct idc; cbn; intuition congruence. Qed.
-*)
-
       Lemma unify_to_typed {t t' pidc idc}
         : forall v,
           @unify t t' pidc idc = Some v
@@ -180,30 +189,6 @@ Module Compilers.
       Proof.
         destruct idc; cbn; break_innermost_match; exact Some_neq_None.
       Qed.
-
-      Lemma to_typed_of_typed_ident {t idc}
-        : forall v,
-          unify (@of_typed_ident t idc) idc = Some v
-          -> forall evm pf,
-            (rew [Compilers.ident] pf in to_typed (@of_typed_ident t idc) evm v)
-            = idc.
-      Proof.
-        destruct idc.
-        all: repeat first [ break_innermost_match_step
-                          | break_innermost_match_hyps_step
-                          | progress intros
-                          | reflexivity
-                          | progress subst
-                          | progress inversion_option
-                          | progress eliminate_hprop_eq
-                          | progress fold (@base.subst_default)
-                          | progress cbn in *
-                          | lazymatch goal with
-                            | [ H : context[base.subst_default (base.relax ?t) ?evm] |- _ ]
-                              => generalize dependent (base.subst_default (base.relax t) evm)
-                            end
-                          | progress Compilers.type.inversion_type ].
-      Qed.
     End ident.
   End pattern.
 End Compilers.