diff options
Diffstat (limited to 'theories/Relations')
| -rw-r--r-- | theories/Relations/Newman.v | 121 | ||||
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 234 | ||||
| -rw-r--r-- | theories/Relations/Relation_Definitions.v | 28 | ||||
| -rw-r--r-- | theories/Relations/Relation_Operators.v | 36 | ||||
| -rw-r--r-- | theories/Relations/Relations.v | 2 | ||||
| -rw-r--r-- | theories/Relations/Rstar.v | 94 | ||||
| -rw-r--r-- | theories/Relations/vo.itarget | 4 |
7 files changed, 180 insertions, 339 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v deleted file mode 100644 index e7bb66eb..00000000 --- a/theories/Relations/Newman.v +++ /dev/null @@ -1,121 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Newman.v 9245 2006-10-17 12:53:34Z notin $ i*) - -Require Import Rstar. - -Section Newman. - -Variable A : Type. -Variable R : A -> A -> Prop. - -Let Rstar := Rstar A R. -Let Rstar_reflexive := Rstar_reflexive A R. -Let Rstar_transitive := Rstar_transitive A R. -Let Rstar_Rstar' := Rstar_Rstar' A R. - -Definition coherence (x y:A) := ex2 (Rstar x) (Rstar y). - -Theorem coherence_intro : - forall x y z:A, Rstar x z -> Rstar y z -> coherence x y. -Proof fun (x y z:A) (h1:Rstar x z) (h2:Rstar y z) => - ex_intro2 (Rstar x) (Rstar y) z h1 h2. - -(** A very simple case of coherence : *) - -Lemma Rstar_coherence : forall x y:A, Rstar x y -> coherence x y. -Proof - fun (x y:A) (h:Rstar x y) => coherence_intro x y y h (Rstar_reflexive y). - -(** coherence is symmetric *) -Lemma coherence_sym : forall x y:A, coherence x y -> coherence y x. -Proof - fun (x y:A) (h:coherence x y) => - ex2_ind - (fun (w:A) (h1:Rstar x w) (h2:Rstar y w) => - coherence_intro y x w h2 h1) h. - -Definition confluence (x:A) := - forall y z:A, Rstar x y -> Rstar x z -> coherence y z. - -Definition local_confluence (x:A) := - forall y z:A, R x y -> R x z -> coherence y z. - -Definition noetherian := - forall (x:A) (P:A -> Prop), - (forall y:A, (forall z:A, R y z -> P z) -> P y) -> P x. - -Section Newman_section. - - (** The general hypotheses of the theorem *) - - Hypothesis Hyp1 : noetherian. - Hypothesis Hyp2 : forall x:A, local_confluence x. - - (** The induction hypothesis *) - - Section Induct. - Variable x : A. - Hypothesis hyp_ind : forall u:A, R x u -> confluence u. - - (** Confluence in [x] *) - - Variables y z : A. - Hypothesis h1 : Rstar x y. - Hypothesis h2 : Rstar x z. - - (** particular case [x->u] and [u->*y] *) - Section Newman_. - Variable u : A. - Hypothesis t1 : R x u. - Hypothesis t2 : Rstar u y. - - (** In the usual diagram, we assume also [x->v] and [v->*z] *) - - Theorem Diagram : forall (v:A) (u1:R x v) (u2:Rstar v z), coherence y z. - Proof - (* We draw the diagram ! *) - fun (v:A) (u1:R x v) (u2:Rstar v z) => - ex2_ind - (* local confluence in x for u,v *) - (* gives w, u->*w and v->*w *) - (fun (w:A) (s1:Rstar u w) (s2:Rstar v w) => - ex2_ind - (* confluence in u => coherence(y,w) *) - (* gives a, y->*a and z->*a *) - (fun (a:A) (v1:Rstar y a) (v2:Rstar w a) => - ex2_ind - (* confluence in v => coherence(a,z) *) - (* gives b, a->*b and z->*b *) - (fun (b:A) (w1:Rstar a b) (w2:Rstar z b) => - coherence_intro y z b (Rstar_transitive y a b v1 w1) w2) - (hyp_ind v u1 a z (Rstar_transitive v w a s2 v2) u2)) - (hyp_ind u t1 y w t2 s1)) (Hyp2 x u v t1 u1). - - Theorem caseRxy : coherence y z. - Proof - Rstar_Rstar' x z h2 (fun v w:A => coherence y w) - (coherence_sym x y (Rstar_coherence x y h1)) (*i case x=z i*) - Diagram. (*i case x->v->*z i*) - End Newman_. - - Theorem Ind_proof : coherence y z. - Proof - Rstar_Rstar' x y h1 (fun u v:A => coherence v z) - (Rstar_coherence x z h2) (*i case x=y i*) - caseRxy. (*i case x->u->*z i*) - End Induct. - - Theorem Newman : forall x:A, confluence x. - Proof fun x:A => Hyp1 x confluence Ind_proof. - -End Newman_section. - - -End Newman. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index d0916b09..1976b435 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Operators_Properties.v 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (************************************************************************) (** * Some properties of the operators on relations *) @@ -16,31 +16,41 @@ Require Import Relation_Definitions. Require Import Relation_Operators. -Require Import Setoid. Section Properties. + Implicit Arguments clos_refl_trans [A]. + Implicit Arguments clos_refl_trans_1n [A]. + Implicit Arguments clos_refl_trans_n1 [A]. + Implicit Arguments clos_refl_sym_trans [A]. + Implicit Arguments clos_refl_sym_trans_1n [A]. + Implicit Arguments clos_refl_sym_trans_n1 [A]. + Implicit Arguments clos_trans [A]. + Implicit Arguments clos_trans_1n [A]. + Implicit Arguments clos_trans_n1 [A]. + Implicit Arguments inclusion [A]. + Implicit Arguments preorder [A]. + Variable A : Type. Variable R : relation A. - Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y. - Section Clos_Refl_Trans. + Local Notation "R *" := (clos_refl_trans R) (at level 8, left associativity). + (** Correctness of the reflexive-transitive closure operator *) - Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R). + Lemma clos_rt_is_preorder : preorder R*. Proof. apply Build_preorder. exact (rt_refl A R). - + 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). + Lemma clos_rt_idempotent : inclusion (R*)* R*. Proof. red in |- *. induction 1; auto with sets. @@ -56,7 +66,7 @@ Section Properties. reflexive-symmetric-transitive closure *) Lemma clos_rt_clos_rst : - inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R). + inclusion (clos_refl_trans R) (clos_refl_sym_trans R). Proof. red in |- *. induction 1; auto with sets. @@ -65,7 +75,7 @@ Section Properties. (** Correctness of the reflexive-symmetric-transitive closure *) - Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R). + Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R). Proof. apply Build_equivalence. exact (rst_refl A R). @@ -76,8 +86,8 @@ Section Properties. (** 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). + inclusion (clos_refl_sym_trans (clos_refl_sym_trans R)) + (clos_refl_sym_trans R). Proof. red in |- *. induction 1; auto with sets. @@ -91,11 +101,11 @@ Section Properties. (** *** Equivalences between the different definition of the reflexive, symmetric, transitive closures *) - (** *** Contributed by P. Casteran *) + (** *** Contributed by P. Castéran *) (** 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. + Lemma clos_t1n_trans : forall x y, clos_trans_1n R x y -> clos_trans R x y. Proof. induction 1. left; assumption. @@ -103,7 +113,7 @@ Section Properties. left; auto. Qed. - Lemma trans_t1n : forall x y, clos_trans A R x y -> clos_trans_1n A R x y. + Lemma clos_trans_t1n : forall x y, clos_trans R x y -> clos_trans_1n R x y. Proof. induction 1. left; assumption. @@ -111,20 +121,20 @@ Section Properties. right with y; auto. right with y; auto. eapply IHIHclos_trans1; auto. - apply t1n_trans; auto. + apply clos_t1n_trans; auto. Qed. - Lemma t1n_trans_equiv : forall x y, - clos_trans A R x y <-> clos_trans_1n A R x y. + Lemma clos_trans_t1n_iff : forall x y, + clos_trans R x y <-> clos_trans_1n R x y. Proof. split. - apply trans_t1n. - apply t1n_trans. + apply clos_trans_t1n. + apply clos_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. + Lemma clos_tn1_trans : forall x y, clos_trans_n1 R x y -> clos_trans R x y. Proof. induction 1. left; assumption. @@ -132,7 +142,7 @@ Section Properties. left; assumption. Qed. - Lemma trans_tn1 : forall x y, clos_trans A R x y -> clos_trans_n1 A R x y. + Lemma clos_trans_tn1 : forall x y, clos_trans R x y -> clos_trans_n1 R x y. Proof. induction 1. left; assumption. @@ -144,31 +154,31 @@ Section Properties. 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. + Lemma clos_trans_tn1_iff : forall x y, + clos_trans R x y <-> clos_trans_n1 R x y. Proof. split. - apply trans_tn1. - apply tn1_trans. + apply clos_trans_tn1. + apply clos_tn1_trans. Qed. - (** Direct reflexive-transitive closure is equivalent to + (** 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. + Lemma clos_rt1n_step : forall x y, R x y -> clos_refl_trans_1n 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. + Lemma clos_rtn1_step : forall x y, R x y -> clos_refl_trans_n1 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. + Lemma clos_rt1n_rt : forall x y, + clos_refl_trans_1n R x y -> clos_refl_trans R x y. Proof. induction 1. constructor 2. @@ -176,33 +186,33 @@ Section Properties. 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. + Lemma clos_rt_rt1n : forall x y, + clos_refl_trans R x y -> clos_refl_trans_1n R x y. Proof. induction 1. - apply R_rt1n; assumption. + apply clos_rt1n_step; 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. + apply clos_rt1n_rt; auto. Qed. - Lemma rt1n_trans_equiv : forall x y, - clos_refl_trans A R x y <-> clos_refl_trans_1n A R x y. + Lemma clos_rt_rt1n_iff : forall x y, + clos_refl_trans R x y <-> clos_refl_trans_1n R x y. Proof. split. - apply trans_rt1n. - apply rt1n_trans. + apply clos_rt_rt1n. + apply clos_rt1n_rt. Qed. - (** Direct reflexive-transitive closure is equivalent to + (** 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. + Lemma clos_rtn1_rt : forall x y, + clos_refl_trans_n1 R x y -> clos_refl_trans R x y. Proof. induction 1. constructor 2. @@ -210,37 +220,37 @@ Section Properties. 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. + Lemma clos_rt_rtn1 : forall x y, + clos_refl_trans R x y -> clos_refl_trans_n1 R x y. Proof. induction 1. - apply R_rtn1; auto. + apply clos_rtn1_step; 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. + Lemma clos_rt_rtn1_iff : forall x y, + clos_refl_trans R x y <-> clos_refl_trans_n1 R x y. Proof. split. - apply trans_rtn1. - apply rtn1_trans. + apply clos_rt_rtn1. + apply clos_rtn1_rt. 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. + (forall y z:A, clos_refl_trans R x y -> P y -> R y z -> P z) -> + forall z:A, clos_refl_trans 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. @@ -253,28 +263,30 @@ Section Properties. 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. + (forall x y, R x y -> clos_refl_trans_1n R y z -> P y -> P x) -> + forall x, clos_refl_trans_1n 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 *. + (forall x y, R x y -> P y -> clos_refl_trans R y z -> P x) -> + forall x, clos_refl_trans R x z -> P x. + intros P z Hz IH x Hxz. + apply clos_rt_rt1n_iff in Hxz. + elim Hxz using rt1n_ind_right; auto. + clear x Hxz. + intros x y Hxy Hyz Hy. + apply clos_rt_rt1n_iff in Hyz. eauto. Qed. - (** Direct reflexive-symmetric-transitive closure is equivalent to + (** 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. + Lemma clos_rst1n_rst : forall x y, + clos_refl_sym_trans_1n R x y -> clos_refl_sym_trans R x y. Proof. induction 1. constructor 2. @@ -282,48 +294,47 @@ Section Properties. 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. + Lemma clos_rst1n_trans : forall x y z, clos_refl_sym_trans_1n R x y -> + clos_refl_sym_trans_1n R y z -> clos_refl_sym_trans_1n 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. + Lemma clos_rst1n_sym : forall x y, clos_refl_sym_trans_1n R x y -> + clos_refl_sym_trans_1n 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. + intros x0 y0 z D H0 H1; apply clos_rst1n_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. + Lemma clos_rst_rst1n : forall x y, + clos_refl_sym_trans R x y -> clos_refl_sym_trans_1n R x y. induction 1. constructor 2 with y; auto. constructor 1. constructor 1. - apply rts1n_sym; auto. - eapply rts_1n_trans; eauto. + apply clos_rst1n_sym; auto. + eapply clos_rst1n_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. + Lemma clos_rst_rst1n_iff : forall x y, + clos_refl_sym_trans R x y <-> clos_refl_sym_trans_1n R x y. Proof. split. - apply rts_rts1n. - apply rts1n_rts. + apply clos_rst_rst1n. + apply clos_rst1n_rst. Qed. - (** Direct reflexive-symmetric-transitive closure is equivalent to + (** 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. + Lemma clos_rstn1_rst : forall x y, + clos_refl_sym_trans_n1 R x y -> clos_refl_sym_trans R x y. Proof. induction 1. constructor 2. @@ -331,46 +342,79 @@ Section Properties. 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. + Lemma clos_rstn1_trans : forall x y z, clos_refl_sym_trans_n1 R x y -> + clos_refl_sym_trans_n1 R y z -> clos_refl_sym_trans_n1 R x z. Proof. - induction 1. + intros x y z H1 H2. + induction H2. 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. + Lemma clos_rstn1_sym : forall x y, clos_refl_sym_trans_n1 R x y -> + clos_refl_sym_trans_n1 R y x. Proof. intros x y H; elim H. constructor 1. - intros y0 z D H0 H1. apply rtsn1_trans with y0; auto. + intros y0 z D H0 H1. apply clos_rstn1_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. + Lemma clos_rst_rstn1 : forall x y, + clos_refl_sym_trans R x y -> clos_refl_sym_trans_n1 R x y. Proof. induction 1. constructor 2 with x; auto. constructor 1. constructor 1. - apply rtsn1_sym; auto. - eapply rtsn1_trans; eauto. + apply clos_rstn1_sym; auto. + eapply clos_rstn1_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. + Lemma clos_rst_rstn1_iff : forall x y, + clos_refl_sym_trans R x y <-> clos_refl_sym_trans_n1 R x y. Proof. split. - apply rts_rtsn1. - apply rtsn1_rts. + apply clos_rst_rstn1. + apply clos_rstn1_rst. Qed. End Equivalences. End Properties. + +(* begin hide *) +(* Compatibility *) +Notation trans_tn1 := clos_trans_tn1 (only parsing). +Notation tn1_trans := clos_tn1_trans (only parsing). +Notation tn1_trans_equiv := clos_trans_tn1_iff (only parsing). + +Notation trans_t1n := clos_trans_t1n (only parsing). +Notation t1n_trans := clos_t1n_trans (only parsing). +Notation t1n_trans_equiv := clos_trans_t1n_iff (only parsing). + +Notation R_rtn1 := clos_rtn1_step (only parsing). +Notation trans_rt1n := clos_rt_rt1n (only parsing). +Notation rt1n_trans := clos_rt1n_rt (only parsing). +Notation rt1n_trans_equiv := clos_rt_rt1n_iff (only parsing). + +Notation R_rt1n := clos_rt1n_step (only parsing). +Notation trans_rtn1 := clos_rt_rtn1 (only parsing). +Notation rtn1_trans := clos_rtn1_rt (only parsing). +Notation rtn1_trans_equiv := clos_rt_rtn1_iff (only parsing). + +Notation rts1n_rts := clos_rst1n_rst (only parsing). +Notation rts_1n_trans := clos_rst1n_trans (only parsing). +Notation rts1n_sym := clos_rst1n_sym (only parsing). +Notation rts_rts1n := clos_rst_rst1n (only parsing). +Notation rts_rts1n_equiv := clos_rst_rst1n_iff (only parsing). + +Notation rtsn1_rts := clos_rstn1_rst (only parsing). +Notation rtsn1_trans := clos_rstn1_trans (only parsing). +Notation rtsn1_sym := clos_rstn1_sym (only parsing). +Notation rts_rtsn1 := clos_rst_rstn1 (only parsing). +Notation rts_rtsn1_equiv := clos_rst_rstn1_iff (only parsing). +(* end hide *) diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 762da1ff..c03c4b95 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -6,19 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Relation_Definitions.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) Section Relation_Definition. Variable A : Type. - + Definition relation := A -> A -> Prop. Variable R : relation. - + Section General_Properties_of_Relations. - + Definition reflexive : Prop := forall x:A, R x x. Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z. Definition symmetric : Prop := forall x y:A, R x y -> R y x. @@ -32,33 +32,33 @@ Section Relation_Definition. Section Sets_of_Relations. - - Record preorder : Prop := + + Record preorder : Prop := { preord_refl : reflexive; preord_trans : transitive}. - - Record order : Prop := + + Record order : Prop := { ord_refl : reflexive; ord_trans : transitive; ord_antisym : antisymmetric}. - - Record equivalence : Prop := + + Record equivalence : Prop := { equiv_refl : reflexive; equiv_trans : transitive; equiv_sym : symmetric}. - + Record PER : Prop := {per_sym : symmetric; per_trans : transitive}. End Sets_of_Relations. Section Relations_of_Relations. - + Definition inclusion (R1 R2:relation) : Prop := forall x y:A, R1 x y -> R2 x y. - + Definition same_relation (R1 R2:relation) : Prop := inclusion R1 R2 /\ inclusion R2 R1. - + Definition commut (R1 R2:relation) : Prop := forall x y:A, R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index 027a9e6c..39e0331d 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Relation_Operators.v 11481 2008-10-20 19:23:51Z herbelin $ i*) +(*i $Id$ i*) (************************************************************************) (** * Bruno Barras, Cristina Cornes *) @@ -17,7 +17,6 @@ (************************************************************************) Require Import Relation_Definitions. -Require Import List. (** * Some operators to build relations *) @@ -65,7 +64,7 @@ Section Reflexive_Transitive_Closure. Inductive clos_refl_trans_1n (x: A) : A -> Prop := | rt1n_refl : clos_refl_trans_1n x x - | rt1n_trans (y z:A) : + | 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 *) @@ -79,10 +78,10 @@ End Reflexive_Transitive_Closure. (** ** Reflexive-symmetric-transitive closure *) -Section Reflexive_Symetric_Transitive_Closure. +Section Reflexive_Symmetric_Transitive_Closure. Variable A : Type. Variable R : relation A. - + (** Definition by direct reflexive-symmetric-transitive closure *) Inductive clos_refl_sym_trans : relation A := @@ -96,18 +95,18 @@ Section Reflexive_Symetric_Transitive_Closure. (** 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 -> + | rst1n_refl : clos_refl_sym_trans_1n x x + | rst1n_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 -> + | rstn1_refl : clos_refl_sym_trans_n1 x x + | rstn1_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. +End Reflexive_Symmetric_Transitive_Closure. (** ** Converse of a relation *) @@ -139,7 +138,7 @@ Inductive le_AsB : A + B -> A + B -> Prop := | 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. +End Disjoint_Union. (** ** Lexicographic order on dependent pairs *) @@ -187,14 +186,15 @@ Section Swap. | sp_swap x y (p:A * A) : symprod A A R R (x, y) p -> swapprod (y, x) p. End Swap. +Local Open Scope list_scope. Section Lexicographic_Exponentiation. - + Variable A : Set. Variable leA : A -> A -> Prop. Let Nil := nil (A:=A). Let List := list A. - + Inductive Ltl : List -> List -> Prop := | 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) @@ -207,7 +207,7 @@ Section Lexicographic_Exponentiation. leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil). Definition Pow : Set := sig Desc. - + Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b). End Lexicographic_Exponentiation. @@ -215,3 +215,11 @@ End Lexicographic_Exponentiation. Hint Unfold transp union: sets v62. Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62. Hint Immediate rst_sym: sets v62. + +(* begin hide *) +(* Compatibility *) +Notation rts1n_refl := rst1n_refl (only parsing). +Notation rts1n_trans := rst1n_trans (only parsing). +Notation rtsn1_refl := rstn1_refl (only parsing). +Notation rtsn1_trans := rstn1_trans (only parsing). +(* end hide *) diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 6368ae25..1c6df08a 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Relations.v 9598 2007-02-06 19:45:52Z herbelin $ i*) +(*i $Id$ i*) Require Export Relation_Definitions. Require Export Relation_Operators. diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v deleted file mode 100644 index 82668006..00000000 --- a/theories/Relations/Rstar.v +++ /dev/null @@ -1,94 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Rstar.v 9642 2007-02-12 10:31:53Z herbelin $ i*) - -(** Properties of a binary relation [R] on type [A] *) - -Section Rstar. - - Variable A : Type. - Variable R : A -> A -> Prop. - - (** Definition of the reflexive-transitive closure [R*] of [R] *) - (** Smallest reflexive [P] containing [R o P] *) - - Definition Rstar (x y:A) := - forall P:A -> A -> Prop, - (forall u:A, P u u) -> (forall u v w:A, R u v -> P v w -> P u w) -> P x y. - - Theorem Rstar_reflexive : forall x:A, Rstar x x. - Proof. - unfold Rstar. intros x P P_refl RoP. apply P_refl. - Qed. - - Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z. - Proof. - intros x y z R_xy Rstar_yz. - unfold Rstar. - intros P P_refl RoP. apply RoP with (v:=y). - assumption. - apply Rstar_yz; assumption. - Qed. - - (** We conclude with transitivity of [Rstar] : *) - - Theorem Rstar_transitive : - forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z. - Proof. - intros x y z Rstar_xy; unfold Rstar in Rstar_xy. - apply Rstar_xy; trivial. - intros u v w R_uv fz Rstar_wz. - apply Rstar_R with (y:=v); auto. - Qed. - - (** Another characterization of [R*] *) - (** Smallest reflexive [P] containing [R o R*] *) - - Definition Rstar' (x y:A) := - forall P:A -> A -> Prop, - P x x -> (forall u:A, R x u -> Rstar u y -> P x y) -> P x y. - - Theorem Rstar'_reflexive : forall x:A, Rstar' x x. - Proof. - unfold Rstar'; intros; assumption. - Qed. - - Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y. - Proof. - unfold Rstar'. intros x y z Rxz Rstar_zy P Pxx RoP. - apply RoP with (u:=z); trivial. - Qed. - - (** Equivalence of the two definitions: *) - - Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y. - Proof. - intros x z Rstar'_xz; unfold Rstar' in Rstar'_xz. - apply Rstar'_xz. - exact (Rstar_reflexive x). - intro y; generalize x y z; exact Rstar_R. - Qed. - - Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y. - Proof. - intros. - apply H. - exact Rstar'_reflexive. - intros u v w R_uv Rs'_vw. apply Rstar'_R with (z:=v). - assumption. - apply Rstar'_Rstar; assumption. - Qed. - - (** Property of Commutativity of two relations *) - - Definition commut (A:Type) (R1 R2:A -> A -> Prop) := - forall x y:A, - R1 y x -> forall z:A, R2 z y -> exists2 y' : A, R2 y' x & R1 z y'. - -End Rstar. diff --git a/theories/Relations/vo.itarget b/theories/Relations/vo.itarget new file mode 100644 index 00000000..9d81dd07 --- /dev/null +++ b/theories/Relations/vo.itarget @@ -0,0 +1,4 @@ +Operators_Properties.vo +Relation_Definitions.vo +Relation_Operators.vo +Relations.vo |