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

[Fritjof Bornebusch]

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.

[Jason -Zhong Sheng- Hu]

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-***@inria.fr <coq-club-***@inria.fr> on behalf of Fritjof Bornebusch <***@uni-bremen.de>
Sent: September 27, 2018 10:45 AM
To: coq-***@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.

[Fritjof Bornebusch]

Post by Jason -Zhong Sheng- Hu
Hi Fritjof,

hi,

Post by Jason -Zhong Sheng- Hu
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.

Post by Jason -Zhong Sheng- Hu
Sincerely Yours,
Jason Hu

--f.

Post by Jason -Zhong Sheng- Hu
________________________________
Sent: September 27, 2018 10:45 AM
Subject: [Coq-Club] proof about applying a function on each element of a list using automaton
Hi,
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).
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.

[Jason -Zhong Sheng- Hu]

Post by Fritjof Bornebusch
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 <***@dfki.de>
Sent: October 1, 2018 6:49 AM
To: Jason -Zhong Sheng- Hu
Cc: Fritjof Bornebusch; coq-***@inria.fr
Subject: Re: [Coq-Club] proof about applying a function on each element of a list using automaton

Post by Fritjof Bornebusch
Hi Fritjof,

hi,

Post by Fritjof Bornebusch
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.

Post by Fritjof Bornebusch
Sincerely Yours,
Jason Hu

--f.

Post by Fritjof Bornebusch
________________________________
Sent: September 27, 2018 10:45 AM
Subject: [Coq-Club] proof about applying a function on each element of a list using automaton
Hi,
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).
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.

[Fritjof Bornebusch]

Post by Jason -Zhong Sheng- Hu

Post by Fritjof Bornebusch
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.

I see. Thank you, I will give it a try.

Btw: this is a little off-top, but, what is good pattern to solve such a goal:
[...]
is' : list I
IHis' : length (mealy f s is') = length is'
______________________________________(1/1)
length (let (s', o) := f s i in o :: mealy f s' is') = Datatypes.S (length is')

If I destruct "f s i" I got something like this: length (o :: mealy f s0 is') = Datatypes.S (length is')
Now I have to deal with a "s0 = s" problem.
Or is there a more clever way to avoid such a problem in general?

Post by Jason -Zhong Sheng- Hu
Sincerely Yours,
Jason Hu

Best regards,
--f.

Post by Jason -Zhong Sheng- Hu
________________________________
Sent: October 1, 2018 6:49 AM
To: Jason -Zhong Sheng- Hu
Subject: Re: [Coq-Club] proof about applying a function on each element of a list using automaton

Post by Fritjof Bornebusch
Hi Fritjof,

hi,

Post by Fritjof Bornebusch
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.

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.

Post by Fritjof Bornebusch
Sincerely Yours,
Jason Hu

--f.

Post by Fritjof Bornebusch
________________________________
Sent: September 27, 2018 10:45 AM
Subject: [Coq-Club] proof about applying a function on each element of a list using automaton
Hi,
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).
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.

[Lily Chung]

[Fritjof Bornebusch]

<div dir='auto'>Probably you need to generalize over s in your inductive hypothesis.</div>

thank you, that does the trick.

regards,
--f.