The Coq mailing list

[Castéran Pierre <pierre.casteran AT gmail.com>]

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.

 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.

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

Best regards,

Pierre


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