The Coq mailing list

[Fritjof Bornebusch <fritjof.bornebusch AT dfki.de>]

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.