coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Access return values in theorem

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Access return values in theorem
Date: Wed, 5 Aug 2020 10:30:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f52.google.com
Ironport-phdr: 9a23:9BmaaRVfVyuSjAvuo+v/IP1D5pTV8LGtZVwlr6E/grcLSJyIuqrYbBOPt8tkgFKBZ4jH8fUM07OQ7/m+HzNQqs7d+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi3oAnLtMQbgoRuJro+xxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKiU0+3/LhMNukK1boQqhpx1hzI7SfIGVL+d1cqfEcd8HWWZNQsNdWipcCY2+coQPFfIMMulWr4b/p1UAoxiwCxSyCuzzxTFFnWP23bQg3ug9DQ3KwA4tEtQTu3rUttX1M6ISXPivwqnJ0zrDdelW1ing44XWdRAhvOuMXa5xccXP1EkkCgTIjk2RqYP7JTOVzPoCv3KH4OpnSOKvkXInqwBvrTiy3coshYzJiZgUylDA7yl23IE1JdihRUN9fNWrH4deuTuAOItqXsMtXXtouCAix7AYp5K1fCgHxYk7yxPDZPKKc5WF7w7iWeuPLzp1i31rdbCjixuz9UWuxPPwWtS23VhEsydLndnCum0Q2hHQ5cWKTOZ28ES52TuXyQzf9uVJLVo3mKfbMZIt3789m5sJvUnDACP7nlj9grWMeUU+4Oeo7vzqYrX4qZ+YMI95kgT+Pb4vmsy7GOg4Mw8OU3WC9eSy1LDv41f1QLpNjv0xnanZtI7VKd4Hqa6+Bg9Zyocj6xChADe6yNkUg2ULIVZfdB+Ej4XlIUzCLfH5APulg1mgji9nx/XcMb3gBpXNIGLDkLDkfbtl805cyRQ8zcpF551KEL0OPPXzWlLrtNzEDx82LRG0zv3oCNV4zIweWGaPDrWFP6PVtF+E/vgvLPWUZI8JpDb9LOAo6OLpjX8ggFMSYa2p3YYMZ32jBfRnI0CZYWL2jdsbEGcKuBA+TO3wh1GYXz5TfSX6Y6VpzTYiQKmiEI2LEouqmfmK2DqxNpxQfGFPTF6WRyTGbYKBDs8NZTiIL4dKlSEeSbmsVsd1zRCjrhX3jbFgM/DI+yAFnZ3m3dlxoebUkEdhpnRPE82B3jTVHClPlWQSSmpzhfgn+BEv+hK4yaF9xsdgO5lT6vdOCFpoMJfdy6l7DIm3VF+bONiOT1miT5OtBjRjFottke9LWF50HpCZtj6GxzCjWuZHmLmCBZhy+aXZjSCodpRNjk3e3axktGEIB85GNGmonKl6rlGBCIvAkkHfnKGvJ/0R

Le mar. 4 août 2020 à 17:53, <fritjof AT uni-bremen.de> a écrit :
>
> On Tue, Aug 04, 2020 at 05:24:19PM +0200, Castéran Pierre wrote:
> > Hi,
> > 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.
> >
>
> Hmm, this would indicate that for all a' the result is green right?
> But, I didn't know that "match" could be used in a theorem.

No, it says that for all *s* the result of (fsm s) is green.

Can you give in english the property you want to prove please? Your
formulas make no sense imho.

> I'm thinking more about formulating a liveness property.

That would need to state something about reapplying fsm to its result
a finite number of time I suppose. This does not appear in your
definitions.

Best
Pierre Courtieu

[Coq-Club] Access return values in theorem, fritjof, 08/04/2020
- Re: [Coq-Club] Access return values in theorem, Castéran Pierre, 08/04/2020
  - Re: [Coq-Club] Access return values in theorem, fritjof, 08/04/2020
    - Re: [Coq-Club] Access return values in theorem, Pierre Courtieu, 08/05/2020
    - Re: [Coq-Club] Access return values in theorem, Castéran Pierre, 08/05/2020