Pattern matching multiple constructors in one sentence in Coq
Suppose I have an inductive type of arithmetic 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 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 designers plus
, minus
, mult
and div
, expsum
doing the same thing after the pattern matching. I would 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 one sentence takes care of multiple constructors. I think I've seen this in other functional languages. Is this possible in Coq?
source to share
This cannot be done in terms of language. Coq is very powerful on its own due to its dependent types, but it is not its own metalanguage; there is no way to write the term Coq that manipulates the Coq constructors as such (just as terms, and this is not enough to construct pattern matching).
There might be a way to do it in vernacular (the top-level language in which you write definitions of terms, evidence in tactical language, etc.), but I don't think there is. If he existed anywhere, I would expect him to be in Program
. But applying the same pattern to constructors that have the same type is a rather specific need.
This can be done using proof language. Evidence in Coq is just terms; tactics of helping with duplicate evidence can help in the same way with duplicate 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 the arity variable, using a tactical construct match goal
to parse the arguments of each constructor and construct an appropriate result.
As long as it works, it is difficult. The tactic is for proof writing where computational content doesn't matter. When you use them to write terms whose actual definition matters (as opposed to type), you have to be very careful to make sure that you are defining the term that you expect and not some other term that is of the same type. ... As you've probably been thinking for a few minutes now, this code hasn't received a readability award.
I do not recommend this method at all because it is error prone. But it can be useful when you have a lot of similar types and functions and the types change during development. You get some pretty unreadable tactics, but once you debug them, they can work even when customizing expression types.
source to share
This is possible at 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*)
source to share