The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi,

I am trying to write a theorem that says that a function produces Some when some conditions are met.

For example, suppose the dummy_function is defined like below

Definition dummy_function (n : nat) : option nat :=

  match n with

    | 0 => None

    | _ => Some 1

  end.

When I try

Theorem dummy_theorem1 : exists n : nat, dummy_function n = Some m.

Coq says

"The reference m was not found in the current environment."

So I tried

Theorem dummy_theorem1 : exists n : nat, dummy_function n = Some _.

In this case, Coq says 

"Error: Cannot infer this placeholder."

After some attempts, I ended up with the following version

Theorem dummy_theorem1 : exists n : nat,

                         match dummy_function n with

                           | None => False

                           | Some _ => True

                         end.

I'd like to know if there is a better way to state a theorem like this.

Thanks,

Saulo Medeiros de Araujo