The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

Consider the following definition of ceval and the progress theorem below.


Inductive ceval : com -> state -> state -> Prop :=
  (*| E_Skip : forall st,
      SKIP / st || st*)
  | E_Ass  : forall st a1 n x,
      aeval st a1 = n ->
      (x ::= a1) / st || (update st x n)
  | E_Seq : forall c1 c2 st st' st'',
      c1 / st  || st' ->
      c2 / st' || st'' ->
      (c1 ;; c2) / st || st''
  | E_IfTrue : forall st st' b c1 c2,
      beval st b = true ->
      c1 / st || st' ->
      (IFB b THEN c1 ELSE c2 FI) / st || st'
  | E_IfFalse : forall st st' b c1 c2,
      beval st b = false ->
      c2 / st || st' ->
      (IFB b THEN c1 ELSE c2 FI) / st || st'
  | E_WhileEnd : forall b st c,
      beval st b = false ->
      (WHILE b DO c END) / st || st
  | E_WhileLoop : forall st st' st'' b c,
      beval st b = true ->
      c / st || st' ->
      (WHILE b DO c END) / st' || st'' ->
      (WHILE b DO c END) / st || st''

  where "c1 '/' st '||' st'" := (ceval c1 st st').

Theorem cevalWhileProgress : forall b c w,
    (forall st, exists st', ceval c st st') ->
    w = (WHILE b DO c END) ->
    (forall st, exists st', ceval w st st').
Proof.
 ???????????
(Note that auxiliary definitions come from the Software Foundations Imp.v source file)

What would be the best way of setting up a proof of this theorem?  The ideal thing would be to do an induction on a hypothesis of type "ceval w st st'".  However, this term is in the conclusion.  Any alternative suggestions?

                    - Ken