The Coq mailing list

[Ian Shillito <Ian.Shillito AT anu.edu.au>]

Thanks for the reference Qinshi. I'll have a look. 🙂

Best,

Ian

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Qinshi Wang <qinshiw AT cs.princeton.edu>
Sent: Friday, 24 September 2021 3:20 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Substitution of sub-tree occurrence in a tree

 

This is not as complete as a library, but you might find it helpful. People in my lab experimented with trees with a hole. You can find a definition and some auxiliary functions in the following link. Also, there could be useful lemmas in other files in that folder.

https://github.com/PrincetonUniversity/VST/blob/master/wand_demo/wand_demo/SearchTree_ext.v

Thanks,

Qinshi

On Thu, Sep 23, 2021 at 10:35 PM Ian Shillito <Ian.Shillito AT anu.edu.au> wrote:

Hi Jason, 

I considered defining an auxiliary type encapsulating the notion of "tree with a hole", but did not know this had a given name. I will investigate in this direction then. Thanks! 

Best,

Ian

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jason Hu <fdhzs2010 AT hotmail.com>
Sent: Friday, 24 September 2021 12:22 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Substitution of sub-tree occurrence in a tree

 

Hi Ian,

 

My intuition is to use zipper instead of a library. If this is not a simplified example, proving a few lemmas about zipper shouldn’t be too bad.

 

Thanks,

Jason Hu

 

From: Ian Shillito
Sent: Thursday, September 23, 2021 7:59 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Substitution of sub-tree occurrence in a tree

 

Hi all, 

 

Is there some library out there which conveniently deals with substitution of sub-tree occurrences in binary trees? I could not find anything of the sort.

 

Here's the definition of binary trees of natural numbers I have in mind:

Inductive binary_tree : Type :=

 | Leaf : nat -> binary_tree

 | Node : binary_tree -> binary_tree -> binary_tree

.

Intuitively, I would like to be able to talk about T(T') where T(_) is a "binary tree with a hole", T' is a binary tree, and T(T') is consequently a binary tree. Expressing this would allow me to substitute the occurrence of T' under focus in T(T') for another binary tree T'' to get T(T''). Any convenient way to do this?

 

Thanks in advance! 

 

Best,

Ian