From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 29 Nov 2003 17:28:49 +0000 Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Relations/Newman.v | 134 +++++++++++++----------- theories/Relations/Operators_Properties.v | 100 +++++++++--------- theories/Relations/Relation_Definitions.v | 65 ++++++------ theories/Relations/Relation_Operators.v | 168 ++++++++++++++++-------------- theories/Relations/Relations.v | 24 ++--- theories/Relations/Rstar.v | 83 ++++++++------- 6 files changed, 297 insertions(+), 277 deletions(-) (limited to 'theories/Relations') diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index 57e93240a..7de49f62f 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -8,108 +8,116 @@ (*i $Id$ i*) -Require Rstar. +Require Import Rstar. Section Newman. -Variable A: Type. -Variable R: A->A->Prop. +Variable A : Type. +Variable R : A -> A -> Prop. -Local Rstar := (Rstar A R). -Local Rstar_reflexive := (Rstar_reflexive A R). -Local Rstar_transitive := (Rstar_transitive A R). -Local Rstar_Rstar' := (Rstar_Rstar' A R). +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:A][y:A] (exT2 ? (Rstar x) (Rstar y)). +Definition coherence (x y:A) := ex2 (Rstar x) (Rstar y). -Theorem coherence_intro : (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y). -Proof [x:A][y:A][z:A][h1:(Rstar x z)][h2:(Rstar y z)] - (exT_intro2 A (Rstar x) (Rstar y) z h1 h2). +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 : (x:A)(y:A)(Rstar x y)->(coherence x y). - Proof [x:A][y:A][h:(Rstar x y)](coherence_intro x y y h (Rstar_reflexive y)). +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: (x:A)(y:A)(coherence x y)->(coherence y x). - Proof [x:A][y:A][h:(coherence x y)] - (exT2_ind A (Rstar x) (Rstar y) (coherence y x) - [w:A][h1:(Rstar x w)][h2:(Rstar y w)] - (coherence_intro y x w h2 h1) h). - -Definition confluence := - [x:A](y:A)(z:A)(Rstar x y)->(Rstar x z)->(coherence y z). +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](y:A)(z:A)(R x y)->(R 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 := - (x:A)(P:A->Prop)((y:A)((z:A)(R y z)->(P z))->(P y))->(P x). + 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:(x:A)(local_confluence x). +Hypothesis Hyp1 : noetherian. +Hypothesis Hyp2 : forall x:A, local_confluence x. (** The induction hypothesis *) Section Induct. - Variable x:A. - Hypothesis hyp_ind:(u:A)(R x u)->(confluence u). + 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). + 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). + 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 : (v:A)(u1:(R x v))(u2:(Rstar v z))(coherence y z). - -Proof (* We draw the diagram ! *) - [v:A][u1:(R x v)][u2:(Rstar v z)] - (exT2_ind A (Rstar u) (Rstar v) (* local confluence in x for u,v *) - (coherence y z) (* gives w, u->*w and v->*w *) - ([w:A][s1:(Rstar u w)][s2:(Rstar v w)] - (exT2_ind A (Rstar y) (Rstar w) (* confluence in u => coherence(y,w) *) - (coherence y z) (* gives a, y->*a and z->*a *) - ([a:A][v1:(Rstar y a)][v2:(Rstar w a)] - (exT2_ind A (Rstar a) (Rstar z) (* confluence in v => coherence(a,z) *) - (coherence y z) (* gives b, a->*b and z->*b *) - ([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 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 - ([v:A][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*) +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 ([u:A][v:A](coherence v z)) - (Rstar_coherence x z h2) (*i case x=y i*) - caseRxy). (*i case x->u->*z i*) +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 : (x:A)(confluence x). -Proof [x:A](Hyp1 x confluence Ind_proof). +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 0ca819b84..9534f707f 100755 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -12,55 +12,53 @@ (* Bruno Barras *) (****************************************************************************) -Require Relation_Definitions. -Require Relation_Operators. +Require Import Relation_Definitions. +Require Import Relation_Operators. Section Properties. - Variable A: Set. - Variable R: (relation A). + Variable A : Set. + Variable R : relation A. - Local incl : (relation A)->(relation A)->Prop := - [R1,R2: (relation A)] (x,y:A) (R1 x y) -> (R2 x y). + 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). + 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). +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. -NewInduction 1; Auto with sets. -Intros. -Apply rt_trans with y; Auto with sets. +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: (A:Set)(R:A->A->Prop)(M:A)(P:A->Prop) - (P M) - ->((P0,N:A) - (clos_refl_trans A R M P0)->(P P0)->(R P0 N)->(P N)) - ->(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. + 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. @@ -69,30 +67,30 @@ 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. -NewInduction 1; Auto with sets. -Apply rst_trans with y; Auto with sets. + 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). + 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_trans A R). -Exact (rst_sym 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. -NewInduction 1; Auto with sets. -Apply rst_trans with y; Auto with sets. + 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. +End Properties. \ No newline at end of file diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 32f433d07..06440fd86 100755 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -10,19 +10,19 @@ Section Relation_Definition. - Variable A: Type. + Variable A : Type. - Definition relation := A -> A -> Prop. + Definition relation := A -> A -> Prop. - Variable R: relation. + Variable R : relation. Section General_Properties_of_Relations. - Definition reflexive : Prop := (x: A) (R x x). - Definition transitive : Prop := (x,y,z: A) (R x y) -> (R y z) -> (R x z). - Definition symmetric : Prop := (x,y: A) (R x y) -> (R y x). - Definition antisymmetric : Prop := (x,y: A) (R x y) -> (R y x) -> x=y. + 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. @@ -33,23 +33,20 @@ End General_Properties_of_Relations. Section Sets_of_Relations. - Record preorder : Prop := { - preord_refl : reflexive; - preord_trans : transitive }. + Record preorder : Prop := + {preord_refl : reflexive; preord_trans : transitive}. - Record order : Prop := { - ord_refl : reflexive; - ord_trans : transitive; - ord_antisym : antisymmetric }. + 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 equivalence : Prop := + {equiv_refl : reflexive; + equiv_trans : transitive; + equiv_sym : symmetric}. - Record PER : Prop := { - per_sym : symmetric; - per_trans : transitive }. + Record PER : Prop := {per_sym : symmetric; per_trans : transitive}. End Sets_of_Relations. @@ -57,27 +54,25 @@ End Sets_of_Relations. Section Relations_of_Relations. - Definition inclusion : relation -> relation -> Prop := - [R1,R2: relation] (x,y:A) (R1 x y) -> (R2 x y). + Definition inclusion (R1 R2:relation) : Prop := + forall x y:A, R1 x y -> R2 x y. - Definition same_relation : relation -> relation -> Prop := - [R1,R2: relation] (inclusion R1 R2) /\ (inclusion R2 R1). + Definition same_relation (R1 R2:relation) : Prop := + inclusion R1 R2 /\ inclusion R2 R1. - Definition commut : relation -> relation -> Prop := - [R1,R2:relation] (x,y:A) (R1 y x) -> (z:A) (R2 z y) - -> (EX y':A |(R2 y' x) & (R1 z y')). + 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. -Hints Unfold reflexive transitive antisymmetric symmetric : sets v62. +Hint Unfold reflexive transitive antisymmetric symmetric: sets v62. -Hints 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 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. -Hints Unfold inclusion same_relation commut : 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 index 7b07ac0db..0d5f2fd97 100755 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -16,72 +16,76 @@ (* L. Paulson JSC (1986) 2, 325-355 *) (****************************************************************************) -Require Relation_Definitions. -Require PolyList. -Require PolyListSyntax. +Require Import Relation_Definitions. +Require Import List. (** Some operators to build relations *) Section Transitive_Closure. - Variable A: Set. - Variable R: (relation A). + Variable A : Set. + Variable R : relation A. - Inductive clos_trans : A->A->Prop := - t_step: (x,y:A)(R x y)->(clos_trans x y) - | t_trans: (x,y,z:A)(clos_trans x y)->(clos_trans y z)->(clos_trans x z). + 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: (x,y:A)(R x y)->(clos_refl_trans x y) - | rt_refl: (x:A)(clos_refl_trans x x) - | rt_trans: (x,y,z: A)(clos_refl_trans x y)->(clos_refl_trans y z) - ->(clos_refl_trans x z). + 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: (x,y:A)(R x y)->(clos_refl_sym_trans x y) - | rst_refl: (x:A)(clos_refl_sym_trans x x) - | rst_sym: (x,y:A)(clos_refl_sym_trans x y)->(clos_refl_sym_trans y x) - | rst_trans: (x,y,z:A)(clos_refl_sym_trans x y)->(clos_refl_sym_trans y z) - ->(clos_refl_sym_trans x z). + 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). + Variable A : Set. + Variable R : relation A. - Definition transp := [x,y:A](R y x). + Definition transp (x y:A) := R y x. End Transposee. Section Union. - Variable A: Set. - Variable R1,R2: (relation A). + Variable A : Set. + Variables R1 R2 : relation A. - Definition union := [x,y:A](R1 x y)\/(R2 x y). + Definition union (x y:A) := R1 x y \/ R2 x y. End Union. Section Disjoint_Union. -Variable A,B:Set. -Variable leA: A->A->Prop. -Variable leB: B->B->Prop. +Variables A B : Set. +Variable leA : A -> A -> Prop. +Variable leB : B -> B -> Prop. -Inductive le_AsB : A+B->A+B->Prop := - le_aa: (x,y:A) (leA x y) -> (le_AsB (inl A B x) (inl A B y)) -| le_ab: (x:A)(y:B) (le_AsB (inl A B x) (inr A B y)) -| le_bb: (x,y:B) (leB x y) -> (le_AsB (inr A B x) (inr A B y)). +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. @@ -90,68 +94,74 @@ 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: (x:A)(B x)->(B x)->Prop. - -Inductive lexprod : (sigS A B) -> (sigS A B) ->Prop := - left_lex : (x,x':A)(y:(B x)) (y':(B x')) - (leA x x') ->(lexprod (existS A B x y) (existS A B x' y')) -| right_lex : (x:A) (y,y':(B x)) - (leB x y y') -> (lexprod (existS A B x y) (existS A B x y')). +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. + 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 : (x,x':A)(leA x x')->(y:B)(symprod (x,y) (x',y)) - | right_sym : (y,y':B)(leB y y')->(x:A)(symprod (x,y) (x,y')). + 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: (x,x':A*A)(symprod A A R R x x')->(swapprod x x') - | sp_swap: (x,y:A)(p:A*A)(symprod A A R R (x,y) p)->(swapprod (y,x) p). + 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. -Local Nil := (nil A). -Local List := (list A). +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 (cons a x)) -| Lt_hd : (a,b:A) (leA a b)-> (x,y:(list A))(Ltl (cons a x) (cons b y)) -| Lt_tl : (a:A)(x,y:List)(Ltl x y) -> (Ltl (cons a x) (cons a y)). +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 : (x:A)(Desc (cons x Nil)) -| d_conc : (x,y:A)(l:List)(leA x y) - -> (Desc l^(cons y Nil))->(Desc (l^(cons y Nil))^(cons x Nil)). +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 List Desc). +Definition Pow : Set := sig Desc. -Definition lex_exp : Pow -> Pow ->Prop := - [a,b:Pow](Ltl (proj1_sig List Desc a) (proj1_sig List Desc b)). +Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b). End Lexicographic_Exponentiation. -Hints Unfold transp union : sets v62. -Hints Resolve t_step rt_step rt_refl rst_step rst_refl : sets v62. -Hints Immediate rst_sym : sets v62. +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 index f792e4c2a..d2c3e2776 100755 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -12,17 +12,17 @@ Require Export Relation_Definitions. Require Export Relation_Operators. Require Export Operators_Properties. -Lemma inverse_image_of_equivalence : (A,B:Set)(f:A->B) - (r:(relation B))(equivalence B r)->(equivalence A [x,y:A](r (f x) (f y))). -Intros; Split; Elim H; Red; Auto. -Intros _ equiv_trans _ x y z H0 H1; Apply equiv_trans with (f y); Assumption. +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 : (A,B:Set)(f:A->B) - (equivalence A [x,y:A](f x)=(f y)). -Split; Red; -[ (* reflexivity *) Reflexivity -| (* transitivity *) Intros; Transitivity (f y); Assumption -| (* symmetry *) Intros; Symmetry; 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 index 90ab6d6c2..349650629 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -13,66 +13,75 @@ Section Rstar. Variable A : Type. -Variable R : A->A->Prop. +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](P:A->A->Prop) - ((u:A)(P u u))->((u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)) -> (P x y). +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: (x:A)(Rstar x x). - Proof [x:A][P:A->A->Prop] - [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)] - (h1 x). +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: (x:A)(y:A)(z:A)(R x y)->(Rstar y z)->(Rstar x z). - Proof [x:A][y:A][z:A][t1:(R x y)][t2:(Rstar y z)] - [P:A->A->Prop] - [h1:(u:A)(P u u)][h2:(u:A)(v:A)(w:A)(R u v)->(P v w)->(P u w)] - (h2 x y z t1 (t2 P h1 h2)). +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: (x:A)(y:A)(z:A)(Rstar x y)->(Rstar y z)->(Rstar x z). - Proof [x:A][y:A][z:A][h:(Rstar x y)] - (h ([u:A][v:A](Rstar v z)->(Rstar u z)) - ([u:A][t:(Rstar u z)]t) - ([u:A][v:A][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)))). +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:A][y:A](P:A->A->Prop) - ((P x x))->((u:A)(R x u)->(Rstar u y)->(P x y)) -> (P x y). +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: (x:A)(Rstar' x x). - Proof [x:A][P:A->A->Prop][h:(P x x)][h':(u:A)(R x u)->(Rstar u x)->(P x x)]h. +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: (x:A)(y:A)(z:A)(R x z)->(Rstar z y)->(Rstar' x y). - Proof [x:A][y:A][z:A][t1:(R x z)][t2:(Rstar z y)] - [P:A->A->Prop][h1:(P x x)] - [h2:(u:A)(R x u)->(Rstar u y)->(P x y)](h2 z t1 t2). +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: (x:A)(y:A)(Rstar' x y)->(Rstar x y). - Proof [x:A][y:A][h:(Rstar' x y)] - (h Rstar (Rstar_reflexive x) ([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 (Rstar_reflexive x) (fun u:A => Rstar_R x u y). -Theorem Rstar_Rstar': (x:A)(y:A)(Rstar x y)->(Rstar' x y). - Proof [x:A][y:A][h:(Rstar x y)](h Rstar' ([u:A](Rstar'_reflexive u)) - ([u:A][v:A][w:A][h1:(R u v)][h2:(Rstar' v w)] - (Rstar'_R u w v h1 (Rstar'_Rstar v w h2)))). +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] - (x,y:A)(R1 y x)->(z:A)(R2 z y) - ->(EX y':A |(R2 y' x) & (R1 z y')). +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. - -- cgit v1.2.3