diff options
Diffstat (limited to 'theories/Init/Logic_Type.v')
| -rw-r--r-- | theories/Init/Logic_Type.v | 25 |
1 files changed, 15 insertions, 10 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index c4e5f6c7..1333f354 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Logic_Type.v 10840 2008-04-23 21:29:34Z herbelin $ i*) +(*i $Id$ i*) (** This module defines type constructors for types in [Type] ([Datatypes.v] and [Logic.v] defined them for types in [Set]) *) @@ -28,23 +28,23 @@ Section identity_is_a_congruence. Variable f : A -> B. Variables x y z : A. - - Lemma sym_id : identity x y -> identity y x. + + Lemma identity_sym : identity x y -> identity y x. Proof. destruct 1; trivial. Defined. - Lemma trans_id : identity x y -> identity y z -> identity x z. + Lemma identity_trans : identity x y -> identity y z -> identity x z. Proof. destruct 2; trivial. Defined. - Lemma congr_id : identity x y -> identity (f x) (f y). + Lemma identity_congr : identity x y -> identity (f x) (f y). Proof. destruct 1; trivial. Defined. - Lemma sym_not_id : notT (identity x y) -> notT (identity y x). + Lemma not_identity_sym : notT (identity x y) -> notT (identity y x). Proof. red in |- *; intros H H'; apply H; destruct H'; trivial. Qed. @@ -53,17 +53,22 @@ End identity_is_a_congruence. Definition identity_ind_r : forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y. - intros A x P H y H0; case sym_id with (1 := H0); trivial. + intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. Definition identity_rec_r : forall (A:Type) (a:A) (P:A -> Set), P a -> forall y:A, identity y a -> P y. - intros A x P H y H0; case sym_id with (1 := H0); trivial. + intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. Definition identity_rect_r : forall (A:Type) (a:A) (P:A -> Type), P a -> forall y:A, identity y a -> P y. - intros A x P H y H0; case sym_id with (1 := H0); trivial. + intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. -Hint Immediate sym_id sym_not_id: core v62. +Hint Immediate identity_sym not_identity_sym: core v62. + +Notation refl_id := identity_refl (only parsing). +Notation sym_id := identity_sym (only parsing). +Notation trans_id := identity_trans (only parsing). +Notation sym_not_id := not_identity_sym (only parsing). |