From 977ddfd1ad41a5620fa4462ff9066f50084f06e7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Apr 2013 15:00:17 +0000
Subject: Added group properties of eq_refl, eq_sym, eq_trans

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16413 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Logic.v | 39 +++++++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 77af30dcba..ee14e012ae 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -416,6 +416,45 @@ Proof.
   destruct 1; destruct 1; destruct 1; destruct 1; destruct 1; reflexivity.
 Qed.
 
+Theorem f_equal_compose : forall A B C (a b:A) (f:A->B) (g:B->C) (e:a=b),
+  f_equal g (f_equal f e) = f_equal (fun a => g (f a)) e.
+Proof.
+  destruct e. reflexivity.
+Defined.
+
+(** The goupoid structure of equality *)
+
+Theorem eq_trans_refl_l : forall A (x y:A) (e:x=y), eq_trans eq_refl e = e.
+Proof.
+  destruct e. reflexivity.
+Defined.
+
+Theorem eq_trans_refl_r : forall A (x y:A) (e:x=y), eq_trans e eq_refl = e.
+Proof.
+  destruct e. reflexivity.
+Defined.
+
+Theorem eq_sym_involutive : forall A (x y:A) (e:x=y), eq_sym (eq_sym e) = e.
+Proof.
+  destruct e; reflexivity.
+Defined.
+
+Theorem eq_trans_sym_inv_l : forall A (x y:A) (e:x=y), eq_trans (eq_sym e) e = eq_refl.
+Proof.
+  destruct e; reflexivity.
+Defined.
+
+Theorem eq_trans_sym_inv_r : forall A (x y:A) (e:x=y), eq_trans e (eq_sym e) = eq_refl.
+Proof.
+  destruct e; reflexivity.
+Defined.
+
+Theorem eq_trans_assoc : forall A (x y z t:A) (e:x=y) (e':y=z) (e'':z=t),
+  eq_trans e (eq_trans e' e'') = eq_trans (eq_trans e e') e''.
+Proof.
+  destruct e''; reflexivity.
+Defined.
+
 (* Aliases *)
 
 Notation sym_eq := eq_sym (compat "8.3").
-- 
cgit v1.2.3