Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] impossible branches in pattern matching

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] impossible branches in pattern matching


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] impossible branches in pattern matching
  • Date: Thu, 13 Feb 2014 15:47:27 -0800

I don't see why Cast should be valid, given that there's no relation
given between tag and n.
--
Daniel Schepler

On Thu, Feb 13, 2014 at 3:35 PM, Kirill Taran
<kirill.t256 AT gmail.com>
wrote:
> Hello again,
>
> What about such piece of code?
>
> Inductive Tag := L | R.
> Definition Element tag :=
> match tag with
> | L => nat
> | R => bool
> end.
> Inductive Node :=
> | left : Element L -> Node
> | right : Element R -> Node.
>
> Definition Cast tag (n : Node) : Element tag :=
> match tag with
> | L => match n return Element L with left e => e end
> | R => match n return Element R with right e => e end
> end.
>
> Coq can't infer that there enough branches and complains on definition of
> Cast.
>
> Pierre,
>
> I didn't find how to launch code with absurd pattern (!), your example
> doesn't work for me.
> Have I to enable any settings?
>
> Sincerely,
> Kirill Taran
>
>
> On Fri, Feb 14, 2014 at 12:32 AM, Kirill Taran
> <kirill.t256 AT gmail.com>
> wrote:
>>
>> Daniel,
>> Ow, I didn't try that; thanks.
>>
>> Pierre,
>> Thanks for advices about return and !. By the way, I really noticed that
>> the code I am working on now becomes pretty difficult in the sense that I
>> have to do some manual work.
>> Maybe there are any libs like lenses for haskell? (For reducing
>> boilerplate, when you need to extract something from the bottom of
>> structure
>> with different dependencies.)
>>
>> Sincerely,
>> Kirill Taran
>>
>>
>> On Thu, Feb 13, 2014 at 11:11 PM, Pierre-Marie Pédrot
>> <pierre-marie.pedrot AT inria.fr>
>> wrote:
>>>
>>> On 13/02/2014 19:54, Kirill Taran wrote:
>>> > But Coq complains about definition of Matching: it says that pattern
>>> > matching is non-exhaustive and there are can be branches L right and R
>>> > left. But we never can construct such objects. Why Coq can't infer
>>> > that?
>>>
>>> Because this is undecidable in general. You have to write out return
>>> clauses by hand when you start messing with dependent pattern-matching.
>>>
>>> Or you can use Program to do the dirty job for you.
>>>
>>> Program Definition Matching (n : Node) :=
>>> match n with
>>> | L left => True
>>> | R right => True
>>> | _ => !
>>> end.
>>>
>>> (Here '!' stands for the absurd case. Have a look at the generated term
>>> to understand how it works.)
>>>
>>> The more your inductives will be dependent, the more you will need to do
>>> things by hand. I recommend the reading of CPDT to get a handful of neat
>>> design patterns when programming with dependent types.
>>>
>>> PMP
>>>
>>>
>>
>



Archive powered by MHonArc 2.6.18.

Top of Page