The Coq mailing list

[Marco Servetto <marco.servetto AT gmail.com>]

Umm, this means that I can have a theorem stating that x/0=x for all x?

On 10 December 2014 at 15:09, Kyle Stemen 
<ncyms8r3x2 AT snkmail.com>
 wrote:
> 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
>> >
>> >
>
>