The Coq mailing list

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

Hello,

Well, if I guess the property you want to prove, it may be like as follows :

Inductive Green : state -> Prop :=

  green1 : forall c w, Green (State c w tramGreen)

 | green2 : forall c t,  Green (State c walkerGreen t)

 | green3 : forall t w, Green (State carGreen t w).

Hint Constructors Green : core.

Fixpoint iterate {A:Type}(f : A -> A) (n: nat)(x:A) :=

  match n with

  | 0 => x

  | S p =>  (iterate  f p (f x))

  end.

Definition green_acc s := exists n:nat, Green (iterate_t  fsm n s).

Lemma green_acc_trans : forall s , green_acc (fsm s) -> green_acc s.

Proof. intros s [n H]. now exists (S n). Qed.

Then you prove the proposition forall s, green_acc s, following the structure of fsm (avoiding to consider all the 16 possible values of s).

If you prefer to consider the transition as relations, you can reason with reflexive and transitive closures (cf  https://coq.inria.fr/distrib/current/stdlib/Coq.Relations.Operators_Properties.html )

Hope that helps,

Pierre

Le 4 août 2020 à 17:53, fritjof AT uni-bremen.de a écrit :

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.