The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

> if a predicate "p" holds for "f s i" than it also holds for every element in "mealy f s l".

This is not true in general though. Your function is effectively a scan operation over a state monad. What I suggested is a closer thing to what you probably want and is provable.

Other way is to define an inductive definition which captures relation between `s` `f` `l` and `mealy f s l`. But this sounds like an overshoot for this problem.

Sincerely Yours,

Jason Hu

---

From: Fritjof Bornebusch <fritjof.bornebusch AT dfki.de>
Sent: October 1, 2018 6:49 AM
To: Jason -Zhong Sheng- Hu
Cc: Fritjof Bornebusch; coq-club AT inria.fr
Subject: Re: [Coq-Club] proof about applying a function on each element of a list using automaton

 

On Thu, Sep 27, 2018 at 03:19:27PM +0000, Jason -Zhong Sheng- Hu wrote:
> Hi Fritjof,
>

hi,
 
> 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.
>

thank you for your reply. I though a little bit like this:
if a predicate "p" holds for "f s i" than it also holds for every element in "mealy f s l".
but I don't know how I can write this in coq.

> Sincerely Yours,
>
> Jason Hu

--f.

> ________________________________
> 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.