Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Substitution of sub-tree occurrence in a tree

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Substitution of sub-tree occurrence in a tree


Chronological Thread 
    < Chronological >      < Thread >
  • From: Ian Shillito <Ian.Shillito AT anu.edu.au>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] Substitution of sub-tree occurrence in a tree
  • Date: Thu, 23 Sep 2021 23:59:24 +0000
  • Accept-language: en-AU, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version; bh=qL8br3WtQkNONnVkxbJi070/9FmYxmPvUmQpilsr2eI=; b=H8OJiwEeG+NfKMkoZbkp7fmHwUJZ3B9hJ8i1R9NcjTqfW0IFYDEP2zdk2CDfJXehH1gwZPZIKLEQ5chTY/VlTGeetc6Z90SNNEQvSKJogpcyAueRh7ePDG0Y+OT+ymo4g5rcXy8CrrcxrB9lMGndXacVo0gnmwm44u5Fd+VoV/WjwUZOJ8U9NToLZhuYOOPC4skRmtLTh7+nGi11wYWR2vaF/NDFMvWHu+uV3VcXIRyhFj4aADb7B8EbgaK0r2R+aLchgyl5fPtptegJG6fo6AKclaMM6FdA+xGmLwy/EQ27f4M3x1S3DZBnCJV734O7T183l9/n6j0+YUSuH+ExeA==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=l3jKoLHjzq6GzktXLh2qq37Pa1uz4Hsc0ovC+HhkjRVkh3dRedg6SJjF2aO3CMy6zp7RBo20H4cmij66dmJijS+hOFoSggGl18gKta8tvphMjFYw5v3ZGumkoDYiR9/4rSMx7+oXf7K4UoAkVzHB62a4JcCrJszpTYcNAZx+xJMt73O5BaZhE1wBX/Bg1i46AL7yNUcwrlA37ky197E2YhjLEvPMj7uZxKl4lgfnObLysoxTgCHDBgIwrp0p2jdse/7QHn4jvypt6KmmHS6WPV943539jd/uEf3ZrHPDbvzu1LY1cFZHSfNiHaiKf4TtSRV1J1Yh52hLlspQhl+4bA==
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Ian.Shillito AT anu.edu.au; spf=Pass smtp.mailfrom=Ian.Shillito AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY4-obe.outbound.protection.outlook.com
  • Ironport-hdrordr: A9a23:l4jjQa6FEmhDYngFXwPXwZSCI+orL9Y04lQ7vn2ZFiY5TiXIraqTdaogviMc0AxhPk3I6urwQZVoIEmsv6KdhLN8AV7MZniDhILFFuBfBOjZsnDd8k/Fh4lgPM5bGsAQZuEYZmIK7voSlTPIdurIt+P3kpxA692/815dCSVRL41w5QZwDQiWVmdsQhNdOJY/HJ2AouJaujuJYx0sH4uGL0hAe9KGi8zAlZrgbxJDLQUg8hOygTSh76O/OwSE3y0ZTyhEzd4ZgCb4ek3Cl+SeWsOAu1zhPlzontZrcRzau55+7fm3+4gow/PX+0KVjcpaKvq/VXsO0ZmSAR4R4aLxSlEbTohOAjrqDxyIiAHw1Qftyisj5knr1EKRi3rmrcvlcig3EdBAg4Vuchax0TtbgPhslKhR32ierfNsfGP9tTW46N7SWx5wkE2o5XIkjO4IlnRaFZATcblLsOUkjTVo+bo7bVbHAbocYZ5T5QDnlYdrWELfa2qcsnhkwdSqUHh2FhCaQlIassjQ1zRNhnh2w0YR2cRaxx47hdoAYogB4/6BPrVjlblIQMNTZaVhBP0ZSc/yDmDWWxrDPG+bPFyiHqAaPHDGrYLx/dwOlaiXUY1NyIF3lIXKUVteu2J3c0XyCdeW1JkO6RzJSHXVZ0WZ9iif3ekKhlTYfsuhDcSuciFQryKQmYRtPiSAYYfOBHt/OY6cEVfT
  • Ironport-phdr: A9a23:lyu+wRIFw5PP5p8NutmcuPdmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvbM81RSUAs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipy+y+4ZnebxhHiDe9Y755MQm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lTbNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8r1rRQfohikZKjA57G/ZhM9sg61Uux+uvQBzz5LObY2JKPZyY6XQds4aS2pbWcZRUjRMDICmYIsJEuEPIOZYr4j5p1sKrBu+GQ6sD/7oxzFLnHD227c23fkhEQHH2AwgG9MOsGjTrNjuLqgSV/21wLPWwjrecvNawy3y6JXRfx0nvPqDUq5+f9DLxkkzCwPKkE+QqYr9Mj6b1OkAs3SW4vZ8We+zi2AqqAF8rzuhy8osiofHhp8Zx07L+yh73os7Kt22RU9mbNOqDZZeuSGUOoV4TM88Xm1lvjsxxL4euZOjcyUG1I4rywPDZ/GFaYSE/w7vWeSLLTtlmH5od6qziwiz/ES8xODxU9S43EpWoSdEl9TAq2wB2hnO5sWHV/Rw+0Ks1SuB2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLuhEj5grKYelk59uSx9uroYLrrqoabN4BvlA7yKKMumtGjAesjNQgOQm6b9vmm2L375035R6lKgeMqnanFsZDaIsIbqrS+Aw9IzoYj7xG/DzCl0NgCgXYHK1dFdAqGj4jvJV7OPOj1APijj1i2jTtn2/LLMqf8DpnRLHXPiqrtcapy5kJEzQo819Ff55ZaCrEbJ/LzX1f8ut/CAR8/KQC63ubnCNR51oMaWGKPHqiZPbjIvl+O++IjOfeDa5IIuDrnMfcl+ubijWUlll8FYampwZwXZWikEfRhOkWVeGbjgtMcEWgRpQc+V+zriFiaUTFJfXqyXqQ85is6CI28F4vDSJqt0/S923LxFZpPI2tCF1qkEHHydozCVe1GIHaZJdYkmTgZX5CgTZUg3Fegrlmp5aBgK7/18ytQjpLi0Nx0++qbwTA783pPD8WZ12CRSEl9mH5OSjMrmqli9x8ugmyf2LR11qQLXedY4OlEB19S3Xv0xupnTd3+R0TIY4XRIL5HavybOmloC+kAn5oJaUs7HMi+hBfe2SbsG6USi7GAGJ0z9OTbwmT1IMF+jX3B0ft457HJasJJKCurirM5/hWBXub0
  • Suggested_attachment_session_id: f7c36c4d-8f40-e28f-1a47-2db8d38b9445
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

Archive powered by MHonArc 2.6.19+.

Top of Page