The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi Julien,

Thank you!

On Wed, Feb 4, 2015 at 2:31 PM, Julien Forest <julien.forest AT ensiie.fr> wrote:

On Wed, 4 Feb 2015 07:24:17 +0100
Julien Forest <julien.forest AT ensiie.fr> wrote:

>
> Hi Mukesh,
> maybe you can define first the Ancestor relation on you tree, the show
> that this relation is well founded and then just write something
> like :
>
> Function f node map {wf Ancestor node} :=
>      | None => None
>      | Some parent => if beq_nat node parent then node else find
>  parent map end.
>
> and do a proof very similar to Pierre's proposal.
>
>
> Best regards,
>
> Julien

>
> On Wed, 4 Feb 2015 09:22:43 +0530
> mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:
>
> > Hi Pierre,
> > Thank you for reply. Sorry for not being clear about problem.
> >
> > On Tue, Feb 3, 2015 at 8:02 PM, Pierre Courtieu
> > <pierre.courtieu AT gmail.com> wrote:
> >
> > > Hi, I found bizarre that you put f as an argument of moveup.
> >
> >
> > The idea is, I have a tree and each node has parent. Root is parent
> > of itself. Now I am looking for path from any given node ( n )  to
> > root.  I am storing node as key and its parent as value in map.
> >
> > Fixpoint f  node map :=
> >   match find node map with
> >     | None => None
> >     | Some parent => if beq_nat node parent then node else find
> > parent map end.
> > This function is not accepted in Coq because Coq is not convinced
> > about termination. If I have well founded relation between node and
> > its parent then it will be convinced.  I am looking for how encode
> > this property as well founded relation. I don't know the path length
> > in advance but all I know is, it will go to root and there my
> > computation will terminate.
> >
> > Regards,
> > Mukesh Tiwari
> >
> >