The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

The problem with your first attempt is just that m was not bound
anywhere in your statement. You can fix it by saying something like

exists n m, dummy_function n = Some m

or

exists n, dummy_function n <> None

Usually, the first form will be more convenient to use.

Best

2014-11-23 8:50 GMT-05:00 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



-- 
Arthur Azevedo de Amorim