coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Enrico Tassi, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Jonathan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Greg Morrisett, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Kevin Sullivan, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Abhishek Anand, 10/08/2014
- Re: [Coq-Club] Why no unfolding on left in match?, Adam Chlipala, 10/08/2014
Archive powered by MHonArc 2.6.18.