The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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