The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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
>>>
>>>
>>
>