diff options
Diffstat (limited to 'theories/Relations')
| -rwxr-xr-x | theories/Relations/Newman.v | 123 | ||||
| -rwxr-xr-x | theories/Relations/Operators_Properties.v | 96 | ||||
| -rwxr-xr-x | theories/Relations/Relation_Definitions.v | 78 | ||||
| -rwxr-xr-x | theories/Relations/Relation_Operators.v | 167 | ||||
| -rwxr-xr-x | theories/Relations/Relations.v | 28 | ||||
| -rwxr-xr-x | theories/Relations/Rstar.v | 87 | ||||
| -rwxr-xr-x | theories/Relations/intro.tex | 23 |
7 files changed, 602 insertions, 0 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v new file mode 100755 index 00000000..3cf604d8 --- /dev/null +++ b/theories/Relations/Newman.v @@ -0,0 +1,123 @@ +(************************************************************************) +(* 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,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ 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 new file mode 100755 index 00000000..5e0e9ec8 --- /dev/null +++ b/theories/Relations/Operators_Properties.v @@ -0,0 +1,96 @@ +(************************************************************************) +(* 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: Operators_Properties.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*) + +(****************************************************************************) +(* Bruno Barras *) +(****************************************************************************) + +Require Import Relation_Definitions. +Require Import Relation_Operators. + + +Section Properties. + + Variable A : Set. + 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. + + Lemma clos_rt_is_preorder : preorder A (clos_refl_trans A R). +apply Build_preorder. +exact (rt_refl A R). + +exact (rt_trans A R). +Qed. + + + +Lemma clos_rt_idempotent : + incl (clos_refl_trans A (clos_refl_trans A R)) (clos_refl_trans A R). +red in |- *. +induction 1; auto with sets. +intros. +apply rt_trans with y; auto with sets. +Qed. + + Lemma clos_refl_trans_ind_left : + forall (A:Set) (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. +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. + + Lemma clos_rt_clos_rst : + inclusion A (clos_refl_trans A R) (clos_refl_sym_trans A R). +red in |- *. +induction 1; auto with sets. +apply rst_trans with y; auto with sets. +Qed. + + Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans A R). +apply Build_equivalence. +exact (rst_refl A R). + +exact (rst_trans A R). + +exact (rst_sym A R). +Qed. + + Lemma clos_rst_idempotent : + incl (clos_refl_sym_trans A (clos_refl_sym_trans A R)) + (clos_refl_sym_trans A R). +red in |- *. +induction 1; auto with sets. +apply rst_trans with y; auto with sets. +Qed. + +End Clos_Refl_Sym_Trans. + +End Properties.
\ No newline at end of file diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v new file mode 100755 index 00000000..e115b0b0 --- /dev/null +++ b/theories/Relations/Relation_Definitions.v @@ -0,0 +1,78 @@ +(************************************************************************) +(* 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: Relation_Definitions.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ 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. + Definition antisymmetric : Prop := forall x y:A, R x y -> R y x -> x = y. + + (* for compatibility with Equivalence in ../PROGRAMS/ALG/ *) + Definition equiv := reflexive /\ transitive /\ symmetric. + +End General_Properties_of_Relations. + + + +Section Sets_of_Relations. + + Record preorder : Prop := + {preord_refl : reflexive; preord_trans : transitive}. + + Record order : Prop := + {ord_refl : reflexive; + ord_trans : transitive; + ord_antisym : antisymmetric}. + + 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'. + +End Relations_of_Relations. + + +End Relation_Definition. + +Hint Unfold reflexive transitive antisymmetric symmetric: sets v62. + +Hint Resolve Build_preorder Build_order Build_equivalence Build_PER + preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl + equiv_trans equiv_sym per_sym per_trans: sets v62. + +Hint Unfold inclusion same_relation commut: sets v62.
\ No newline at end of file diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v new file mode 100755 index 00000000..b6359ada --- /dev/null +++ b/theories/Relations/Relation_Operators.v @@ -0,0 +1,167 @@ +(************************************************************************) +(* 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: Relation_Operators.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ 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 *) +(****************************************************************************) + +Require Import Relation_Definitions. +Require Import List. + +(** Some operators to build relations *) + +Section Transitive_Closure. + Variable A : Set. + Variable R : relation A. + + Inductive clos_trans : A -> A -> Prop := + | t_step : forall x y:A, R x y -> clos_trans x y + | t_trans : + forall x y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z. +End Transitive_Closure. + + +Section Reflexive_Transitive_Closure. + Variable A : Set. + Variable R : relation A. + + Inductive clos_refl_trans : relation A := + | rt_step : forall x y:A, R x y -> clos_refl_trans x y + | rt_refl : forall x:A, clos_refl_trans x x + | rt_trans : + forall x y z:A, + clos_refl_trans x y -> clos_refl_trans y z -> clos_refl_trans x z. +End Reflexive_Transitive_Closure. + + +Section Reflexive_Symetric_Transitive_Closure. + Variable A : Set. + 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, + clos_refl_sym_trans x y -> + clos_refl_sym_trans y z -> clos_refl_sym_trans x z. +End Reflexive_Symetric_Transitive_Closure. + + +Section Transposee. + Variable A : Set. + Variable R : relation A. + + Definition transp (x y:A) := R y x. +End Transposee. + + +Section Union. + Variable A : Set. + Variables R1 R2 : relation A. + + Definition union (x y:A) := R1 x y \/ R2 x y. +End Union. + + +Section Disjoint_Union. +Variables A B : Set. +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 B x) (inl B y) + | le_ab : forall (x:A) (y:B), le_AsB (inl B x) (inr A y) + | le_bb : forall x y:B, leB x y -> le_AsB (inr A x) (inr A y). + +End Disjoint_Union. + + + +Section Lexicographic_Product. +(* Lexicographic order on dependent pairs *) + +Variable A : Set. +Variable B : A -> Set. +Variable leA : A -> A -> Prop. +Variable leB : forall x:A, B x -> B x -> Prop. + +Inductive lexprod : sigS B -> sigS B -> Prop := + | left_lex : + forall (x x':A) (y:B x) (y':B x'), + leA x x' -> lexprod (existS B x y) (existS B x' y') + | 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. + + +Section Symmetric_Product. + Variable A : Set. + Variable B : Set. + Variable leA : A -> A -> Prop. + Variable leB : B -> B -> Prop. + + Inductive symprod : A * B -> A * B -> Prop := + | left_sym : + forall x x':A, leA x x' -> forall y:B, symprod (x, y) (x', y) + | right_sym : + forall y y':B, leB y y' -> forall x:A, symprod (x, y) (x, y'). + +End Symmetric_Product. + + +Section Swap. + Variable A : Set. + 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. +End Swap. + + +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 : 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). + + +Inductive Desc : List -> Prop := + | d_nil : Desc Nil + | d_one : forall x:A, Desc (x :: Nil) + | d_conc : + forall (x y:A) (l:List), + 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. + +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.
\ No newline at end of file diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v new file mode 100755 index 00000000..6c96f14d --- /dev/null +++ b/theories/Relations/Relations.v @@ -0,0 +1,28 @@ +(************************************************************************) +(* 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: Relations.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*) + +Require Export Relation_Definitions. +Require Export Relation_Operators. +Require Export Operators_Properties. + +Lemma inverse_image_of_equivalence : + forall (A B:Set) (f:A -> B) (r:relation B), + equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). +intros; split; elim H; red in |- *; auto. +intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption. +Qed. + +Lemma inverse_image_of_eq : + forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y). +split; red in |- *; + [ (* reflexivity *) reflexivity + | (* transitivity *) intros; transitivity (f y); assumption + | (* symmetry *) intros; symmetry in |- *; assumption ]. +Qed.
\ No newline at end of file diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v new file mode 100755 index 00000000..7bb3ee93 --- /dev/null +++ b/theories/Relations/Rstar.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* 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,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ 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 + fun (x:A) (P:A -> A -> Prop) (h1:forall u:A, P u u) + (h2:forall u v w:A, R u v -> P v w -> P u w) => + h1 x. + +Theorem Rstar_R : forall x y z:A, R x y -> Rstar y z -> Rstar x z. + Proof + fun (x y z:A) (t1:R x y) (t2:Rstar y z) (P:A -> A -> Prop) + (h1:forall u:A, P u u) (h2:forall u v w:A, R u v -> P v w -> P u w) => + h2 x y z t1 (t2 P h1 h2). + +(** We conclude with transitivity of [Rstar] : *) + +Theorem Rstar_transitive : + forall x y z:A, Rstar x y -> Rstar y z -> Rstar x z. + Proof + fun (x y z:A) (h:Rstar x y) => + h (fun u v:A => Rstar v z -> Rstar u z) (fun (u:A) (t:Rstar u z) => t) + (fun (u v w:A) (t1:R u v) (t2:Rstar w z -> Rstar v z) + (t3:Rstar w z) => Rstar_R u v z t1 (t2 t3)). + +(** 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 + fun (x:A) (P:A -> A -> Prop) (h:P x x) + (h':forall u:A, R x u -> Rstar u x -> P x x) => h. + +Theorem Rstar'_R : forall x y z:A, R x z -> Rstar z y -> Rstar' x y. + Proof + fun (x y z:A) (t1:R x z) (t2:Rstar z y) (P:A -> A -> Prop) + (h1:P x x) (h2:forall u:A, R x u -> Rstar u y -> P x y) => + h2 z t1 t2. + +(** Equivalence of the two definitions: *) + +Theorem Rstar'_Rstar : forall x y:A, Rstar' x y -> Rstar x y. + Proof + fun (x y:A) (h:Rstar' x y) => + h Rstar (Rstar_reflexive x) (fun u:A => Rstar_R x u y). + +Theorem Rstar_Rstar' : forall x y:A, Rstar x y -> Rstar' x y. + Proof + fun (x y:A) (h:Rstar x y) => + h Rstar' (fun u:A => Rstar'_reflexive u) + (fun (u v w:A) (h1:R u v) (h2:Rstar' v w) => + Rstar'_R u w v h1 (Rstar'_Rstar v w h2)). + + +(** Property of Commutativity of two relations *) + +Definition commut (A:Set) (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/intro.tex b/theories/Relations/intro.tex new file mode 100755 index 00000000..5056f36f --- /dev/null +++ b/theories/Relations/intro.tex @@ -0,0 +1,23 @@ +\section{Relations}\label{Relations} + +This library develops closure properties of relations. + +\begin{itemize} +\item {\tt Relation\_Definitions.v} deals with the general notions + about binary relations (orders, equivalences, ...) + +\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various + closures of relations (by symmetry, by transitivity, ...) and + lexicographic orderings. + +\item {\tt Operators\_Properties.v} states and proves facts on the + various closures of a relation. + +\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt + Relation\_Operators.v} and \\ + {\tt Operators\_Properties.v} together. + +\item {\tt Newman.v} proves Newman's lemma on noetherian and locally + confluent relations. + +\end{itemize} |