From 6d28daee5feee9da501c758cc0516e57660a252e Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 17 Jul 2008 12:39:17 +0000 Subject: - Suppression de Rstar/Newman peu utilisables comme biblio (encodage des inductifs à l'ordre supérieur par exemple) et qui sont de toutes façons accessible en contrib dans Rocq/CoC_History. - MAJ numéro de version dans Tutorial.tex 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@11232 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Newman.v | 121 -------------------------------------------- theories/Relations/Rstar.v | 94 ---------------------------------- 2 files changed, 215 deletions(-) delete mode 100644 theories/Relations/Newman.v delete mode 100644 theories/Relations/Rstar.v (limited to 'theories/Relations') diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v deleted file mode 100644 index d97943280..000000000 --- a/theories/Relations/Newman.v +++ /dev/null @@ -1,121 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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/Rstar.v b/theories/Relations/Rstar.v deleted file mode 100644 index 095c94cfe..000000000 --- a/theories/Relations/Rstar.v +++ /dev/null @@ -1,94 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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. -- cgit v1.2.3