coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: Fritjof Bornebusch <fritjof AT uni-bremen.de>, "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] proof about applying a function on each element of a list using automaton
Date: Thu, 27 Sep 2018 15:19:27 +0000
Accept-language: en-CA, en-US
Authentication-results: mail3-smtp-sop.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 NAM04-CO1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:O1TyaBz/+Xxj4QzXCy+O+j09IxM/srCxBDY+r6Qd2ugVIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiScIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CRWRPQNtfVzBPDI2/YYsADfYOMulDoobnu1cCsQGzCRWwCO/xzDJDm3/43bc90+QkCQzI2BYvH8kJsHTSsd75LaQdUeCyzKnOwjXIcu5Y2Tfj54jOfRAtuOyHU7BtccHMzkQvGR7KjlWRqIz+IT+ZyvkBv3SA4upgUuKvl2snpBtwojir3Msjlo7JhocMx13C6C53w541KMW3RUJne9KpFIVcuzuHO4dqWM8vQ3xktD40yrIYupO3YC0HxZE9yBPbdfCIaI2F7g/hWemKLzd1gXFod6ykiBu38EWv0eP8WdKy3V1XtCRKiMPMuWoI1xHL6siIVP99/kC51DiXyw3d7f1ILE8tmafFMpAt36c8lp0IvkvdBCP2n1j2jLONeUUj5+io7fnobq/+pp+GMI90lh/xPbgymsy+BuQ4NBICX2+G+eSg0L3j+kr5QLZQgvIqlanZtYjWJcUdpqGnHw9Yyoku5wqlAzqiztgUh2QLIE5fdB+HkoTlI1TOL+r5Dfe7jVSsijBrx/XeM73vH5rNLnnCkKz/cbph9kJQ1BE+zdBY55JID7EOOvPzWkvruNPECR85NhS4w/z7B9VlyoMeRWWPD7eFP6PVqF+E//4gI+2RZIAOozv9MPgk5/v2jXAjg1MdfK+p3YEWaH+iBPhmLV+ZMjLQhYIvC2YWvA0wBMbtkluPWyNIbHb6C6wm5y05D4yOEIHCA4q3jbmM2mG3E8sSLipNDUnJGnP1fa2FXe0NYWScOIUpxjcDTP2qT5Ir/RCorg7zjbR9eLn64Cod4LDqz99zr6jhlRY0+nRPD8mb3CTFb3w8ym0ERy0thvgm+WR9zUuG2Kl8xfdfEIoAtLtyTg4mOMuEnKRBANfoV1eEJ4/REQf0cpCdGTg0C+kJ7ZoLakd5Fc+li0mYjSqtH7oclrjND5sxoPuFgyrBYv1lwnOD75EPykE8S5IUZ22hmqt29gyVDInMwR3AyvSaMJ8E1SuIz1+tiGqDuEYED1xWeICdATU0QRKTqt70oETfU7WpFLIrdBNbztKPIbdLbduvikhaQPDkO5LVZGfjwmo=

Hi Fritjof,

What about the following?

Goal forall (S I O : Type) (f : S -> I -> S * O) s l,

Forall2 (fun i o => exists s' s'', f s' i = (s'', o)) l (mealy f s l).

it says, virtually, for all pairs of `i` and `o`, they are connected by `f`. But it does not say `f` is actually used.

Sincerely Yours,

Jason Hu

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Fritjof Bornebusch <fritjof AT uni-bremen.de>
Sent: September 27, 2018 10:45 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] proof about applying a function on each element of a list using automaton

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