Fast boolean equality proofs on finite types

fast_fin.v

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.

Lemma negb_existsb_nth_error {A} (ls : list A) (f : A -> bool) (H : existsb f ls = false) n v (H' : nth_error ls n = Some v)
  : f v = false.
Proof.
  revert dependent n; induction ls, n; cbn in *; intros; try congruence.
  all: repeat first [ progress subst
                    | rewrite orb_false_iff in *
                    | match goal with
                      | [ H : Some _ = Some _ |- _ ] => inversion H; clear H
                      | [ H : and _ _ |- _ ] => destruct H
                      end
                    | solve [ eauto ] ].
Qed.

Section fin.
  Context (t : Type)
          (ls : list t)
          (beq : t -> t -> bool)
          (to_nat : t -> nat)
          (ls_has_all : forall e, nth_error ls (to_nat e) = Some e)
          (beq_refl : forallb (fun x => beq x x) ls = true)
          (beq_unique : list_rect (fun _ => bool) true (fun x xs acc => andb acc (andb (negb (existsb (fun y => beq y x) xs)) (negb (existsb (beq x) xs)))) ls = true).


  Lemma nth_error_beq n m x y
    : nth_error ls n = Some x -> nth_error ls m = Some y -> beq x y = true -> n = m.
  Proof.
    clear ls_has_all.
    generalize dependent ls; clear dependent ls.
    revert m x y; induction n, m, ls; try reflexivity; repeat let H := fresh in intro H.
    all: cbn [nth_error list_rect forallb] in *; try congruence.
    all: repeat first [ progress subst
                      | apply (f_equal S)
                      | rewrite negb_true_iff in *
                      | rewrite andb_true_iff in *
                      | discriminate
                      | solve [ eauto ]
                      | match goal with
                        | [ H : Some ?x = Some ?y |- _ ] => inversion H; clear H
                        | [ H : and _ _ |- _ ] => destruct H
                        | [ H : existsb _ _ = false, H' : nth_error _ _ = Some _ |- _ ]
                          => rewrite (@negb_existsb_nth_error _ _ _ H _ _ H') in *
                        end ].
  Qed.


  Lemma reflect_of_fin : forall x y, reflect (x = y) (beq x y).
  Proof.
    intros x y; remember (beq x y) as b eqn:Heqb; destruct b; symmetry in Heqb; constructor.
    { cut (Some x = Some y); [ congruence | ].
      rewrite <- (ls_has_all x), <- (ls_has_all y).
      eapply f_equal, nth_error_beq; eauto. }
    { intro H; subst y.
      generalize beq_refl.
      rewrite forallb_forall; intro H.
      rewrite H in Heqb; [ discriminate | ].
      eapply nth_error_In; eauto. }
  Qed.
End fin.

Inductive t := a0 | a1 | a2 | a3 | a4 | a5 | a6 | a7 | a8 | a9 | a10 | a11 | a12 | a13 | a14 | a15 | a16 | a17 | a18 | a19 | a20 | a21 | a22 | a23 | a24 | a25 | a26 | a27 | a28 | a29 | a30 | a31 | a32 | a33 | a34 | a35 | a36 | a37 | a38 | a39 | a40 | a41 | a42 | a43 | a44 | a45 | a46 | a47 | a48 | a49 | a50 | a51 | a52 | a53 | a54 | a55 | a56 | a57 | a58 | a59 | a60 | a61 | a62 | a63 | a64 | a65 | a66 | a67 | a68 | a69 | a70 | a71 | a72 | a73 | a74 | a75 | a76 | a77 | a78 | a79 | a80 | a81 | a82 | a83 | a84 | a85 | a86 | a87 | a88 | a89 | a90 | a91 | a92 | a93 | a94 | a95 | a96 | a97 | a98 | a99 | a100 | a101 | a102 | a103 | a104 | a105 | a106 | a107 | a108 | a109 | a110 | a111 | a112 | a113 | a114 | a115 | a116 | a117 | a118 | a119 | a120 | a121 | a122 | a123 | a124 | a125 | a126 | a127 | a128 | a129 | a130 | a131 | a132 | a133 | a134 | a135 | a136 | a137 | a138 | a139 | a140 | a141 | a142 | a143 | a144 | a145 | a146 | a147 | a148 | a149 | a150 | a151 | a152 | a153 | a154 | a155 | a156 | a157 | a158 | a159 | a160 | a161 | a162 | a163 | a164 | a165 | a166 | a167 | a168 | a169 | a170 | a171 | a172 | a173 | a174 | a175 | a176 | a177 | a178 | a179 | a180 | a181 | a182 | a183 | a184 | a185 | a186 | a187 | a188 | a189 | a190 | a191 | a192 | a193 | a194 | a195 | a196 | a197 | a198 | a199 | a200 | a201 | a202 | a203 | a204 | a205 | a206 | a207 | a208 | a209 | a210 | a211 | a212 | a213 | a214 | a215 | a216 | a217 | a218 | a219 | a220 | a221 | a222 | a223 | a224 | a225 | a226 | a227 | a228 | a229 | a230 | a231 | a232 | a233 | a234 | a235 | a236 | a237 | a238 | a239 | a240 | a241 | a242 | a243 | a244 | a245 | a246 | a247 | a248 | a249 | a250 | a251 | a252 | a253 | a254 | a255.
Definition to_nat (x : t) : nat := match x with a0 => 0 | a1 => 1 | a2 => 2 | a3 => 3 | a4 => 4 | a5 => 5 | a6 => 6 | a7 => 7 | a8 => 8 | a9 => 9 | a10 => 10 | a11 => 11 | a12 => 12 | a13 => 13 | a14 => 14 | a15 => 15 | a16 => 16 | a17 => 17 | a18 => 18 | a19 => 19 | a20 => 20 | a21 => 21 | a22 => 22 | a23 => 23 | a24 => 24 | a25 => 25 | a26 => 26 | a27 => 27 | a28 => 28 | a29 => 29 | a30 => 30 | a31 => 31 | a32 => 32 | a33 => 33 | a34 => 34 | a35 => 35 | a36 => 36 | a37 => 37 | a38 => 38 | a39 => 39 | a40 => 40 | a41 => 41 | a42 => 42 | a43 => 43 | a44 => 44 | a45 => 45 | a46 => 46 | a47 => 47 | a48 => 48 | a49 => 49 | a50 => 50 | a51 => 51 | a52 => 52 | a53 => 53 | a54 => 54 | a55 => 55 | a56 => 56 | a57 => 57 | a58 => 58 | a59 => 59 | a60 => 60 | a61 => 61 | a62 => 62 | a63 => 63 | a64 => 64 | a65 => 65 | a66 => 66 | a67 => 67 | a68 => 68 | a69 => 69 | a70 => 70 | a71 => 71 | a72 => 72 | a73 => 73 | a74 => 74 | a75 => 75 | a76 => 76 | a77 => 77 | a78 => 78 | a79 => 79 | a80 => 80 | a81 => 81 | a82 => 82 | a83 => 83 | a84 => 84 | a85 => 85 | a86 => 86 | a87 => 87 | a88 => 88 | a89 => 89 | a90 => 90 | a91 => 91 | a92 => 92 | a93 => 93 | a94 => 94 | a95 => 95 | a96 => 96 | a97 => 97 | a98 => 98 | a99 => 99 | a100 => 100 | a101 => 101 | a102 => 102 | a103 => 103 | a104 => 104 | a105 => 105 | a106 => 106 | a107 => 107 | a108 => 108 | a109 => 109 | a110 => 110 | a111 => 111 | a112 => 112 | a113 => 113 | a114 => 114 | a115 => 115 | a116 => 116 | a117 => 117 | a118 => 118 | a119 => 119 | a120 => 120 | a121 => 121 | a122 => 122 | a123 => 123 | a124 => 124 | a125 => 125 | a126 => 126 | a127 => 127 | a128 => 128 | a129 => 129 | a130 => 130 | a131 => 131 | a132 => 132 | a133 => 133 | a134 => 134 | a135 => 135 | a136 => 136 | a137 => 137 | a138 => 138 | a139 => 139 | a140 => 140 | a141 => 141 | a142 => 142 | a143 => 143 | a144 => 144 | a145 => 145 | a146 => 146 | a147 => 147 | a148 => 148 | a149 => 149 | a150 => 150 | a151 => 151 | a152 => 152 | a153 => 153 | a154 => 154 | a155 => 155 | a156 => 156 | a157 => 157 | a158 => 158 | a159 => 159 | a160 => 160 | a161 => 161 | a162 => 162 | a163 => 163 | a164 => 164 | a165 => 165 | a166 => 166 | a167 => 167 | a168 => 168 | a169 => 169 | a170 => 170 | a171 => 171 | a172 => 172 | a173 => 173 | a174 => 174 | a175 => 175 | a176 => 176 | a177 => 177 | a178 => 178 | a179 => 179 | a180 => 180 | a181 => 181 | a182 => 182 | a183 => 183 | a184 => 184 | a185 => 185 | a186 => 186 | a187 => 187 | a188 => 188 | a189 => 189 | a190 => 190 | a191 => 191 | a192 => 192 | a193 => 193 | a194 => 194 | a195 => 195 | a196 => 196 | a197 => 197 | a198 => 198 | a199 => 199 | a200 => 200 | a201 => 201 | a202 => 202 | a203 => 203 | a204 => 204 | a205 => 205 | a206 => 206 | a207 => 207 | a208 => 208 | a209 => 209 | a210 => 210 | a211 => 211 | a212 => 212 | a213 => 213 | a214 => 214 | a215 => 215 | a216 => 216 | a217 => 217 | a218 => 218 | a219 => 219 | a220 => 220 | a221 => 221 | a222 => 222 | a223 => 223 | a224 => 224 | a225 => 225 | a226 => 226 | a227 => 227 | a228 => 228 | a229 => 229 | a230 => 230 | a231 => 231 | a232 => 232 | a233 => 233 | a234 => 234 | a235 => 235 | a236 => 236 | a237 => 237 | a238 => 238 | a239 => 239 | a240 => 240 | a241 => 241 | a242 => 242 | a243 => 243 | a244 => 244 | a245 => 245 | a246 => 246 | a247 => 247 | a248 => 248 | a249 => 249 | a250 => 250 | a251 => 251 | a252 => 252 | a253 => 253 | a254 => 254 | a255 => 255 end.
Definition ls : list t := [a0 ; a1 ; a2 ; a3 ; a4 ; a5 ; a6 ; a7 ; a8 ; a9 ; a10 ; a11 ; a12 ; a13 ; a14 ; a15 ; a16 ; a17 ; a18 ; a19 ; a20 ; a21 ; a22 ; a23 ; a24 ; a25 ; a26 ; a27 ; a28 ; a29 ; a30 ; a31 ; a32 ; a33 ; a34 ; a35 ; a36 ; a37 ; a38 ; a39 ; a40 ; a41 ; a42 ; a43 ; a44 ; a45 ; a46 ; a47 ; a48 ; a49 ; a50 ; a51 ; a52 ; a53 ; a54 ; a55 ; a56 ; a57 ; a58 ; a59 ; a60 ; a61 ; a62 ; a63 ; a64 ; a65 ; a66 ; a67 ; a68 ; a69 ; a70 ; a71 ; a72 ; a73 ; a74 ; a75 ; a76 ; a77 ; a78 ; a79 ; a80 ; a81 ; a82 ; a83 ; a84 ; a85 ; a86 ; a87 ; a88 ; a89 ; a90 ; a91 ; a92 ; a93 ; a94 ; a95 ; a96 ; a97 ; a98 ; a99 ; a100 ; a101 ; a102 ; a103 ; a104 ; a105 ; a106 ; a107 ; a108 ; a109 ; a110 ; a111 ; a112 ; a113 ; a114 ; a115 ; a116 ; a117 ; a118 ; a119 ; a120 ; a121 ; a122 ; a123 ; a124 ; a125 ; a126 ; a127 ; a128 ; a129 ; a130 ; a131 ; a132 ; a133 ; a134 ; a135 ; a136 ; a137 ; a138 ; a139 ; a140 ; a141 ; a142 ; a143 ; a144 ; a145 ; a146 ; a147 ; a148 ; a149 ; a150 ; a151 ; a152 ; a153 ; a154 ; a155 ; a156 ; a157 ; a158 ; a159 ; a160 ; a161 ; a162 ; a163 ; a164 ; a165 ; a166 ; a167 ; a168 ; a169 ; a170 ; a171 ; a172 ; a173 ; a174 ; a175 ; a176 ; a177 ; a178 ; a179 ; a180 ; a181 ; a182 ; a183 ; a184 ; a185 ; a186 ; a187 ; a188 ; a189 ; a190 ; a191 ; a192 ; a193 ; a194 ; a195 ; a196 ; a197 ; a198 ; a199 ; a200 ; a201 ; a202 ; a203 ; a204 ; a205 ; a206 ; a207 ; a208 ; a209 ; a210 ; a211 ; a212 ; a213 ; a214 ; a215 ; a216 ; a217 ; a218 ; a219 ; a220 ; a221 ; a222 ; a223 ; a224 ; a225 ; a226 ; a227 ; a228 ; a229 ; a230 ; a231 ; a232 ; a233 ; a234 ; a235 ; a236 ; a237 ; a238 ; a239 ; a240 ; a241 ; a242 ; a243 ; a244 ; a245 ; a246 ; a247 ; a248 ; a249 ; a250 ; a251 ; a252 ; a253 ; a254 ; a255].
Definition beq (x y : t) : bool :=
  match x, y with a0, a0 => true | a0, _ => false | a1, a1 => true | a1, _ => false | a2, a2 => true | a2, _ => false | a3, a3 => true | a3, _ => false | a4, a4 => true | a4, _ => false | a5, a5 => true | a5, _ => false | a6, a6 => true | a6, _ => false | a7, a7 => true | a7, _ => false | a8, a8 => true | a8, _ => false | a9, a9 => true | a9, _ => false | a10, a10 => true | a10, _ => false | a11, a11 => true | a11, _ => false | a12, a12 => true | a12, _ => false | a13, a13 => true | a13, _ => false | a14, a14 => true | a14, _ => false | a15, a15 => true | a15, _ => false | a16, a16 => true | a16, _ => false | a17, a17 => true | a17, _ => false | a18, a18 => true | a18, _ => false | a19, a19 => true | a19, _ => false | a20, a20 => true | a20, _ => false | a21, a21 => true | a21, _ => false | a22, a22 => true | a22, _ => false | a23, a23 => true | a23, _ => false | a24, a24 => true | a24, _ => false | a25, a25 => true | a25, _ => false | a26, a26 => true | a26, _ => false | a27, a27 => true | a27, _ => false | a28, a28 => true | a28, _ => false | a29, a29 => true | a29, _ => false | a30, a30 => true | a30, _ => false | a31, a31 => true | a31, _ => false | a32, a32 => true | a32, _ => false | a33, a33 => true | a33, _ => false | a34, a34 => true | a34, _ => false | a35, a35 => true | a35, _ => false | a36, a36 => true | a36, _ => false | a37, a37 => true | a37, _ => false | a38, a38 => true | a38, _ => false | a39, a39 => true | a39, _ => false | a40, a40 => true | a40, _ => false | a41, a41 => true | a41, _ => false | a42, a42 => true | a42, _ => false | a43, a43 => true | a43, _ => false | a44, a44 => true | a44, _ => false | a45, a45 => true | a45, _ => false | a46, a46 => true | a46, _ => false | a47, a47 => true | a47, _ => false | a48, a48 => true | a48, _ => false | a49, a49 => true | a49, _ => false | a50, a50 => true | a50, _ => false | a51, a51 => true | a51, _ => false | a52, a52 => true | a52, _ => false | a53, a53 => true | a53, _ => false | a54, a54 => true | a54, _ => false | a55, a55 => true | a55, _ => false | a56, a56 => true | a56, _ => false | a57, a57 => true | a57, _ => false | a58, a58 => true | a58, _ => false | a59, a59 => true | a59, _ => false | a60, a60 => true | a60, _ => false | a61, a61 => true | a61, _ => false | a62, a62 => true | a62, _ => false | a63, a63 => true | a63, _ => false | a64, a64 => true | a64, _ => false | a65, a65 => true | a65, _ => false | a66, a66 => true | a66, _ => false | a67, a67 => true | a67, _ => false | a68, a68 => true | a68, _ => false | a69, a69 => true | a69, _ => false | a70, a70 => true | a70, _ => false | a71, a71 => true | a71, _ => false | a72, a72 => true | a72, _ => false | a73, a73 => true | a73, _ => false | a74, a74 => true | a74, _ => false | a75, a75 => true | a75, _ => false | a76, a76 => true | a76, _ => false | a77, a77 => true | a77, _ => false | a78, a78 => true | a78, _ => false | a79, a79 => true | a79, _ => false | a80, a80 => true | a80, _ => false | a81, a81 => true | a81, _ => false | a82, a82 => true | a82, _ => false | a83, a83 => true | a83, _ => false | a84, a84 => true | a84, _ => false | a85, a85 => true | a85, _ => false | a86, a86 => true | a86, _ => false | a87, a87 => true | a87, _ => false | a88, a88 => true | a88, _ => false | a89, a89 => true | a89, _ => false | a90, a90 => true | a90, _ => false | a91, a91 => true | a91, _ => false | a92, a92 => true | a92, _ => false | a93, a93 => true | a93, _ => false | a94, a94 => true | a94, _ => false | a95, a95 => true | a95, _ => false | a96, a96 => true | a96, _ => false | a97, a97 => true | a97, _ => false | a98, a98 => true | a98, _ => false | a99, a99 => true | a99, _ => false | a100, a100 => true | a100, _ => false | a101, a101 => true | a101, _ => false | a102, a102 => true | a102, _ => false | a103, a103 => true | a103, _ => false | a104, a104 => true | a104, _ => false | a105, a105 => true | a105, _ => false | a106, a106 => true | a106, _ => false | a107, a107 => true | a107, _ => false | a108, a108 => true | a108, _ => false | a109, a109 => true | a109, _ => false | a110, a110 => true | a110, _ => false | a111, a111 => true | a111, _ => false | a112, a112 => true | a112, _ => false | a113, a113 => true | a113, _ => false | a114, a114 => true | a114, _ => false | a115, a115 => true | a115, _ => false | a116, a116 => true | a116, _ => false | a117, a117 => true | a117, _ => false | a118, a118 => true | a118, _ => false | a119, a119 => true | a119, _ => false | a120, a120 => true | a120, _ => false | a121, a121 => true | a121, _ => false | a122, a122 => true | a122, _ => false | a123, a123 => true | a123, _ => false | a124, a124 => true | a124, _ => false | a125, a125 => true | a125, _ => false | a126, a126 => true | a126, _ => false | a127, a127 => true | a127, _ => false | a128, a128 => true | a128, _ => false | a129, a129 => true | a129, _ => false | a130, a130 => true | a130, _ => false | a131, a131 => true | a131, _ => false | a132, a132 => true | a132, _ => false | a133, a133 => true | a133, _ => false | a134, a134 => true | a134, _ => false | a135, a135 => true | a135, _ => false | a136, a136 => true | a136, _ => false | a137, a137 => true | a137, _ => false | a138, a138 => true | a138, _ => false | a139, a139 => true | a139, _ => false | a140, a140 => true | a140, _ => false | a141, a141 => true | a141, _ => false | a142, a142 => true | a142, _ => false | a143, a143 => true | a143, _ => false | a144, a144 => true | a144, _ => false | a145, a145 => true | a145, _ => false | a146, a146 => true | a146, _ => false | a147, a147 => true | a147, _ => false | a148, a148 => true | a148, _ => false | a149, a149 => true | a149, _ => false | a150, a150 => true | a150, _ => false | a151, a151 => true | a151, _ => false | a152, a152 => true | a152, _ => false | a153, a153 => true | a153, _ => false | a154, a154 => true | a154, _ => false | a155, a155 => true | a155, _ => false | a156, a156 => true | a156, _ => false | a157, a157 => true | a157, _ => false | a158, a158 => true | a158, _ => false | a159, a159 => true | a159, _ => false | a160, a160 => true | a160, _ => false | a161, a161 => true | a161, _ => false | a162, a162 => true | a162, _ => false | a163, a163 => true | a163, _ => false | a164, a164 => true | a164, _ => false | a165, a165 => true | a165, _ => false | a166, a166 => true | a166, _ => false | a167, a167 => true | a167, _ => false | a168, a168 => true | a168, _ => false | a169, a169 => true | a169, _ => false | a170, a170 => true | a170, _ => false | a171, a171 => true | a171, _ => false | a172, a172 => true | a172, _ => false | a173, a173 => true | a173, _ => false | a174, a174 => true | a174, _ => false | a175, a175 => true | a175, _ => false | a176, a176 => true | a176, _ => false | a177, a177 => true | a177, _ => false | a178, a178 => true | a178, _ => false | a179, a179 => true | a179, _ => false | a180, a180 => true | a180, _ => false | a181, a181 => true | a181, _ => false | a182, a182 => true | a182, _ => false | a183, a183 => true | a183, _ => false | a184, a184 => true | a184, _ => false | a185, a185 => true | a185, _ => false | a186, a186 => true | a186, _ => false | a187, a187 => true | a187, _ => false | a188, a188 => true | a188, _ => false | a189, a189 => true | a189, _ => false | a190, a190 => true | a190, _ => false | a191, a191 => true | a191, _ => false | a192, a192 => true | a192, _ => false | a193, a193 => true | a193, _ => false | a194, a194 => true | a194, _ => false | a195, a195 => true | a195, _ => false | a196, a196 => true | a196, _ => false | a197, a197 => true | a197, _ => false | a198, a198 => true | a198, _ => false | a199, a199 => true | a199, _ => false | a200, a200 => true | a200, _ => false | a201, a201 => true | a201, _ => false | a202, a202 => true | a202, _ => false | a203, a203 => true | a203, _ => false | a204, a204 => true | a204, _ => false | a205, a205 => true | a205, _ => false | a206, a206 => true | a206, _ => false | a207, a207 => true | a207, _ => false | a208, a208 => true | a208, _ => false | a209, a209 => true | a209, _ => false | a210, a210 => true | a210, _ => false | a211, a211 => true | a211, _ => false | a212, a212 => true | a212, _ => false | a213, a213 => true | a213, _ => false | a214, a214 => true | a214, _ => false | a215, a215 => true | a215, _ => false | a216, a216 => true | a216, _ => false | a217, a217 => true | a217, _ => false | a218, a218 => true | a218, _ => false | a219, a219 => true | a219, _ => false | a220, a220 => true | a220, _ => false | a221, a221 => true | a221, _ => false | a222, a222 => true | a222, _ => false | a223, a223 => true | a223, _ => false | a224, a224 => true | a224, _ => false | a225, a225 => true | a225, _ => false | a226, a226 => true | a226, _ => false | a227, a227 => true | a227, _ => false | a228, a228 => true | a228, _ => false | a229, a229 => true | a229, _ => false | a230, a230 => true | a230, _ => false | a231, a231 => true | a231, _ => false | a232, a232 => true | a232, _ => false | a233, a233 => true | a233, _ => false | a234, a234 => true | a234, _ => false | a235, a235 => true | a235, _ => false | a236, a236 => true | a236, _ => false | a237, a237 => true | a237, _ => false | a238, a238 => true | a238, _ => false | a239, a239 => true | a239, _ => false | a240, a240 => true | a240, _ => false | a241, a241 => true | a241, _ => false | a242, a242 => true | a242, _ => false | a243, a243 => true | a243, _ => false | a244, a244 => true | a244, _ => false | a245, a245 => true | a245, _ => false | a246, a246 => true | a246, _ => false | a247, a247 => true | a247, _ => false | a248, a248 => true | a248, _ => false | a249, a249 => true | a249, _ => false | a250, a250 => true | a250, _ => false | a251, a251 => true | a251, _ => false | a252, a252 => true | a252, _ => false | a253, a253 => true | a253, _ => false | a254, a254 => true | a254, _ => false | a255, a255 => true | a255, _ => false end.
Lemma ls_has_all : forall e, nth_error ls (to_nat e) = Some e.
Proof. destruct e; reflexivity. Qed.
Lemma beq_refl : forallb (fun x => beq x x) ls = true.
Proof. vm_cast_no_check (eq_refl true). Qed.
Lemma beq_unique : list_rect (fun _ => bool) true (fun x xs acc => andb acc (andb (negb (existsb (fun y => beq y x) xs)) (negb (existsb (beq x) xs)))) ls = true.
Proof. vm_cast_no_check (eq_refl true). Qed.

Lemma reflect_beq : forall x y, reflect (x = y) (beq x y).
Proof. eapply reflect_of_fin; [ apply ls_has_all | apply beq_refl | apply beq_unique ]. Qed.

Hi, I tried here to extend your approach to non-enumerable types. Maybe that can interest you. The code is arguably ugly, but it works and the performance seems decent. The idea is a bit different, because I decided to accept already existing equality checking functions for the parameters of the constructors. Thus I wrote a generic test function beq_gen that takes as an argument a kind of description of the constructors of the inductive type (with dependent types to make it work). Then I have a single check that verifies that this description is faithful to the real inductive type. If this check succeeds on a given type, I can specialize beq_gen to this type. I also tried to accept recursive arguments in the constructor (this is the second file), but then I was annoyed with termination problems. I assumed that I was given a well-founded order on the type of interest, but there are probably lighter solutions.