diff options
author | 2003-03-29 16:47:26 +0000 | |
---|---|---|
committer | 2003-03-29 16:47:26 +0000 | |
commit | 7bdfef00a00a6c7403166bcaadc9cdfcd0e92451 (patch) | |
tree | c8e57c7de1998e89ed48289f8fb015fd7fa022f9 /theories/Init/Logic_Type.v | |
parent | b2f779cf923cab0d5c8990678fd9568250e014c8 (diff) |
eq fusionne avec eqT et devient par défaut sur Type,
idem pour ex et exT, ex2 et exT2, all et allT
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Init/Logic_Type.v')
-rwxr-xr-x | theories/Init/Logic_Type.v | 43 |
1 files changed, 40 insertions, 3 deletions
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index e4982c1f6..de4d2721f 100755 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -18,7 +18,11 @@ Require LogicSyntax. (** [allT A P], or simply [(ALLT x | P(x))], stands for [(x:A)(P x)] when [A] is of type [Type] *) +(* Definition allT := [A:Type][P:A->Prop](x:A)(P x). +*) + +Syntactic Definition allT := all. Section universal_quantification. @@ -27,7 +31,7 @@ Variable P : A->Prop. Theorem inst : (x:A)(allT ? [x](P x))->(P x). Proof. -Unfold allT; Auto. +Unfold all; Auto. Qed. Theorem gen : (B:Prop)(f:(y:A)B->(P y))B->(allT A P). @@ -45,12 +49,23 @@ End universal_quantification. (** [exT2 A P Q], or simply [(EXT x | P(x) & Q(x))], stands for the existential quantification on both [P] and [Q] when [A] is of type [Type] *) - +(* Inductive exT [A:Type;P:A->Prop] : Prop := exT_intro : (x:A)(P x)->(exT A P). +*) + +Syntactic Definition exT := ex. +Syntactic Definition exT_intro := ex_intro. +Syntactic Definition exT_ind := ex_ind. +(* Inductive exT2 [A:Type;P,Q:A->Prop] : Prop := exT_intro2 : (x:A)(P x)->(Q x)->(exT2 A P Q). +*) + +Syntactic Definition exT2 := ex2. +Syntactic Definition exT_intro2 := ex_intro2. +Syntactic Definition exT2_ind := ex2_ind. (** Leibniz equality : [A:Type][x,y:A] (P:A->Prop)(P x)->(P y) @@ -58,11 +73,20 @@ Inductive exT2 [A:Type;P,Q:A->Prop] : Prop type [Type]. This equality satisfies reflexivity (by definition), symmetry, transitivity and stability by congruence *) + +(* Inductive eqT [A:Type;x:A] : A -> Prop := refl_eqT : (eqT A x x). -Hints Resolve refl_eqT exT_intro2 exT_intro : core v62. +Hints Resolve refl_eqT (* exT_intro2 exT_intro *) : core v62. +*) +Syntactic Definition eqT := eq. +Syntactic Definition refl_eqT := refl_equal. +Syntactic Definition eqT_ind := eq_ind. +Syntactic Definition eqT_rect := eq_rect. +Syntactic Definition eqT_rec := eq_rec. +(* Section Equality_is_a_congruence. Variables A,B : Type. @@ -91,11 +115,19 @@ Section Equality_is_a_congruence. Qed. End Equality_is_a_congruence. +*) +Syntactic Definition sym_eqT := sym_eq. +Syntactic Definition trans_eqT := trans_eq. +Syntactic Definition congr_eqT := f_equal. +Syntactic Definition sym_not_eqT := sym_not_eq. +(* Hints Immediate sym_eqT sym_not_eqT : core v62. +*) (** This states the replacement of equals by equals *) +(* Definition eqT_ind_r : (A:Type)(x:A)(P:A->Prop)(P x)->(y:A)(eqT ? y x)->(P y). Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. @@ -107,6 +139,11 @@ Defined. Definition eqT_rect_r : (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eqT ? y x)->(P y). Intros A x P H y H0; Case sym_eqT with 1:=H0; Trivial. Defined. +*) + +Syntactic Definition eqT_ind_r := eq_ind_r. +Syntactic Definition eqT_rec_r := eq_rec_r. +Syntactic Definition eqT_rect_r := eq_rect_r. (** Some datatypes at the [Type] level *) |