Pattern matching multiple constructors in a single clause in Coq

Question

Suppose I have an inductive type of arithmetical expressions exp

Inductive exp : Type :=
| num : nat -> exp
| plus : exp -> exp -> exp
| minus : exp -> exp -> exp
| mult : exp -> exp -> exp
| div : exp -> exp -> exp.

and I want to define a function expsum that returns the sum of all numbers that occur in an exp. The obvious implementation is

Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n 
| plus e1 e2 => expsum e1 + expsum e2
| minus e1 e2 => expsum e1 + expsum e2
| mult e1 e2 => expsum e1 + expsum e2
| div e1 e2 => expsum e1 + expsum e2
end.

But for constructors plus, minus, mult, and div, expsum does exactly the same thing after pattern matching. I'd like to simplify it into something like

Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n 
| [ plus e1 e2 | minus e1 e2 | mult e1 e2 | div e1 e2 ]
   => expsum e1 + expsum e2
end.

so that a single clause takes care of multiple constructors. I think I've seen this done in other functional languages. Is this possible in Coq?

Answer 1

This can't be done in the term language. Coq's language is very powerful in itself, thanks to its dependent types, but it isn't its own metalanguage; there's no way to write a Coq term that manipulates Coq constructors as such (only as terms, and that's not good enough to build a pattern matching).

There could be a way to do this in the vernacular (the toplevel language in which you write definitions of terms, proofs in the tactic language, etc.), but I don't think there is. If it existed anywhere, I'd expect it to be in Program. But applying the same pattern to constructors that happen to have the same type is a rather specialized need.

It can be done with the proof language. Proofs in Coq are just terms; tactics that help with repetitive proofs can help in the same way with repetitive terms.

Inductive exp : Type :=
| num : nat -> exp
| plus : exp -> exp -> exp
| minus : exp -> exp -> exp
| mult : exp -> exp -> exp
| div : exp -> exp -> exp.

(* The boring old code *)    
Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n 
| plus e1 e2 => expsum e1 + expsum e2
| minus e1 e2 => expsum e1 + expsum e2
| mult e1 e2 => expsum e1 + expsum e2
| div e1 e2 => expsum e1 + expsum e2
end.

Definition expsum_tactic : exp -> nat.
  induction 1;
    (* Figure out the computation automatically based on what arguments are present *)
    exact n || exact (IHexp1 + IHexp2).
Defined. (* "Defined" rather than "Qed" to get a transparent definition *)

(* Show the two definitions in a nice way to visually compare them *)
Print expsum.
Eval compute [expsum expsum_tactic exp_rec] in (expsum, expsum_tactic).

This could be generalized to variable arity by using the match goal tactical construct to analyze the arguments of each constructor and building the result term accordingly.

While this works, it's tricky. Tactics are geared towards writing proofs, where the computational content is irrelevant. When you use them to write terms whose actual definition matters (as opposed to just the type), you need to be very careful to ensure that you're defining the term that you expected, rather than some other term that happens to have the same type. As you've probably been thinking for a few minutes now, that code doesn't win readability awards.

I don't recommend this method in general, because it's error-prone. But it can be useful when you have many similar types and functions and the types change during development. You end up with rather unreadable tacticals, but once you've debugged them, they can work even when you tweak the expression types.

Answer 2

This is possible in Coq >=8.5

Fixpoint expsum (e : exp) : nat :=
match e with
| num n => n
| (plus e1 e2 | minus e1 e2 | mult e1 e2 | div e1 e2) => expsum e1 + expsum e2 end.

Print expsum. (*expsum = 
fix expsum (e : exp) : nat :=
  match e with
  | num n => n
  | plus e1 e2 => expsum e1 + expsum e2
  | minus e1 e2 => expsum e1 + expsum e2
  | mult e1 e2 => expsum e1 + expsum e2
  | div e1 e2 => expsum e1 + expsum e2
  end
     : exp -> nat*)