Created
May 23, 2019 02:42
-
-
Save JasonGross/0218fac1e348bd09bdfb3cbad12eeef1 to your computer and use it in GitHub Desktop.
Fast boolean equality proofs on finite types
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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 specializebeq_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.