coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Removing two axioms from Raxioms.v

From: "Roland Zumkeller" <roland.zumkeller AT gmail.com>
To: milad AT cs.ru.nl
Cc: coq-club AT pauillac.inria.fr, hurkens AT sci.kun.nl
Subject: Re: [Coq-Club] Removing two axioms from Raxioms.v
Date: Wed, 23 May 2007 21:36:35 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=ijyL8uEYOKXnh0mSQy5o6U1es8r36RO/VSZ1Tov05b8QTwo8Oi7UEeYGbiahp41L7Vq81pdf1wRbDr+U/qjgTg5NE7/WjS6obk5wTuy5tN38CDiQ9lQ4o5wGby22RmZRr/IA2+abU+bmSJppuxwfVDsHeQ9A5Xa6vCQnfkSmtpk=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

I further suggest to replace the axiom
Rplus_opp_r : forall r:R, r + - r = 0
by
Rplus_opp_l : forall r:R, - r + r = 0.

Then the axiom
Rplus_comm : forall r1 r2 : R, r1 + r2 = r2 + r1
can be removed and proven as a lemma.

The proof below is taken from "H. Eves and C. V. Newsom, An
Introduction to the Foundations and Fundamental Concepts of
Mathematics, 1965" and Assia Mahboubi helped me to formalise it.

Roland

Require Import Rdefinitions.
Open Scope R_scope.

Axiom Rplus_assoc : forall r1 r2 r3:R, r1 + r2 + r3 = r1 + (r2 + r3).
Axiom Rplus_0_l : forall r:R, 0 + r = r.
Axiom Rplus_opp_l : forall r:R, -r + r = 0.

Axiom Rmult_1_l : forall r:R, 1 * r = r.
Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.

Axiom Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2
+ r1 * r3.

Lemma Rplus_opp_r : forall r:R, r + - r = 0.
intros.
rewrite <- (Rplus_0_l (r + -r)).
rewrite <- (Rplus_opp_l (-r)).
rewrite Rplus_assoc.
rewrite <- (Rplus_assoc (-r)).
rewrite Rplus_opp_l.
rewrite Rplus_0_l.
reflexivity.
Qed.

Lemma Rplus_0_r r : r + 0 = r.
intros.
rewrite <- (Rplus_opp_l r).
rewrite <- Rplus_assoc.
rewrite Rplus_opp_r.
apply Rplus_0_l.
Qed.

Lemma Rplus_eq_reg_l r r1 r2 : r + r1 = r + r2 -> r1 = r2.
intros.
rewrite <- (Rplus_0_l r1).
rewrite <- (Rplus_0_l r2).
rewrite <- (Rplus_opp_l r).
do 2 rewrite Rplus_assoc.
rewrite H.
reflexivity.
Qed.

Lemma Rplus_eq_reg_r r r1 r2 : r1 + r = r2 + r -> r1 = r2.
intros.
rewrite <- (Rplus_0_r r1).
rewrite <- (Rplus_0_r r2).
rewrite <- (Rplus_opp_r r).
do 2 rewrite <- Rplus_assoc.
rewrite H.
reflexivity.
Qed.

Lemma Rmult_plus_distr_r r1 r2 r3 : (r1 + r2) * r3 = r1 * r3 + r2 * r3.
intros.
do 3 rewrite (fun x => Rmult_comm x r3).
apply Rmult_plus_distr_l.
Qed.

Theorem Rplus_comm : forall r1 r2 : R, r1 + r2 = r2 + r1.
intros.
apply (Rplus_eq_reg_l r1).
apply (Rplus_eq_reg_r r2).
transitivity ((1+1)*(r1+r2)).
rewrite Rmult_plus_distr_l.
do 2 rewrite Rmult_plus_distr_r.
do 2 rewrite Rmult_1_l.
repeat rewrite Rplus_assoc.
reflexivity.

rewrite Rmult_plus_distr_r.
rewrite Rmult_1_l.
repeat rewrite Rplus_assoc.
reflexivity.
Qed.

--
http://www.lix.polytechnique.fr/~zumkeller/

[Coq-Club] Removing two axioms from Raxioms.v, Milad Niqui
- Re: [Coq-Club] Removing two axioms from Raxioms.v, Milad Niqui
- Re: [Coq-Club] Removing two axioms from Raxioms.v, Roland Zumkeller