The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

And yet another possibility (using an inductively defined Prop which
is equivalent to the previous TagOfNode n = tag):

Inductive NodeHasTag : Node -> Tag -> Prop :=
| left_has_tag_L e : NodeHasTag (left e) L
| right_has_tag_R e : NodeHasTag (right e) R.

Program Definition Cast'' tag
  (n:Node | NodeHasTag 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.
Solve Obligations using program_simpl;
  match goal with
  | H : NodeHasTag _ _ |- _ => inversion H
  end.
-- 
Daniel Schepler

On Thu, Feb 13, 2014 at 4:53 PM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> 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
>>> >>>>
>>> >>>>
>>> >>>
>>> >>
>>> >
>>
>>