diff options
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 43 | ||||
| -rw-r--r-- | theories/Logic/Eqdep_dec.v | 19 | ||||
| -rw-r--r-- | theories/Relations/Operators_Properties.v | 6 | ||||
| -rw-r--r-- | theories/Relations/Relation_Operators.v | 16 | ||||
| -rw-r--r-- | theories/Relations/Relations.v | 4 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 | ||||
| -rw-r--r-- | theories/Wellfounded/Lexicographic_Product.v | 12 | ||||
| -rw-r--r-- | theories/Wellfounded/Transitive_Closure.v | 4 | ||||
| -rw-r--r-- | theories/Wellfounded/Well_Ordering.v | 14 |
9 files changed, 51 insertions, 69 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 2f36b8bb5..7627d2a6b 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P]. (** Dependent equality is equivalent to equality on dependent pairs *) Lemma eq_sigS_eq_dep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), - existS P p x = existS P q y -> eq_dep p x q y. + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), + existT P p x = existT P q y -> eq_dep p x q y. Proof. intros. dependent rewrite H. @@ -114,7 +114,7 @@ Proof. Qed. Lemma equiv_eqex_eqdep : - forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q), + forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q), existS P p x = existS P q y <-> eq_dep p x q y. Proof. split. @@ -248,28 +248,13 @@ End Equivalences. Section Corollaries. Variable U:Type. - Variable V:Set. (** UIP implies the injectivity of equality on dependent pairs in Type *) - - Definition Inj_dep_pairT := - forall (P:U -> Type) (p:U) (x y:P p), - existT P p x = existT P p y -> x = y. - - Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT. - Proof. - intro eq_dep_eq; red; intros. - apply eq_dep_eq. - apply eq_sigT_eq_dep. - assumption. - Qed. - - (** UIP implies the injectivity of equality on dependent pairs in Set *) - Definition Inj_dep_pairS := - forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y. + Definition Inj_dep_pair := + forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. - Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS. + Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair. Proof. intro eq_dep_eq; red; intros. apply eq_dep_eq. @@ -279,6 +264,11 @@ Section Corollaries. End Corollaries. +Notation Inj_dep_pairS := Inj_dep_pair. +Notation Inj_dep_pairT := Inj_dep_pair. +Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2. + + (************************************************************************) (** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *) @@ -333,18 +323,13 @@ End Axioms. (** UIP implies the injectivity of equality on dependent pairs in Type *) -Lemma inj_pairT2 : +Lemma inj_pair2 : forall (U:Type) (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y. -Proof (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)). - -(** UIP implies the injectivity of equality on dependent pairs in Set *) - -Lemma inj_pair2 : - forall (U:Set) (P:U -> Set) (p:U) (x y:P p), - existS P p x = existS P p y -> x = y. Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)). +Notation inj_pairT2 := inj_pair2. + End EqdepTheory. Implicit Arguments eq_dep []. diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v index b45aa23fe..3c276cd2b 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -242,7 +242,7 @@ End DecidableEqDep. Module Type DecidableSet. - Parameter U:Set. + Parameter U:Type. Axiom eq_dec : forall x y:U, {x = y} + {x <> y}. End DecidableSet. @@ -283,14 +283,6 @@ Module DecidableEqDepSet (M:DecidableSet). forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. Proof N.Streicher_K. - (** Injectivity of equality on dependent pairs with second component - in [Type] *) - - Lemma inj_pairT2 : - forall (P:U -> Type) (p:U) (x y:P p), - existT P p x = existT P p y -> x = y. - Proof N.inj_pairT2. - (** Proof-irrelevance on subsets of decidable sets *) Lemma inj_pairP2 : @@ -298,11 +290,16 @@ Module DecidableEqDepSet (M:DecidableSet). ex_intro P x p = ex_intro P x q -> p = q. Proof N.inj_pairP2. - (** Injectivity of equality on dependent pairs in [Set] *) + (** Injectivity of equality on dependent pairs in [Type] *) Lemma inj_pair2 : - forall (P:U -> Set) (p:U) (x y:P p), + forall (P:U -> Type) (p:U) (x y:P p), existS P p x = existS P p y -> x = y. Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq. + (** Injectivity of equality on dependent pairs with second component + in [Type] *) + + Notation inj_pairT2 := inj_pair2. + End DecidableEqDepSet. diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v index 3cae9d571..4a6d58ec2 100644 --- a/theories/Relations/Operators_Properties.v +++ b/theories/Relations/Operators_Properties.v @@ -18,7 +18,7 @@ Require Import Relation_Operators. Section Properties. - Variable A : Set. + Variable A : Type. Variable R : relation A. Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y. @@ -43,7 +43,7 @@ Section Properties. Qed. Lemma clos_refl_trans_ind_left : - forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop), + forall (A:Type) (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. @@ -95,4 +95,4 @@ Section Properties. End Clos_Refl_Sym_Trans. -End Properties.
\ No newline at end of file +End Properties. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index e4918d40e..c8ace84c3 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -78,7 +78,7 @@ End Union. Section Disjoint_Union. -Variables A B : Set. +Variables A B : Type. Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. @@ -94,8 +94,8 @@ End Disjoint_Union. Section Lexicographic_Product. (* Lexicographic order on dependent pairs *) - Variable A : Set. - Variable B : A -> Set. + Variable A : Type. + Variable B : A -> Type. Variable leA : A -> A -> Prop. Variable leB : forall x:A, B x -> B x -> Prop. @@ -110,8 +110,8 @@ End Lexicographic_Product. Section Symmetric_Product. - Variable A : Set. - Variable B : Set. + Variable A : Type. + Variable B : Type. Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. @@ -125,7 +125,7 @@ End Symmetric_Product. Section Swap. - Variable A : Set. + Variable A : Type. Variable R : A -> A -> Prop. Inductive swapprod : A * A -> A * A -> Prop := @@ -138,7 +138,7 @@ End Swap. Section Lexicographic_Exponentiation. - Variable A : Set. + Variable A : Type. Variable leA : A -> A -> Prop. Let Nil := nil (A:=A). Let List := list A. @@ -156,7 +156,7 @@ Section Lexicographic_Exponentiation. 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 Pow : Type := sig Desc. Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b). diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v index 938d514df..1c6df08a4 100644 --- a/theories/Relations/Relations.v +++ b/theories/Relations/Relations.v @@ -13,7 +13,7 @@ Require Export Relation_Operators. Require Export Operators_Properties. Lemma inverse_image_of_equivalence : - forall (A B:Set) (f:A -> B) (r:relation B), + forall (A B:Type) (f:A -> B) (r:relation B), equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)). Proof. intros; split; elim H; red in |- *; auto. @@ -21,7 +21,7 @@ Proof. Qed. Lemma inverse_image_of_eq : - forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y). + forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y). Proof. split; red in |- *; [ (* reflexivity *) reflexivity diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v index 69421255d..4d6d66c3d 100644 --- a/theories/Wellfounded/Lexicographic_Exponentiation.v +++ b/theories/Wellfounded/Lexicographic_Exponentiation.v @@ -18,7 +18,7 @@ Require Import Relation_Operators. Require Import Transitive_Closure. Section Wf_Lexicographic_Exponentiation. - Variable A : Set. + Variable A : Type. Variable leA : A -> A -> Prop. Notation Power := (Pow A leA). diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index 82bede919..f41b6e93d 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -18,8 +18,8 @@ Require Import Transitive_Closure. L. Paulson JSC (1986) 2, 325-355 *) Section WfLexicographic_Product. - Variable A : Set. - Variable B : A -> Set. + Variable A : Type. + Variable B : A -> Type. Variable leA : A -> A -> Prop. Variable leB : forall x:A, B x -> B x -> Prop. @@ -74,8 +74,8 @@ End WfLexicographic_Product. Section Wf_Symmetric_Product. - Variable A : Set. - Variable B : Set. + Variable A : Type. + Variable B : Type. Variable leA : A -> A -> Prop. Variable leB : B -> B -> Prop. @@ -106,7 +106,7 @@ End Wf_Symmetric_Product. Section Swap. - Variable A : Set. + Variable A : Type. Variable R : A -> A -> Prop. Notation SwapProd := (swapprod A R). @@ -168,4 +168,4 @@ Section Swap. apply Acc_swapprod; auto with sets. Qed. -End Swap.
\ No newline at end of file +End Swap. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 1866c5035..5e33da5ff 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -14,7 +14,7 @@ Require Import Relation_Definitions. Require Import Relation_Operators. Section Wf_Transitive_Closure. - Variable A : Set. + Variable A : Type. Variable R : relation A. Notation trans_clos := (clos_trans A R). @@ -44,4 +44,4 @@ Section Wf_Transitive_Closure. unfold well_founded in |- *; auto with sets. Qed. -End Wf_Transitive_Closure.
\ No newline at end of file +End Wf_Transitive_Closure. diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v index b1cb63be1..7296897ef 100644 --- a/theories/Wellfounded/Well_Ordering.v +++ b/theories/Wellfounded/Well_Ordering.v @@ -15,10 +15,10 @@ Require Import Eqdep. Section WellOrdering. - Variable A : Set. - Variable B : A -> Set. + Variable A : Type. + Variable B : A -> Type. - Inductive WO : Set := + Inductive WO : Type := sup : forall (a:A) (f:B a -> WO), WO. @@ -52,7 +52,7 @@ Section Characterisation_wf_relations. (* in course of development *) - Variable A : Set. + Variable A : Type. Variable leA : A -> A -> Prop. Definition B (a:A) := {x : A | leA x a}. @@ -60,12 +60,12 @@ Section Characterisation_wf_relations. Definition wof : well_founded leA -> A -> WO A B. Proof. intros. - apply (well_founded_induction H (fun a:A => WO A B)); auto. - intros. + apply (well_founded_induction_type H (fun a:A => WO A B)); auto. + intros x H1. apply (sup A B x). unfold B at 1 in |- *. destruct 1 as [x0]. apply (H1 x0); auto. Qed. -End Characterisation_wf_relations.
\ No newline at end of file +End Characterisation_wf_relations. |