coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] How do I define this function for non-empty lists?
Date: Thu, 29 Oct 2020 16:20:10 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay3-d.mail.gandi.net
Ironport-phdr: 9a23:LYSsVRGJJAiW4tq/aKW5W51GYnF86YWxBRYc798ds5kLTJ7ypsuwAkXT6L1XgUPTWs2DsrQY0rWQ4vqrCTVIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLF/IA+yoAnPucUbgpZuIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFokaxVvhyhqRx8zYDabo6aO/hxcb/Sc94BWWpMXdxcWzBdDo6ybYYCCfcKM+ZCr4n6olsDtRqwChOwA+Pz0DBIgGf506w70+QlCg7JwhYgH84Tu3nTo9X6LrkdUfyvw6nO1znDYPJW2TPm54fWaBAhveqBXalzccvR0kkvFALFjlCVqYP7JTOZzOINvHaH7+d5U++klmEopR1rrDe12scslpfGhpgTyl3c9St0wZs4KNykREN0YdOoDZReuSGHOodoXs4vQX9ltTg5x7AapZK2fisHxZAlyhLDafGKc4mF7xDjWuieITp1mnRoc6+xiRa19Eiv0Oz8Vs+s3VZFrypFjtnMtm0W2BDJ9seHTf5980G80jiMzwDe8v9ILV02mKbBKZMt3qQ8mocQvEnNBCP6hUH7ga+Oekk59OWl5P7rbqjiq5OGKoN5iAXzPr4zlsGxHOg1NBUFUXKB9uSmzrLj+FX0QLVUgf0ylanUqIraKtofpqGjAw5Y3J8v5AulAzejytsYnH0HIEhKeB2diYjmJlDOLOr+Dfihn1SgiDZrx/bYMb39GpjBMGXPnbX7cbt/90JQ0hc/wNNR6p5OF70MJPL+Vlf0tNPCDx85NwK0w/zgCNV4zo4eVniADbGFMKzIt1+E/O0vI+iIZIAOpjn9MeQl6uX1jX86mV4dZqqp3ZoSaHC9APtmOV+VYXzyjdcdCWsKpBYxTPT2iF2eVj5ef2q9X6Ul5j0iFI2mCZrDSZu2jbya3Ca7G4VWaXpcBlCNF3fobYSEVO0WZCKcOM8y2gADALOmUsoq0QyknA780btuaOTOqQMCspe2+9H2++TVoj4z8TZ5FdjVh26EQn19mCUHRjs80bpjiVd+20yA0K19juYeE9FPsaAaGjwmPILRmrQpQ+v5XRjMK4/QFASWB+6+CDR0deofhscUah8jSc6hnwvA3i+vDqVTkbGXVsRtr/DsmkPpLsM48E7okaksi158H5lVOGmvl/U6+07WDo/N1UqQkaqrM6IRwHyVrTbR/S+1pEhdFTVIf+DAVHEbaFHRqI2ntFjBXqStCLEiPxEHz8OeePJH

If you do "cbv" in your proof, you will get the goal

match list_nil_dec nat nil with
| left _ => < 1 >
| right pr => match pr eq_refl return (nonEmpty nat) with
end :| 1
end = < 1 >

this means reduction is blocked by your lemma list_nil_dec.
If you change the Qed to Defined for list_nil_dec, reflexivity works.

Gaëtan Gilbert

On 29/10/2020 16:09, Agnishom Chattopadhyay wrote:

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 <https://gist.github.com/Agnishom/573a697dab82ddb72360136014065f7f>,
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