From 00a42993444ad6f77c8f20921e4c3e2cdaf56b66 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 29 Sep 2023 23:17:25 -0700
Subject: [PATCH] Drastically speed up ByteCompareSpec

Old:
```
theories/ByteCompareSpec.vo (real: 113.67, user: 111.75, sys: 1.57, mem: 1287536 ko)
```
New:
```
COQC theories/ByteCompareSpec.v
theories/ByteCompareSpec.vo (real: 9.46, user: 8.89, sys: 0.26, mem: 442460 ko)
```

The new file is also compatible with COQNATIVE, taking only seconds
rather than dozens of minutes or more.
---
 utils/theories/ByteCompareSpec.v | 26 +++++++++++++++++++-------
 1 file changed, 19 insertions(+), 7 deletions(-)

diff --git a/utils/theories/ByteCompareSpec.v b/utils/theories/ByteCompareSpec.v
index 1bf10f910..207588924 100644
--- a/utils/theories/ByteCompareSpec.v
+++ b/utils/theories/ByteCompareSpec.v
@@ -1,4 +1,4 @@
-From Coq Require Import Strings.Byte NArith.
+From Coq Require Import Strings.Byte NArith Eqdep_dec.
 From MetaCoq.Utils Require Import ReflectEq ByteCompare.
 From Equations Require Import Equations.
 
@@ -6,19 +6,31 @@ Derive NoConfusion for comparison.
 
 Section ByteNoConf.
   Local Ltac solve_noconf ::= idtac.
+  (** The NoConfusion definition is quite large, so we define a much more compact version of it that is nevertheless convertible *)
+  Definition eta_byte {A} (f : forall b : byte, A b) (b : byte) : A b
+    := Eval cbv in
+      ltac:(pose (f b) as v; destruct b; let val := (eval cbv in v) in exact val).
+  Definition uneta_byte {A f b} : @eta_byte A f b = f b
+    := match b with x00 | _ => eq_refl end.
+  Definition NoConfusion_byte_alt : byte -> byte -> Prop
+    := eta_byte (fun b1 b2 => eta_byte (fun b2 => if Byte.eqb b1 b2 then True else False) b2).
   Derive NoConfusion for byte.
   Next Obligation.
-    destruct a; abstract (destruct b; try exact (False_ind _ H); exact eq_refl).
-  Defined.
+    change (NoConfusion_byte a b) with (NoConfusion_byte_alt a b) in *.
+    cbv [NoConfusion_byte_alt] in *; apply byte_dec_bl.
+    rewrite !uneta_byte in *.
+    destruct Byte.eqb; [ reflexivity | exfalso; assumption ].
+  Qed.
   Next Obligation.
     destruct b; cbn; exact I.
   Defined.
   Next Obligation.
-    destruct a; abstract (destruct b; try (exact (False_ind _ e)); destruct e; exact eq_refl).
-  Defined.
+    lazymatch goal with |- ?f _ _ ?g = ?e => generalize g; revert e end; intros e g; subst; revert e.
+    destruct b; vm_compute; intros []; reflexivity.
+  Qed.
   Next Obligation.
-    destruct b; cbn; exact eq_refl.
-  Defined.
+    apply UIP_dec, byte_eq_dec.
+  Qed.
 End ByteNoConf.
 
 Lemma reflect_equiv P Q b : P <-> Q -> Bool.reflect P b -> Bool.reflect Q b.