Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why no unfolding on left in match?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why no unfolding on left in match?


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why no unfolding on left in match?
  • Date: Wed, 08 Oct 2014 16:04:11 -0400

On 10/08/2014 03:46 PM, Jonathan wrote:
On 10/08/2014 03:14 PM, Greg Morrisett wrote:
This is an instance of a more general problem with datatypes/inductive
definitions that arises in the ML/Haskell/Coq/etc. community: pattern
matching does not promote abstraction.

I’ve always wanted to have more control over this in the form of
an abstract pattern declaration (with attendant proofs that the
patterns are exhaustive and non-overlapping.)

-Greg

Aren't you just requesting the common "dependent view" idiom? Define a new inductive type with constructors that are the patterns you want, then define a total function mapping the original type(s) to the view type. Think of the classic isEven/isOdd example.

-- Jonathan


Definition foo := 1.

Inductive isFoo(i : nat) : Type :=
| Yes(eq : i = foo)
| No(neq : i <> foo).

Definition IsFoo(i : nat) : isFoo i := ....

Definition bar (n:nat): nat := match IsFoo(n) with Yes _ _ => 1 | No _ _ => 0 end.

In other words, as long as you consider a match statement as being partnered with an inductive view and total view function, then taken together they are abstract.

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page