The Coq mailing list

[fritjof AT uni-bremen.de]

On Tue, Aug 04, 2020 at 05:24:19PM +0200, Castéran Pierre wrote:
> Hi,
>

Hi,
   
> I’m not sure I understand well  what you mean.
> 
> First, It, would be better to include in your mail the declarations and 
> definitions you want to use.
> 

thank you for your answer. No problem:

Inductive trafficLightCar:=
    | carRed
    | carYellow
    | carGreen
    | carRedYellow.

Inductive trafficLightWalker:=
    | walkerRed
    | walkerGreen.

Inductive trafficLightTram:=
    | tramRed
    | tramGreen.


Inductive state :=
    | State : trafficLightCar -> trafficLightWalker -> trafficLightTram -> 
state.


Definition fsm (s : state) : state :=
    match s with
     | State carRed walkerRed tramRed => State carRed walkerRed tramGreen 
     | State carRed walkerRed tramGreen => State carRedYellow walkerRed 
tramRed
     | State carRedYellow walkerRed tramRed => State carGreen walkerRed 
tramRed
     | State carGreen walkerRed tramRed => State carYellow walkerRed tramRed
     | State carYellow walkerRed tramRed => State carRed walkerGreen tramRed
     | State _ _ _ => State carRed walkerRed tramRed
    end.

>  Do you agree with the following ones ?
> 
> Variables a b: Type.
> Variable green: a.
> Inductive state :=
>    | State : a -> b -> state.
> 
> Variable fsm : state -> state. 
> 
> Now, if s is any state, you can decompose it with a match.
> Since fsm is a function, (fsm s) is a single value, the first component of 
> which is (or not) green. 
> So I don’t understand the need for an existential quantifier.
> 
> What do you think about the following statement ? Is it what you meant ?
> 
> Theorem foo:
>   forall (s : state),
>          match fsm s with (State a' b') => a' = green end.
> 

Hmm, this would indicate that for all a' the result is green right?
But, I didn't know that "match" could be used in a theorem.

I'm thinking more about formulating a liveness property.

> Now, if fsm is a binary relation, instead of a function, then my answer 
> would have been different.
> 
> Best regards,
> 
> Pierre
> 
> 

Best regards,
--f.

> > Le 4 août 2020 à 16:51, fritjof AT uni-bremen.de a écrit :
> > 
> > Hi,
> > 
> > I have the following definition fsm : state -> state.
> > 
> > The state is defined as
> >  Inductive state :=
> >    | State : a -> b -> state
> > 
> > I want to show something like:
> > Theorem foo:
> >  forall s : state,
> >  State a' b' = fsm s -> (exists a', a' = green).
> > 
> > 
> > In a more informal way:
> > I want to show that there is a state. returned by *fsm s* where
> > a' is green.
> > 
> > The answer from Coq is: The reference a' was not found in the current 
> > environment.
> > 
> > Does someone has a solution for that?
> > 
> > Regards,
> > --f.
>