The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi,

It seems to me 

length (moore .... is) = length is 

hence is <> [] is redundant with In o os. 
Then I see no reason why os should only 
contains copies of the value (of s') 
...

Best,

Dominique

----- Mail original -----
> De: "Fritjof Bornebusch" <fritjof.bornebusch AT dfki.de>
> À: "coq-club" <coq-club AT inria.fr>
> Envoyé: Jeudi 7 Janvier 2021 15:20:24
> Objet: [Coq-Club] Moore state machine output function for every new state

> 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