coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Progress theorem

From: Daniel Schepler <dschepler AT gmail.com>
To: Andrew Hirsch <akhirsch AT cs.cornell.edu>
Cc: coq-club AT inria.fr, Kenneth Roe <kendroe AT hotmail.com>
Subject: Re: [Coq-Club] Progress theorem
Date: Fri, 24 Jan 2014 19:12:08 -0800

On Friday, January 24, 2014 05:28:48 PM Andrew Hirsch wrote:
> Daniel: I'm relatively certain that would be true even if b always
> evaluates to true. Note that it is a progress theorem, not a termination
> theorem.
>
> Kenneth: Will an induction on ceval c st st' not work?
>
> -Andrew

OK, then I'm not sure what you mean by "progress". To me, looking at the
definition of ceval, it looks pretty much exactly like what I'd write for
"program c when starting in state st terminates in state st'".
--
Daniel Schepler

[Coq-Club] Progress theorem, Kenneth Roe, 01/25/2014
- Re: [Coq-Club] Progress theorem, Daniel Schepler, 01/25/2014
  - Re: [Coq-Club] Progress theorem, Andrew Hirsch, 01/25/2014
    - Re: [Coq-Club] Progress theorem, Daniel Schepler, 01/25/2014