coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Moore state machine output function for every new state

From: Fritjof Bornebusch <fritjof.bornebusch AT dfki.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Moore state machine output function for every new state
Date: Thu, 7 Jan 2021 15:20:24 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=fritjof.bornebusch AT dfki.de; spf=Pass smtp.mailfrom=fritjof.bornebusch AT dfki.de; spf=None smtp.helo=postmaster AT lnv-91185.sb.dfki.de
Ironport-phdr: 9a23:xcmF0RNw/qIV0haufrwl6mtUPXoX/o7sNwtQ0KIMzox0Ivr+rarrMEGX3/hxlliBBdydt6sbzbCK6eu9BiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+Ngu6oArPusUZgYZvKLs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxVoByvuQFxzY3bb46JKfVzZb/dcc8ASGZdQspdSy5MD4WhZIUPFeoBOuNYopH9qVsUrBu+GQusBOThyjRVm3L22rc60+I/Hg7dwQwgBM4BsHTJp9jyOqcSS+G1zLXKzTXEYfNawyzy6I/SchAnv/6DRq9wcdHNxkkvDA7Kk1uQqY/kPz+Py+sCrXGW4ux9Xu2gl2ApsRt+oiSzxsgykInJgJoYxF/a+Cll3Is4J9K1RkBmbNOqDZddqi6XOoVqTs4iTGxlpik0xLMHtJO1cyYHyJYqywLDZvCZb4WF7A7vWumfLzp+mXlre6q/ig6v/UWuxeDwTM253VdQoiZYltTAq2oB2wHQ58WHUvdw/UWs1SyS2wzN5OxIO104mbbHJ5I7zbM9kpweulnZECDsgkX5lqqWe10k+ue27+TnZa3rppuaN49qkw3zNrkiltG8DOk4KAQORHOU9f6h273t/k35Qa9GgeAonaXBsZDaI9oUprKhDgNI3Isu5AyzAjOn3dgCgHUKKE9JdAiag4XqO1zCOPX4Au2+g1Sonjdr3ffGPrj5D5XDNHjDkavhfbR6605S0gY81tdf54hSCr4fO/3zR1Txu8DYDhIiLgO0zeXnCNRn2owDR22DGrWZP7/KsV+U+uIvJPGBa5MSuDbkMvQq+/rujWIillIGZqmo3Z4XaGiiEfh8IkWZZ2DsgtYbHmsQsAo+Vr+itFrXWjlKIn22QqgU5zchCYvgA52QaJqqhemvxianHJpYLkpBEFaBG2rzfIXMD/kWaT6QJcEnmDseU7WrVpQq1Tmiugz7jbZqeLmHshYEvI7ugYAmr9bYkgs/oGQtXpatllqVRmQxpVsmAjo/3aRxu0t4mwWP36t5xfBVR4UKuqF5FzwiPJuZ9NRUTtD/XgWbJIWNTkjjE4z/UWx3Vdh3z9ENYgBxFof610yR72+RG7YQ0oezKtks6KuNjXT/JMc7x3uUjKQ=

Hi,

I want to check that the Moore state machine calls the output function (of)
for
every new state.

tf means transition function
s are the individual states
i are the inputs the new state is computed from

Fixpoint moore {S I O:Type} (tf: S -> I -> S) (of: S -> O) (s: S) (l:
list(I)) : list(O) :=
match l with
| [] => nil
| i::is => let s' := tf s i in
let o := of s' in
o :: moore tf of s' is
end.

Theorem mooreMachineNotEmptyList:
forall {S I O:Type} (tf : S -> I -> S) (of : S -> O),
forall s : S,
forall i : I,
forall o : O,
forall is : list(I),
let s' := tf s i in
let os := moore tf of s is in
is <> [] -> In o os -> o = of s'.
Proof.
....
Qed.

But I'm unable to verify this.
Am I missing something?

I came up with the following idea, but it seems a bit curious:

Theorem mooreMachineNotEmptyList1:
forall {S I O:Type} (tf : S -> I -> S) (of : S -> O),
forall s s' : S,
forall i : I,
forall is : list(I),
let s' := tf s i in
moore tf of s (i::is) = of s' :: moore tf of s' is.

Kind Regards,
fritjof

[Coq-Club] Moore state machine output function for every new state, Fritjof Bornebusch, 01/07/2021
- Re: [Coq-Club] Moore state machine output function for every new state, Dominique Larchey-Wendling, 01/07/2021
  - Re: [Coq-Club] Moore state machine output function for every new state, Jim Fehrle, 01/07/2021