I wrote a proof that entailment is decidable in singleton logic (one antecedent, one succedent). Here is my development:

```
Require Import Coq.Relations.Relation_Definitions.
Require Import Coq.Strings.String.
(** Singleton logic: only one assumption, only one conclusion *)
Inductive SingProp: Set :=
(** Atomic variable *)
| Var: string -> SingProp
(** Disjunction *)
| plus_: SingProp -> SingProp -> SingProp
(** Conjunction *)
| with_: SingProp -> SingProp -> SingProp.
Scheme Equality for SingProp.
Notation "A + B" := (plus_ A B) (at level 50, left associativity).
Notation "A & B" := (with_ A B) (at level 50, left associativity).
Reserved Notation "A |> B" (at level 60, no associativity).
Inductive entails: relation SingProp :=
| id s: Var s |> Var s
| plus_l A B C: A |> C -> B |> C -> A + B |> C
| plus_r1 A B C: A |> B -> A |> B + C
| plus_r2 A B C: A |> C -> A |> B + C
| with_l1 A B C: A |> C -> A & B |> C
| with_l2 A B C: B |> C -> A & B |> C
| with_r A B C: A |> B -> A |> C -> A |> B & C
where "A |> B" := (entails A B).
Lemma dec_entails A B: {A |> B} + {~ A |> B}.
Proof.
Admitted.
```

`dec_entails`

has a simple informal proof, proceeding by induction on the sum of the sizes of the hypothesis and conclusion. When both are of the form `Var _`

(corresponding to a combined size of zero), entailment is decidable as there is only one inference rule that mentions atomic variables. Otherwise, we check if any other inference rule applies. All inference rules have antecedents that are strictly smaller than their conclusions, so we can decide the antecedents using the induction hypothesis.

I’ve implemented this by enumerating every possible antecedent and showing that it is decidable. So one case of the proof looks like:

```
(* case _ & _ |> _ + _ *)
- show_decidable (H (s1, s3 + s4)).
show_decidable (H (s2, s3 + s4)).
show_decidable (H (s1 & s2, s3)).
show_decidable (H (s1 & s2, s4)).
```

The resulting decision procedure is positively enormous! I’m not sure how to get an exact number, but when I write `Print dec_entails`

I get a four-thousand-line definition, with lots of `...`

hiding even more code. Checking the proof takes about one second, and printing it takes several. I haven’t tried writing an unverified version, but I suspect it would be under fifty lines of code.

So my question is: how do you a) write efficient decision procedures, and b) assess the efficiency of an existing decision procedure?