aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-18 14:32:00 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-10-18 14:32:00 +0000
commit1f915bf2b4edc46461fef4106f4fe77e89c3fd4f (patch)
tree368beb885e742af9ea6097ac8b0be8ad10189a5a /theories
parent586d6add6d2d4405eacf9241ee0d55f58435e364 (diff)
Intégration et formattage du développement de Pierre Castéran sur les
définitions alternatives de la transitivé d'une relation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11462 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Relations/Operators_Properties.v334
-rw-r--r--theories/Relations/Relation_Operators.v132
2 files changed, 397 insertions, 69 deletions
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 4a6d58ec2..22582f75d 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -8,13 +8,15 @@
(*i $Id$ i*)
-(****************************************************************************)
-(* Bruno Barras *)
-(****************************************************************************)
+(************************************************************************)
+(** * Some properties of the operators on relations *)
+(************************************************************************)
+(** * Initial version by Bruno Barras *)
+(************************************************************************)
Require Import Relation_Definitions.
Require Import Relation_Operators.
-
+Require Import Setoid.
Section Properties.
@@ -25,6 +27,8 @@ Section Properties.
Section Clos_Refl_Trans.
+ (** Correctness of the reflexive-transitive closure operator *)
+
Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R).
Proof.
apply Build_preorder.
@@ -33,6 +37,8 @@ Section Properties.
exact (rt_trans A R).
Qed.
+ (** Idempotency of the reflexive-transitive closure operator *)
+
Lemma clos_rt_idempotent :
incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R).
Proof.
@@ -42,32 +48,13 @@ Section Properties.
apply rt_trans with y; auto with sets.
Qed.
- Lemma clos_refl_trans_ind_left :
- forall (A:Type) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
- P M ->
- (forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
- forall a:A, clos_refl_trans A R M a -> P a.
- Proof.
- intros.
- generalize H H0.
- clear H H0.
- elim H1; intros; auto with sets.
- apply H2 with x; auto with sets.
-
- apply H3.
- apply H0; auto with sets.
-
- intros.
- apply H5 with P0; auto with sets.
- apply rt_trans with y; auto with sets.
- Qed.
-
-
End Clos_Refl_Trans.
-
Section Clos_Refl_Sym_Trans.
+ (** Reflexive-transitive closure is included in the
+ reflexive-symmetric-transitive closure *)
+
Lemma clos_rt_clos_rst :
inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R).
Proof.
@@ -76,14 +63,18 @@ Section Properties.
apply rst_trans with y; auto with sets.
Qed.
+ (** Correctness of the reflexive-symmetric-transitive closure *)
+
Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R).
Proof.
apply Build_equivalence.
exact (rst_refl A R).
exact (rst_trans A R).
- exact (rst_sym A R).
+ exact (fun x y => rst_sym A R y x).
Qed.
+ (** Idempotency of the reflexive-symmetric-transitive closure operator *)
+
Lemma clos_rst_idempotent :
incl (clos_refl_sym_trans A (clos_refl_sym_trans A R))
(clos_refl_sym_trans A R).
@@ -92,7 +83,294 @@ Section Properties.
induction 1; auto with sets.
apply rst_trans with y; auto with sets.
Qed.
-
+
End Clos_Refl_Sym_Trans.
+ Section Equivalences.
+
+ (** *** Equivalences between the different definition of the reflexive,
+ symmetric, transitive closures *)
+
+ (** *** Contributed by P. Casteran *)
+
+ (** Direct transitive closure vs left-step extension *)
+
+ Lemma t1n_trans : forall x y, clos_trans_1n A R x y -> clos_trans A R x y.
+ Proof.
+ induction 1.
+ left; assumption.
+ right with y; auto.
+ left; auto.
+ Qed.
+
+ Lemma trans_t1n : forall x y, clos_trans A R x y -> clos_trans_1n A R x y.
+ Proof.
+ induction 1.
+ left; assumption.
+ generalize IHclos_trans2; clear IHclos_trans2; induction IHclos_trans1.
+ right with y; auto.
+ right with y; auto.
+ eapply IHIHclos_trans1; auto.
+ apply t1n_trans; auto.
+ Qed.
+
+ Lemma t1n_trans_equiv : forall x y,
+ clos_trans A R x y <-> clos_trans_1n A R x y.
+ Proof.
+ split.
+ apply trans_t1n.
+ apply t1n_trans.
+ Qed.
+
+ (** Direct transitive closure vs right-step extension *)
+
+ Lemma tn1_trans : forall x y, clos_trans_n1 A R x y -> clos_trans A R x y.
+ Proof.
+ induction 1.
+ left; assumption.
+ right with y; auto.
+ left; assumption.
+ Qed.
+
+ Lemma trans_tn1 : forall x y, clos_trans A R x y -> clos_trans_n1 A R x y.
+ Proof.
+ induction 1.
+ left; assumption.
+ elim IHclos_trans2.
+ intro y0; right with y.
+ auto.
+ auto.
+ intros.
+ right with y0; auto.
+ Qed.
+
+ Lemma tn1_trans_equiv : forall x y,
+ clos_trans A R x y <-> clos_trans_n1 A R x y.
+ Proof.
+ split.
+ apply trans_tn1.
+ apply tn1_trans.
+ Qed.
+
+ (** Direct reflexive-transitive closure is equivalent to
+ transitivity by left-step extension *)
+
+ Lemma R_rt1n : forall x y, R x y -> clos_refl_trans_1n A R x y.
+ Proof.
+ intros x y H.
+ right with y;[assumption|left].
+ Qed.
+
+ Lemma R_rtn1 : forall x y, R x y -> clos_refl_trans_n1 A R x y.
+ Proof.
+ intros x y H.
+ right with x;[assumption|left].
+ Qed.
+
+ Lemma rt1n_trans : forall x y,
+ clos_refl_trans_1n A R x y -> clos_refl_trans A R x y.
+ Proof.
+ induction 1.
+ constructor 2.
+ constructor 3 with y; auto.
+ constructor 1; auto.
+ Qed.
+
+ Lemma trans_rt1n : forall x y,
+ clos_refl_trans A R x y -> clos_refl_trans_1n A R x y.
+ Proof.
+ induction 1.
+ apply R_rt1n; assumption.
+ left.
+ generalize IHclos_refl_trans2; clear IHclos_refl_trans2;
+ induction IHclos_refl_trans1; auto.
+
+ right with y; auto.
+ eapply IHIHclos_refl_trans1; auto.
+ apply rt1n_trans; auto.
+ Qed.
+
+ Lemma rt1n_trans_equiv : forall x y,
+ clos_refl_trans A R x y <-> clos_refl_trans_1n A R x y.
+ Proof.
+ split.
+ apply trans_rt1n.
+ apply rt1n_trans.
+ Qed.
+
+ (** Direct reflexive-transitive closure is equivalent to
+ transitivity by right-step extension *)
+
+ Lemma rtn1_trans : forall x y,
+ clos_refl_trans_n1 A R x y -> clos_refl_trans A R x y.
+ Proof.
+ induction 1.
+ constructor 2.
+ constructor 3 with y; auto.
+ constructor 1; assumption.
+ Qed.
+
+ Lemma trans_rtn1 : forall x y,
+ clos_refl_trans A R x y -> clos_refl_trans_n1 A R x y.
+ Proof.
+ induction 1.
+ apply R_rtn1; auto.
+ left.
+ elim IHclos_refl_trans2; auto.
+ intros.
+ right with y0; auto.
+ Qed.
+
+ Lemma rtn1_trans_equiv : forall x y,
+ clos_refl_trans A R x y <-> clos_refl_trans_n1 A R x y.
+ Proof.
+ split.
+ apply trans_rtn1.
+ apply rtn1_trans.
+ Qed.
+
+ (** Induction on the left transitive step *)
+
+ Lemma clos_refl_trans_ind_left :
+ forall (x:A) (P:A -> Prop), P x ->
+ (forall y z:A, clos_refl_trans A R x y -> P y -> R y z -> P z) ->
+ forall z:A, clos_refl_trans A R x z -> P z.
+ Proof.
+ intros.
+ revert H H0.
+ induction H1; intros; auto with sets.
+ apply H1 with x; auto with sets.
+
+ apply IHclos_refl_trans2.
+ apply IHclos_refl_trans1; auto with sets.
+
+ intros.
+ apply H0 with y0; auto with sets.
+ apply rt_trans with y; auto with sets.
+ Qed.
+
+ (** Induction on the right transitive step *)
+
+ Lemma rt1n_ind_right : forall (P : A -> Prop) (z:A),
+ P z ->
+ (forall x y, R x y -> clos_refl_trans_1n A R y z -> P y -> P x) ->
+ forall x, clos_refl_trans_1n A R x z -> P x.
+ induction 3; auto.
+ apply H0 with y; auto.
+ Qed.
+
+ Lemma clos_refl_trans_ind_right : forall (P : A -> Prop) (z:A),
+ P z ->
+ (forall x y, R x y -> P y -> clos_refl_trans A R y z -> P x) ->
+ forall x, clos_refl_trans A R x z -> P x.
+ intros.
+ rewrite rt1n_trans_equiv in H1.
+ elim H1 using rt1n_ind_right; auto.
+ intros; rewrite <- rt1n_trans_equiv in *.
+ eauto.
+ Qed.
+
+ (** Direct reflexive-symmetric-transitive closure is equivalent to
+ transitivity by symmetric left-step extension *)
+
+ Lemma rts1n_rts : forall x y,
+ clos_refl_sym_trans_1n A R x y -> clos_refl_sym_trans A R x y.
+ Proof.
+ induction 1.
+ constructor 2.
+ constructor 4 with y; auto.
+ case H;[constructor 1|constructor 3; constructor 1]; auto.
+ Qed.
+
+ Lemma rts_1n_trans : forall x y, clos_refl_sym_trans_1n A R x y ->
+ forall z, clos_refl_sym_trans_1n A R y z ->
+ clos_refl_sym_trans_1n A R x z.
+ induction 1.
+ auto.
+ intros; right with y; eauto.
+ Qed.
+
+ Lemma rts1n_sym : forall x y, clos_refl_sym_trans_1n A R x y ->
+ clos_refl_sym_trans_1n A R y x.
+ Proof.
+ intros x y H; elim H.
+ constructor 1.
+ intros x0 y0 z D H0 H1; apply rts_1n_trans with y0; auto.
+ right with x0.
+ tauto.
+ left.
+ Qed.
+
+ Lemma rts_rts1n : forall x y,
+ clos_refl_sym_trans A R x y -> clos_refl_sym_trans_1n A R x y.
+ induction 1.
+ constructor 2 with y; auto.
+ constructor 1.
+ constructor 1.
+ apply rts1n_sym; auto.
+ eapply rts_1n_trans; eauto.
+ Qed.
+
+ Lemma rts_rts1n_equiv : forall x y,
+ clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_1n A R x y.
+ Proof.
+ split.
+ apply rts_rts1n.
+ apply rts1n_rts.
+ Qed.
+
+ (** Direct reflexive-symmetric-transitive closure is equivalent to
+ transitivity by symmetric right-step extension *)
+
+ Lemma rtsn1_rts : forall x y,
+ clos_refl_sym_trans_n1 A R x y -> clos_refl_sym_trans A R x y.
+ Proof.
+ induction 1.
+ constructor 2.
+ constructor 4 with y; auto.
+ case H;[constructor 1|constructor 3; constructor 1]; auto.
+ Qed.
+
+ Lemma rtsn1_trans : forall y z, clos_refl_sym_trans_n1 A R y z->
+ forall x, clos_refl_sym_trans_n1 A R x y ->
+ clos_refl_sym_trans_n1 A R x z.
+ Proof.
+ induction 1.
+ auto.
+ intros.
+ right with y0; eauto.
+ Qed.
+
+ Lemma rtsn1_sym : forall x y, clos_refl_sym_trans_n1 A R x y ->
+ clos_refl_sym_trans_n1 A R y x.
+ Proof.
+ intros x y H; elim H.
+ constructor 1.
+ intros y0 z D H0 H1. apply rtsn1_trans with y0; auto.
+ right with z.
+ tauto.
+ left.
+ Qed.
+
+ Lemma rts_rtsn1 : forall x y,
+ clos_refl_sym_trans A R x y -> clos_refl_sym_trans_n1 A R x y.
+ Proof.
+ induction 1.
+ constructor 2 with x; auto.
+ constructor 1.
+ constructor 1.
+ apply rtsn1_sym; auto.
+ eapply rtsn1_trans; eauto.
+ Qed.
+
+ Lemma rts_rtsn1_equiv : forall x y,
+ clos_refl_sym_trans A R x y <-> clos_refl_sym_trans_n1 A R x y.
+ Proof.
+ split.
+ apply rts_rtsn1.
+ apply rtsn1_rts.
+ Qed.
+
+ End Equivalences.
+
End Properties.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index a5ad269d4..2793da5b1 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -8,66 +8,117 @@
(*i $Id$ i*)
-(****************************************************************************)
-(* Bruno Barras, Cristina Cornes *)
-(* *)
-(* Some of these definitons were taken from : *)
-(* Constructing Recursion Operators in Type Theory *)
-(* L. Paulson JSC (1986) 2, 325-355 *)
-(****************************************************************************)
+(************************************************************************)
+(** * Bruno Barras, Cristina Cornes *)
+(** * *)
+(** * Some of these definitions were taken from : *)
+(** * Constructing Recursion Operators in Type Theory *)
+(** * L. Paulson JSC (1986) 2, 325-355 *)
+(************************************************************************)
Require Import Relation_Definitions.
Require Import List.
-(** Some operators to build relations *)
+(** * Some operators to build relations *)
+
+(** ** Transitive closure *)
Section Transitive_Closure.
Variable A : Type.
Variable R : relation A.
-
+
+ (** Definition by direct transitive closure *)
+
Inductive clos_trans (x: A) : A -> Prop :=
- | t_step : forall y:A, R x y -> clos_trans x y
- | t_trans :
- forall y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
+ | t_step (y:A) : R x y -> clos_trans x y
+ | t_trans (y z:A) : clos_trans x y -> clos_trans y z -> clos_trans x z.
+
+ (** Alternative definition by transitive extension on the left *)
+
+ Inductive clos_trans_1n (x: A) : A -> Prop :=
+ | t1n_step (y:A) : R x y -> clos_trans_1n x y
+ | t1n_trans (y z:A) : R x y -> clos_trans_1n y z -> clos_trans_1n x z.
+
+ (** Alternative definition by transitive extension on the right *)
+
+ Inductive clos_trans_n1 (x: A) : A -> Prop :=
+ | tn1_step (y:A) : R x y -> clos_trans_n1 x y
+ | tn1_trans (y z:A) : R y z -> clos_trans_n1 x y -> clos_trans_n1 x z.
+
End Transitive_Closure.
+(** ** Reflexive-transitive closure *)
Section Reflexive_Transitive_Closure.
Variable A : Type.
Variable R : relation A.
- Inductive clos_refl_trans (x:A) : A -> Prop:=
- | rt_step : forall y:A, R x y -> clos_refl_trans x y
+ (** Definition by direct reflexive-transitive closure *)
+
+ Inductive clos_refl_trans (x:A) : A -> Prop :=
+ | rt_step (y:A) : R x y -> clos_refl_trans x y
| rt_refl : clos_refl_trans x x
- | rt_trans :
- forall y z:A,
+ | rt_trans (y z:A) :
clos_refl_trans x y -> clos_refl_trans y z -> clos_refl_trans x z.
+
+ (** Alternative definition by transitive extension on the left *)
+
+ Inductive clos_refl_trans_1n (x: A) : A -> Prop :=
+ | rt1n_refl : clos_refl_trans_1n x x
+ | rt1n_trans (y z:A) :
+ R x y -> clos_refl_trans_1n y z -> clos_refl_trans_1n x z.
+
+ (** Alternative definition by transitive extension on the right *)
+
+ Inductive clos_refl_trans_n1 (x: A) : A -> Prop :=
+ | rtn1_refl : clos_refl_trans_n1 x x
+ | rtn1_trans (y z:A) :
+ R y z -> clos_refl_trans_n1 x y -> clos_refl_trans_n1 x z.
+
End Reflexive_Transitive_Closure.
+(** ** Reflexive-symmetric-transitive closure *)
Section Reflexive_Symetric_Transitive_Closure.
Variable A : Type.
Variable R : relation A.
- Inductive clos_refl_sym_trans : relation A :=
- | rst_step : forall x y:A, R x y -> clos_refl_sym_trans x y
- | rst_refl : forall x:A, clos_refl_sym_trans x x
- | rst_sym :
- forall x y:A, clos_refl_sym_trans x y -> clos_refl_sym_trans y x
- | rst_trans :
- forall x y z:A,
+ (** Definition by direct reflexive-symmetric-transitive closure *)
+
+ Inductive clos_refl_sym_trans (x:A) : A -> Prop :=
+ | rst_step (y:A) : R x y -> clos_refl_sym_trans x y
+ | rst_refl : clos_refl_sym_trans x x
+ | rst_sym (y:A) : clos_refl_sym_trans y x -> clos_refl_sym_trans x y
+ | rst_trans (y z:A) :
clos_refl_sym_trans x y ->
clos_refl_sym_trans y z -> clos_refl_sym_trans x z.
+
+ (** Alternative definition by symmetric-transitive extension on the left *)
+
+ Inductive clos_refl_sym_trans_1n (x: A) : A -> Prop :=
+ | rts1n_refl : clos_refl_sym_trans_1n x x
+ | rts1n_trans (y z:A) : R x y \/ R y x ->
+ clos_refl_sym_trans_1n y z -> clos_refl_sym_trans_1n x z.
+
+ (** Alternative definition by symmetric-transitive extension on the right *)
+
+ Inductive clos_refl_sym_trans_n1 (x: A) : A -> Prop :=
+ | rtsn1_refl : clos_refl_sym_trans_n1 x x
+ | rtsn1_trans (y z:A) : R y z \/ R z y ->
+ clos_refl_sym_trans_n1 x y -> clos_refl_sym_trans_n1 x z.
+
End Reflexive_Symetric_Transitive_Closure.
+(** ** Converse of a relation *)
-Section Transposee.
+Section Converse.
Variable A : Type.
Variable R : relation A.
Definition transp (x y:A) := R y x.
-End Transposee.
+End Converse.
+(** ** Union of relations *)
Section Union.
Variable A : Type.
@@ -76,6 +127,7 @@ Section Union.
Definition union (x y:A) := R1 x y \/ R2 x y.
End Union.
+(** ** Disjoint union of relations *)
Section Disjoint_Union.
Variables A B : Type.
@@ -83,16 +135,15 @@ Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
Inductive le_AsB : A + B -> A + B -> Prop :=
- | le_aa : forall x y:A, leA x y -> le_AsB (inl _ x) (inl _ y)
- | le_ab : forall (x:A) (y:B), le_AsB (inl _ x) (inr _ y)
- | le_bb : forall x y:B, leB x y -> le_AsB (inr _ x) (inr _ y).
+ | le_aa (x y:A) : leA x y -> le_AsB (inl _ x) (inl _ y)
+ | le_ab (x:A) (y:B) : le_AsB (inl _ x) (inr _ y)
+ | le_bb (x y:B) : leB x y -> le_AsB (inr _ x) (inr _ y).
End Disjoint_Union.
-
+(** ** Lexicographic order on dependent pairs *)
Section Lexicographic_Product.
- (* Lexicographic order on dependent pairs *)
Variable A : Type.
Variable B : A -> Type.
@@ -106,8 +157,10 @@ Section Lexicographic_Product.
| right_lex :
forall (x:A) (y y':B x),
leB x y y' -> lexprod (existS B x y) (existS B x y').
+
End Lexicographic_Product.
+(** ** Product of relations *)
Section Symmetric_Product.
Variable A : Type.
@@ -123,16 +176,15 @@ Section Symmetric_Product.
End Symmetric_Product.
+(** ** Multiset of two relations *)
Section Swap.
Variable A : Type.
Variable R : A -> A -> Prop.
Inductive swapprod : A * A -> A * A -> Prop :=
- | sp_noswap : forall x x':A * A, symprod A A R R x x' -> swapprod x x'
- | sp_swap :
- forall (x y:A) (p:A * A),
- symprod A A R R (x, y) p -> swapprod (y, x) p.
+ | sp_noswap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (x, y) p
+ | sp_swap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (y, x) p.
End Swap.
@@ -144,16 +196,14 @@ Section Lexicographic_Exponentiation.
Let List := list A.
Inductive Ltl : List -> List -> Prop :=
- | Lt_nil : forall (a:A) (x:List), Ltl Nil (a :: x)
- | Lt_hd : forall a b:A, leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
- | Lt_tl : forall (a:A) (x y:List), Ltl x y -> Ltl (a :: x) (a :: y).
-
+ | Lt_nil (a:A) (x:List) : Ltl Nil (a :: x)
+ | Lt_hd (a b:A) : leA a b -> forall x y:list A, Ltl (a :: x) (b :: y)
+ | Lt_tl (a:A) (x y:List) : Ltl x y -> Ltl (a :: x) (a :: y).
Inductive Desc : List -> Prop :=
| d_nil : Desc Nil
- | d_one : forall x:A, Desc (x :: Nil)
- | d_conc :
- forall (x y:A) (l:List),
+ | d_one (x:A) : Desc (x :: Nil)
+ | d_conc (x y:A) (l:List) :
leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
Definition Pow : Set := sig Desc.