diff options
Diffstat (limited to 'theories/Sets/Uniset.v')
| -rw-r--r-- | theories/Sets/Uniset.v | 34 |
1 files changed, 16 insertions, 18 deletions
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 48789f9a..6e38b5e5 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Uniset.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** Sets as characteristic functions *) (* G. Huet 1-9-95 *) @@ -53,37 +51,37 @@ Hint Unfold seq. Lemma leb_refl : forall b:bool, leb b b. Proof. -destruct b; simpl in |- *; auto. +destruct b; simpl; auto. Qed. Hint Resolve leb_refl. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. Proof. -unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. +unfold incl; intros s1 s2 E a; elim (E a); auto. Qed. Lemma incl_right : forall s1 s2:uniset, seq s1 s2 -> incl s2 s1. Proof. -unfold incl in |- *; intros s1 s2 E a; elim (E a); auto. +unfold incl; intros s1 s2 E a; elim (E a); auto. Qed. Lemma seq_refl : forall x:uniset, seq x x. Proof. -destruct x; unfold seq in |- *; auto. +destruct x; unfold seq; auto. Qed. Hint Resolve seq_refl. Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. Proof. -unfold seq in |- *. -destruct x; destruct y; destruct z; simpl in |- *; intros. +unfold seq. +destruct x; destruct y; destruct z; simpl; intros. rewrite H; auto. Qed. Lemma seq_sym : forall x y:uniset, seq x y -> seq y x. Proof. -unfold seq in |- *. -destruct x; destruct y; simpl in |- *; auto. +unfold seq. +destruct x; destruct y; simpl; auto. Qed. (** uniset union *) @@ -92,20 +90,20 @@ Definition union (m1 m2:uniset) := Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). Proof. -unfold seq in |- *; unfold union in |- *; simpl in |- *; auto. +unfold seq; unfold union; simpl; auto. Qed. Hint Resolve union_empty_left. Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). Proof. -unfold seq in |- *; unfold union in |- *; simpl in |- *. +unfold seq; unfold union; simpl. intros x a; rewrite (orb_b_false (charac x a)); auto. Qed. Hint Resolve union_empty_right. Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). Proof. -unfold seq in |- *; unfold charac in |- *; unfold union in |- *. +unfold seq; unfold charac; unfold union. destruct x; destruct y; auto with bool. Qed. Hint Resolve union_comm. @@ -113,14 +111,14 @@ Hint Resolve union_comm. Lemma union_ass : forall x y z:uniset, seq (union (union x y) z) (union x (union y z)). Proof. -unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z; auto with bool. Qed. Hint Resolve union_ass. Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). Proof. -unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. @@ -128,7 +126,7 @@ Hint Resolve seq_left. Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). Proof. -unfold seq in |- *; unfold union in |- *; unfold charac in |- *. +unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. @@ -212,4 +210,4 @@ i*) End defs. -Unset Implicit Arguments.
\ No newline at end of file +Unset Implicit Arguments. |