coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Access return values in theorem

From: fritjof AT uni-bremen.de
To: coq-club AT inria.fr
Subject: [Coq-Club] Access return values in theorem
Date: Tue, 4 Aug 2020 16:51:06 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fritjof AT uni-bremen.de; spf=Pass smtp.mailfrom=fritjof AT uni-bremen.de; spf=None smtp.helo=postmaster AT gabriel-vm-2.zfn.uni-bremen.de
Ironport-phdr: 9a23:TxJGixZxH2bXYxqWD3mGSBD/LSx+4OfEezUN459isYplN5qZoMW+bnLW6fgltlLVR4KTs6sC17OI9f++EjNfqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5zIRmsrwjct8YajIlgJ60s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKxVrhK/qRJiwIDbb52aO+dlc6PBYd8XX3ZNUtpNWyFDBI63cosBD/AGPeZdt4T9qUEOrRqiBQmuA+PvxCRFhmLw3a07yuguChvG0xIlH90QtnTYtsj6O7kUXOuow6bG0S/NYOlK2Tfh9ofIaBYhrOmIUL90bMfcx0YhGx7Fg1mOqoHrPy2Z2OQQvmWa4OdsS+KihnIjpg1srDahxtoghpfUi4wV11zJ6Dh1zYg2KNC5TkNwfN2qEINIui2HOYZ7TdkuT3x0tCok0LELuYK3cDIXxJkl3xLTdvKKfoeS7h7+SOqdPy10iGx4dL+8nRq+71WsxvH6W8KpylhFtDBFncPJtn0V1xzc9MyHSvxl80euwzmAzBrT6uBaLkAwjKbbNZshzqcumpYJsEXDECn2lF/rjK+Qd0Uo4/On6/75bbXjuJCcMZV4hRzgPag2m8y/B/o3MhQWUmSG9+mx26fv8VDlTLlUlPE7krXVvIrHKckZvqK5BhVa0ocn6xaxFTem19EYkGEJLFJfeRKHk4rpO1bAIP3jEPe/hVWsnC5wyPDcILLhB4vCLn7ZnLj8Y7lx81RcxxYrzdBD+5JUDakML+70Wk/ordDXEhs5MxGvzOv8E9V81oYeWXqVDaODMaPSt0WI5uM1LOWWao8VomW1F/9w7Pn3yHQ9hFU1fK+z3JJRZmrrMO5hJhCXe3vwgNAPOXoMv080VuHvhVvEXTMAND6JQ6sg62RjW8qdBoDZS9X12eDT7GKABpRTI1t+JBWUC36xKteZXfZJYjifJ8Jn1DAJB+D4Gt0RkCq2vQq/8IJJa+/d+ykWr5XmjYUn+uvS0Bso+Dl5CYKR3jPUFjwmriYzXzYzmZtHjwl9x1OEivIqjPVSD91e47ZXV0Jgc4zSyapnDdG3UBjMe9qPDlqrEI2r

Hi,

I have the following definition fsm : state -> state.

The state is defined as
Inductive state :=
| State : a -> b -> state

I want to show something like:
Theorem foo:
forall s : state,
State a' b' = fsm s -> (exists a', a' = green).

In a more informal way:
I want to show that there is a state. returned by *fsm s* where
a' is green.

The answer from Coq is: The reference a' was not found in the current
environment.

Does someone has a solution for that?

Regards,
--f.

[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