coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] proof about applying a function on each element of a list using automaton

From: Fritjof Bornebusch <fritjof AT uni-bremen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] proof about applying a function on each element of a list using automaton
Date: Thu, 27 Sep 2018 16:45:49 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=SoftFail smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT lnv-91185.sb.dfki.de
Ironport-phdr: 9a23:w6kHIx9h+hr0if9uRHKM819IXTAuvvDOBiVQ1KB41+4cTK2v8tzYMVDF4r011RmVBdqds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55/ebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRhHohikZKjA3827YhdBtg69AvBKtuwZyz5LIbI2JNvdzeL7Wc9MARWpGW8ZcTyxPApm9b4sTDeoBOuhYpJTgqlsJtxu+AxejC/jyyj9TmnD23bAx3uMvEQHc3QwgA9AOsHParNjuKacSV+G1wLDTwjXZcfxW3Cny6I7Sfh88v/6BRLR9etfSx0k3Dw7Jk1udpIP/Mz6R1+kBqXWX4u59We61lmIqqAF8riCyysoihYTFnJ8Zxkza+Slj3oo5ON61RFRlbdK5DJddsTyROZFsTcM4WW5ovT43yr0Ytp6/eygH0JAnxxjBa/Ced4WE/w/vWeWRLDtin3JqY6iziAu88Uijy+3wTNS730hSoipElNnDqGwN2gTO5sWJRfZx5EOs1DeV2wzO7uxIPFo4mbfYJpMh2rIwk4AcsUXHHi/4gkX2i6qWe10q+uiy6uTnfrfmppiSN4JvlwH+NKUultWkDuQiLAcOWnaU+eKm2LL+40L1WK9KgeEukqnFrJDaItwWqbK+Aw9My4os9xK/Dyq939kDhnkGLFdFeAqdgITzOlHOJur4DfaljFi2njdr3aOOArq0CZLUa3PHjb3JfLBn6kcaxhBg48pY4sd6ELAdIvX9EmX2rtrVBAIiOAz8l+j9Ccl/0Y02RGSOR6WDPabftxmE67R8cKG3eIYJtWOleLAe7Pn0gCphwA5PTeySxZISLUuAMLFjKkSdb2Drh45cQ3oMv080VuHvhVvEXTMBPC/uDZJ53SkyDcedNamGXpqk2eHTwSG6W5dMa2VLDBaAHCWwLtjWa7I3cCuXZ/RZvHkEWLymEdVz0Rew8V6jkuo6aPHevCEWtpOl2NUnv+A=

Hi,

I'm struggeling a bit with the following proof:
I have an automaton (mealy machine) and I want to show that a given function
(f) to this
machine is applied to all elements of a given list (l).

The mealy machine is defined as:
Fixpoint mealy {S I O:Type} (f: S -> I -> (S*O)) (s: S) (l: list(I)) :
list(O) :=
match l with
| [] => nil
| i::is => match f s i with
| (s', o) => o :: (mealy f s' is)
end
end.

How can I formulate this in Coq?

Regards,
--f.

[Coq-Club] proof about applying a function on each element of a list using automaton, Fritjof Bornebusch, 09/27/2018
- Re: [Coq-Club] proof about applying a function on each element of a list using automaton, Jason -Zhong Sheng- Hu, 09/27/2018