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 17:37:31 -0400

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




Archive powered by MHonArc 2.6.18.

Top of Page