The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Daniel,

That really works. But it is not obvious for me, why "fresh" function is casted to proper type while given argument isn't.
What about Cast function, I can't imagine how to tie node and tag together yet.

Sincerely,
Kirill Taran

On Fri, Feb 14, 2014 at 4:04 AM, Daniel Schepler <dschepler AT gmail.com> wrote:

For the definition of Wrap, you need the "convoy pattern" described in
CPDT to get m to be the right type inside the match:

Definition Wrap {tag} (m : Element tag) : Node :=

  match tag return (Element tag -> Node) with
  | L => fun m => left m
  | R => fun m => right m
  end m.

(And then, of course, you could optimize that to something like:
Definition Wrap' {tag} : Element tag -> Node :=
  match tag (* return (Element tag -> Node) *) with
  | L => left
  | R => right
  end.
)
--
Daniel Schepler

On Thu, Feb 13, 2014 at 3:47 PM, Kirill Taran <kirill.t256 AT gmail.com> wrote:
> I also tried (not very hard) to invent "opposite" of previous definition:
>
> Definition Wrap tag (m : Element tag) : Node :=
>   match tag with
>   | L => left m
>   | R => right m
>   end.
>
> But that fails, too. (Coq expects m to be Element L instead of Element tag.)
> I definetely should to glance at CPDT, but hadn't time for that yet.
>
> Sincerely,
> Kirill Taran
>
>
> On Fri, Feb 14, 2014 at 3:35 AM, 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
>>>>
>>>>
>>>
>>
>