diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-17 15:00:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-17 15:00:17 +0000 |
commit | 977ddfd1ad41a5620fa4462ff9066f50084f06e7 (patch) | |
tree | d44861db661240eae6f29de21cf213259c55f82b /theories/Init/Logic.v | |
parent | d8e39f445103466b36a2c04cca52ddb880d9cae7 (diff) |
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
Diffstat (limited to 'theories/Init/Logic.v')
-rw-r--r-- | theories/Init/Logic.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 77af30dcb..ee14e012a 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"). |