Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
    < Chronological >      < Thread >
  • From: Jason Hu <fdhzs2010 AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Substitution of sub-tree occurrence in a tree
  • Date: Fri, 24 Sep 2021 02:22:40 +0000
  • Accept-language: en-CA, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; 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=pcHcEpJvM8D+cqzQOoJV7P7v6eVAcnpFum81n+RJie4=; b=cPJ/EGmHwywTeBTg6eWuqOFx3jlkX0J8e7mMYAH+7s5Bh6hcmkNZ9zPOpaesHzA116y2WLztVuCXY5AbFSSM2TM1ET6SRt/XKsMHjamNTCM5UDgbFPPrnua+pFQliRUNWrjyGJRktyxmnEE0qLRn727oZ3qUQUYtBHGJO1fcNaM9EKHaHcZmqit3dKBJkmCzMVkSoVSAid29FMd6MDwPT51DIQJP9UUbeHfJckROlsxY0cn3hIpQVYiWVgG8cIU3AGBPR5qCV+qnyqHdVza6hiSme2rJfu3dTId1cYMqd2HvrvYSzwUQsc2nHEMB0ap92dLqhCpHlLKvKxUmjitkmQ==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=d5v4ffSyF6+RnyypzuaLPj6rW3cTdDqOBysPPv7iNJbDF0h04HRUlo0EfFrR+t4aXIPeZ0i6ceAyrKtgHlwD7RMJkgF34SKa732GjWAjXVWlUvRIvjuVOedYCAuw2pE/ai9TS4kp4Az7us06UKAKshiRKbZxA8eKqtPOSP+fZBOTI/YU3by6WcWlmkMC1wcpmv1PRrx8k0/mMCQPK7vFvohDryOzkuDnKVvPCVafoqN8++WDdtaIHN+HOKJhTCezQkmlaxMBAUVAv28SneNp5jmDhQ+0px5OnlbZOpYPGDYXFVfL49nbunsNSlST7GW9iLIQwr77XM9/gcRUIKYpOg==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM12-DM6-obe.outbound.protection.outlook.com
  • Ironport-hdrordr: A9a23:LooK1q8teFqMhjXbxRNuk+CtI+orL9Y04lQ7vn2ZJiY4TiX1ra2TdYoguyMc4Qx5MBodcLu7V5VoL0m3yaJI
  • Ironport-phdr: A9a23:qZOooBLQN4SeFhqY8NmcuNNmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvbM81RSUAs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmTowZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipy+y+4ZnebxhHiDe9Y755MQm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lTbNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8r1rRQfohikZKjA57G/ZhM9+jK1ZvB2uqAdyzJTIbI2JLvdyYr/RcNMcSGFcXshRTStBAoakYoULFeUBJuFYr4/grFUMsBu1GA6hBO3yxT9Ih372xrM23/g8HQ3axwEgH9UOsGjRrNrvNacSVfq5w7XPzTXGdv5b3yr254fUfB47u/6MQa5wftTLyUkpDw7IjludpIL5Mj6Uy+kBrmiW4/ZgWO+ulmMqpA9/rDiyysotlIXEgoEYx1HE+Ct5wIg4J9+1RVB0bNK6DJdeuS6UOo1rSc0hW2FloCk3xqEctZO/YiQG0oorywDFZ/CZcYWE+gzvWeeNLTp2gX9pZa6ziA2z/EWlxODwSse53VNIoyVYl9TBs24B2wLV58OaUPVy5F2h1iyK1w3L6uFLP0Q0la3DJpA53rM+kYcfvVraEiH4n0v7jbaadkI/9ee28ejnZajmpoOHOI9zlwH+NLkhltanAeQiNQgOQ3aU9vig1L3i+k35Rq9GjvorkqnFtJDaIsMbpq2jDwBJ1YYj7g6zDzag0NsGgXkKNF1IdA6dg4XtJV3COu70Aemlj1iykjpn3/XGMafgApXJIHjDirDhfbNl5k5S1QUzzdFe54lKBr0dPf7/RlT8tNzfDh8lNgy72efnCNFn2owCXmKPB7eVMLnOvl+Q+uIvP+6MaZcJtzb6Mvgp/uLhjXskmVAGZqSpxpsWaHWgHvt8OUmZYHzsgs0AEWgQpAY+Qvbq2xW+VmsZbHGrGqk4+zsTCYS8DI6FSJrnyOiK2z7+FZlLbEhHDEqNGDHmbdPXde0LbXewK9RmlHQkSPD1RYMhxwr07Fai47pgMu/d+ylevpXmgosmr9bPnA0/oGQnR/+W1HuAGjkcdoYgRzgq2al+pQp2zVLRicCQbNRYEsBW7vJNFAw9MMyFpwSbI/bbf1ubO/usFhOhSNjgBiwtRNUsxdNIe1x6B9ipkhHE2WytHqMRkLuIQpcz9/CFt0U=

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

 


Archive powered by MHonArc 2.6.19+.

Top of Page