coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How do I define this function for non-empty lists?

From: Agnishom Chattopadhyay <agnishom AT cmi.ac.in>
To: coq-club AT inria.fr
Subject: [Coq-Club] How do I define this function for non-empty lists?
Date: Thu, 29 Oct 2020 10:09:35 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=agnishom AT cmi.ac.in; spf=Pass smtp.mailfrom=agnishom AT cmi.ac.in; spf=None smtp.helo=postmaster AT mail.cmi.ac.in
Ironport-phdr: 9a23:x/vcSR18NJsdUByAsmDT+DRfVm0co7zxezQtwd8ZseITIvad9pjvdHbS+e9qxAeQG9mCtLQV0aGG6ujJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhjexe7d/IAu5oQjSq8UdnJdvJLs2xhbVuHVDZv5YxXlvJVKdnhb84tm/8Zt++ClOuPwv6tBNX7zic6s3UbJXAjImM3so5MLwrhnMURGP5noHXWoIlBdDHhXI4wv7Xpf1tSv6q/Z91SyHNsD4Ubw4RTKv5LptRRT1iikIKiQ5/XnYhcJwgqxVow+vqQJjzIPPeo6ZKOBzc7nBcd8GR2dMWNtaWSxbAoO7aosCF/YMPeler4n8vFsOrRy+BQyxD+7xyj9HnGP23bE90+Q5Cw7JwQwgHtIUv3XUsd74M70dUe+zzKnJ1jXDb/RW2TLm5YfUdxAhoOuAUqhsfsbLyEkvERrIg1ONooPqIz2bzP4Cs3SH7+V+T+KvjXYqpgVvrzWt28siipXFiIwVx17L6Sl13IU4K9K2RUN1ZdOpDZVduiCZOoZoQc4vQGFltignx7ACpJK2fTUGxpQ6yhPZdveJfY+I4hf5W+aQJzd1nH1leLOjhxay7Eiv0ffwWdWz0FZPqCdOj9rCtmgV2hDO9MSKROFx80av1DqVyQzf9u9JLVoqmabGNZIt2qA8moYXvEjZHSL7mF/6gLKXe0gl4OSl6/jrb7P7rZGGLYB0kBvxMqE2l8y/H+s4Ng8OUnCe+eum1b3j+Vf1T6lPjv03iKXWqozVKd4apq6/GwNV04Aj5AijDzq+zdgUg3cKIEhEdR+JlYTlJU3CLf7iAfuhnligji9nx/XcMb3gBpXNIGLDkLDkfbtl8UFcxwwzzdFE55JUDbEBJen+VVP0tNzZFBM2KRC7z/zmCNV7zo8eQ36AAreFMKPOtl+F/v4gI+6VZIMMpDn9L+Ul6OX1gH8imV4deLGp0oENZHC5GPRmOUSZbmD2jtcPC2dZ9jY5GeftkRiJVSNZT3e0RaM1oD8hW6y8CoKWb4+rgaeB2yLzNZ1fenxBElmAEWbhZs3QUvgKaTmSJcpJmTkFE7GqDY4ng0L9/DTmwqZqe7KHshYTsojugYAsu7/j0Coq/DkxNPyzlnmXRjgtzGgNRnk/1+Z+px4lkwbR4e1Dm/VdUOdrybZMWwY+O4TbyrUjWdv3W0TIdZGITgT/G4j0MXQKVts0huQ2TQN9FtGl106R2iOrB/kekr3NDZdy86SOh3U=

Hi;

For an application, non-empty lists occur naturally. One way to deal with this would be to define a type of non-empty lists and then all the necessary functions and lemmas for them.

However, I am trying to recycle the theorems available in the standard library. To do this, I am defining a function which lifts functions on list to functions on my non-empty type provided they preserve non-emptiness.

But I am facing some trouble with this. For example, I cannot prove the lemma simple, over here.

What am I doing wrong?

--Agnishom

[Coq-Club] How do I define this function for non-empty lists?, Agnishom Chattopadhyay, 10/29/2020
- Re: [Coq-Club] How do I define this function for non-empty lists?, Gaëtan Gilbert, 10/29/2020
  - Re: [Coq-Club] How do I define this function for non-empty lists?, Agnishom Chattopadhyay, 10/29/2020
    - Re: [Coq-Club] How do I define this function for non-empty lists?, Jason Gross, 10/29/2020
      - Re: [Coq-Club] How do I define this function for non-empty lists?, Agnishom Chattopadhyay, 10/29/2020