The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

For Cast, how about something like:

Require Import Program.

Definition TagOf (n:Node) : Tag :=
match n with
| left _ => L
| right _ => R
end.

Program Definition Cast tag (n:Node | TagOf n = tag) :
  Element tag :=
match tag with
| L => match n with
       | left e => e
       | right _ => !
       end
| R => match n with
       | left _ => !
       | right e => e
       end
end.

(* or *)

Definition Cast' (n:Node) : Element (TagOf n) :=
match n with
| left e => e
| right e => e
end.
-- 
Daniel Schepler

On Thu, Feb 13, 2014 at 4:26 PM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> 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
>> >>>>
>> >>>>
>> >>>
>> >>
>> >
>
>