The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/08/2014 05:04 PM, Greg Morrisett wrote:
> Yes. I just want some syntactic support to make this lighter weight. (Maybe 
> it can be done with clever notation now?). Bonus points if your solution 
> supports nested patterns.
>
> The classic example is wanting to match a string based on regexps.
>
> -Greg

Probably the correct answer is "write a DSL".   The inductive view/total 
function/match idiom is so general purpose that a lighter weight syntax 
would probably limit its capabilities in some way. Unless you just mean 
by omitting redundant parts.  For example, in this case, we currently have:

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

Definition IsFoo(i : nat) : isFoo i :=
match (Nat.eq_dec i foo) with
| left e => Yes i e
| right e => No i e
end.

Maybe syntactic sugar-coat both of those definitions into one like so:

View IsFoo(i : nat) : Type :=
match (Nat.eq_dec i foo) with
| left e => Yes e
| right e => No e
end.

If you then combined this into the target match in the bar function, 
you'd actually be reducing abstraction - since the IsFoo view may be is 
useful to functions other than bar.  You would then have to argue that 
Coq doesn't promote local definitions instead of that it doesn't promote 
abstraction.

-- Jonathan