diff options
author | 2006-04-28 14:59:16 +0000 | |
---|---|---|
committer | 2006-04-28 14:59:16 +0000 | |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/subtac/Utils.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib/subtac/Utils.v')
-rw-r--r-- | contrib/subtac/Utils.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v new file mode 100644 index 00000000..9acb10ae --- /dev/null +++ b/contrib/subtac/Utils.v @@ -0,0 +1,34 @@ +Set Implicit Arguments. + +Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. +intros. +induction t. +exact x. +Defined. + +Check proj1_sig. +Lemma subset_simpl : forall (A : Set) (P : A -> Prop) + (t : sig P), P (proj1_sig t). +Proof. +intros. +induction t. + simpl ; auto. +Qed. + +Lemma ex_pi2 : forall (A : Prop) (P : A -> Prop) (t : ex P), + P (ex_pi1 t). +intros A P. +dependent inversion t. +simpl. +exact p. +Defined. + +Notation "'forall' { x : A | P } , Q" := + (forall x:{x:A|P}, Q) + (at level 200, x ident, right associativity). + +Notation "'fun' { x : A | P } => Q" := + (fun x:{x:A|P} => Q) + (at level 200, x ident, right associativity). + +Notation "( x & y )" := (@existS _ _ x y) : core_scope. |