The Coq mailing list

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

2014-11-23 9:55 GMT-05:00 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.

For simple cases like that, eauto takes care of the job, and you don't
have to actually provide the value of m:

Lemma foo : exists n m, dummy_function n = Some m.
Proof.
  exists 1. simpl. eauto.
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.

If you need to state lots of properties about the value that is
produced by your function, it's probably better to use a custom
inductive instead of combining them with lots of conjunctions and
existentials in an ad-hoc way:

Inductive foo :=
| Foo : forall n m, dummy_function n = Some m ->
  P m ->
  Q m ->
  (* .... *)
  foo.

Best


>
> 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
>
>



-- 
Arthur Azevedo de Amorim