The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I don't see how this could possibly be true if, for example, b always evaluates to true.  Take this with a grain of salt as I'm not too familiar with this, but: I'd suppose that to prove a WHILE statement terminates, you typically give some well-founded ordering on states (for example by comparing the values of some measure function to nat), and then prove something like beval st b = true -> exists st', st' < st /\ ceval c st st'.  Then the proof, roughly, would go by induction on (Acc (<) st): if beval st b = false, you use E_WhileEnd.  Otherwise, if beval st b = true, you use the progress statement on c to get st', and since st' < st, the WHILE statement terminates with starting state st' by induction.  Then the constructor E_WhileLoop gives WHILE terminating with starting state st.

-- 

Daniel Schepler

On Fri, Jan 24, 2014 at 3:51 PM, Kenneth Roe <kendroe AT hotmail.com> wrote:

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