The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Hi Artur,

Thanks for your help. I have tried your suggestions and they indeed work. However, when I try to prove the theorem looks like I need to know what is the value of m.

Here is the first version of the theorem and its proof:

Theorem dummy_theorem1 : exists n : nat, match dummy_function n with

  | None => False

  | Some _ => True

end.

Proof.

exists 1.

reflexivity.

Qed.

Here is the second version:

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

Proof.

exists 1.

reflexivity.

Qed.

But Coq says

"Tactic failure: The relation ex is not a declared reflexive relation. Maybe you need to require the Setoid library.Compilation output:"

, probably because I did not specify the value of m.

Coq accepts the proof below. But this requires that I know the specific value that is inside the option produce by (dummy_function 1).

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

Proof.

exists 1.

exists 1.

reflexivity.

Qed.

Your second suggestion (exists n, dummy_function n <> None) is really nice but my problem is a little more complicated than dummy_function because my (real) theorem says something about the value that is inside the option produced by a function.

I tried to formulate my doubts using dummy_function as an example, but I simplified the problem too much.

Thanks for your help!

Saulo

On Sun, Nov 23, 2014 at 11:31 AM, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

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