From 1f915bf2b4edc46461fef4106f4fe77e89c3fd4f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 18 Oct 2008 14:32:00 +0000 Subject: Intégration et formattage du développement de Pierre Castéran sur les définitions alternatives de la transitivé d'une relation MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11462 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Operators_Properties.v | 334 +++++++++++++++++++++++++++--- theories/Relations/Relation_Operators.v | 132 ++++++++---- 2 files changed, 397 insertions(+), 69 deletions(-) (limited to 'theories/Relations') 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. -- cgit v1.2.3