diff options
Diffstat (limited to 'theories/Relations/Relation_Operators.v')
| -rwxr-xr-x | theories/Relations/Relation_Operators.v | 168 |
1 files changed, 89 insertions, 79 deletions
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 |