Init/Logic: commutativity and associativity of /\ and \/

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12643 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 0 deletions

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index e1bb443a63..4fca1d1dbb 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -112,6 +112,16 @@ Proof.
 intros; tauto.
 Qed.
 
+Theorem and_comm : forall A B : Prop, A /\ B <-> B /\ A.
+Proof.
+intros; tauto.
+Qed.
+
+Theorem and_assoc : forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C.
+Proof.
+intros; tauto.
+Qed.
+
 Theorem or_cancel_l : forall A B C : Prop,
   (B -> ~ A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
 Proof.
@@ -124,6 +134,16 @@ Proof.
 intros; tauto.
 Qed.
 
+Theorem or_comm : forall A B : Prop, (A \/ B) <-> (B \/ A).
+Proof.
+intros; tauto.
+Qed.
+
+Theorem or_assoc : forall A B C : Prop, (A \/ B) \/ C <-> A \/ B \/ C.
+Proof.
+intros; tauto.
+Qed.
+
 (** Backward direction of the equivalences above does not need assumptions *)
 
 Theorem and_iff_compat_l : forall A B C : Prop,