The Coq mailing list

[Kyle Stemen <bluelightning32 AT gmail.com>]

Good question.

Q is the rational type in coq. It is defined as Z / positive.

The Pos.of_nat function converts a natural number (which includes 0) into a positive number (does not include 0). In the case of 0, Pos.of_nat is defined to return 1.

Coq < Eval compute in (Pos.of_nat 0).
     = 1%positive
     : positive

So if you pass 0 for n, the theorem simplifies to (1/1) = (1/2) + (1/2).

On Tue, Dec 9, 2014 at 11:53 PM, Marco Servetto marco.servetto-at-gmail.com |coq-club/Example Allow| <rhl7blvknt AT sneakemail.com> wrote:

1/2n + 1/2n = 1/n for all n.
I'm wrong or this does not holds for n=0?

On 10 December 2014 at 13:51, Kyle Stemen <ncyms8r3x2 AT snkmail.com> wrote:
> I haven't found a good book or tutorial for rationals in coq. Let me know if
> you find one.
>
> Is this the proof you're looking for?
> Require Import QArith.
>
> Theorem simple: forall n:nat,
>     (1 # Pos.of_nat n) == (1 # (2*Pos.of_nat n)) + (1 # (2 * Pos.of_nat n)).
> Proof.
>   intros.
>   unfold Qplus.
>   unfold Qeq.
>   simpl.
>   rewrite -> Pos.add_diag.
>   rewrite -> Pos.mul_comm.
>   reflexivity.
> Qed.
>
> Now I've got a follow up question that maybe someone else can answer. Why
> doesn't SearchPattern find the lemmas in the Pos module?
> Coq < Require Import QArith.
> [Loading ML file z_syntax_plugin.cmxs ... done]
> [Loading ML file quote_plugin.cmxs ... done]
> [Loading ML file newring_plugin.cmxs ... done]
> [Loading ML file omega_plugin.cmxs ... done]
>
> Coq < SearchPattern (_ * _ = _ * _)%positive.
>
> Coq < Check Pos.mul_comm.
> Pos.mul_comm
>      : forall p q : positive, (p * q)%positive = (q * p)%positive
>
> Coq < SearchPattern (_ * _ = _ * _)%nat.
> mult_comm: forall n m : nat, (n * m)%nat = (m * n)%nat
> mult_assoc_reverse: forall n m p : nat, (n * m * p)%nat = (n * (m * p))%nat
> mult_assoc: forall n m p : nat, (n * (m * p))%nat = (n * m * p)%nat
>
>
> On Tue, Dec 9, 2014 at 5:51 PM, Daniel Galvez dt.galvez-at-gmail.com
> |coq-club/Example Allow| <w75rw6tgit AT sneakemail.com> wrote:
>>
>> Hello,
>>
>> A subgoal in a proof of mine is the following:
>>
>> forall n:nat, (1 # Pos.of_nat n) == (1 # (2*Pos.of_nat n)) + (1 # (2 *
>> Pos.of_nat n)).
>>
>> That is, 1/n = 1/(2n) + 1/(2n).
>>
>> The domain of discourse here is the rationals. Perhaps there is something
>> I am
>> not seeing being new to Coq, but I would expect a simple call to some
>> tactic
>> like compute to dismiss this. I make progress in the code below by doing
>> induction on n, but am at a complete as for what to do in the inductive
>> case.
>>
>> (Note that the edge case of n = 0 does not invalidate this, as Post.of_nat
>> 0 =
>> 1.)
>>
>> Require Import QArith.
>>
>> Theorem simple:
>> forall n:nat, (1 # Pos.of_nat n) == (1 # (2*Pos.of_nat n)) + (1 # (2 *
>> Pos.of_nat n)).
>> intros.
>> unfold Qplus.
>> unfold Qeq. simpl.
>> induction n.
>> simpl. reflexivity.
>>
>> Does anyone have a suggestion as to where I should look for completing
>> this
>> proof?
>>
>> Thank you,
>> Daniel Galvez
>
>