diff options
author | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2007-02-13 13:48:12 +0000 |
commit | 55ce117e8083477593cf1ff2e51a3641c7973830 (patch) | |
tree | a82defb4105f175c71b0d13cae42831ce608c4d6 /theories/Logic | |
parent | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff) |
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'theories/Logic')
-rw-r--r-- | theories/Logic/ClassicalDescription.v | 42 | ||||
-rw-r--r-- | theories/Logic/ConstructiveEpsilon.v | 155 | ||||
-rw-r--r-- | theories/Logic/EqdepFacts.v | 47 | ||||
-rw-r--r-- | theories/Logic/Eqdep_dec.v | 21 |
4 files changed, 195 insertions, 70 deletions
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v index 7053266a..1f1c34bf 100644 --- a/theories/Logic/ClassicalDescription.v +++ b/theories/Logic/ClassicalDescription.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*) +(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*) (** This file provides classical logic and definite description *) @@ -57,14 +57,11 @@ Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) : (exists! x:A, P x) -> P (iota i P) := proj2_sig (classical_definite_description P i). -(** Weaker lemmas (compatibility lemmas) *) - -Unset Implicit Arguments. - -Lemma dependent_description : - forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), - (forall x:A, exists! y : B x, R x y) -> - (exists f : (forall x:A, B x), forall x:A, R x (f x)). +(** Axiom of unique "choice" (functional reification of functional relations) *) +Theorem dependent_unique_choice : + forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), + (forall x:A, exists! y : B x, R x y) -> + (exists f : (forall x:A, B x), forall x:A, R x (f x)). Proof. intros A B R H. assert (Hexuni:forall x, exists! y, R x y). @@ -74,27 +71,18 @@ intro x. apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))). Qed. -Theorem description : - forall (A B:Type) (R:A -> B -> Prop), - (forall x : A, exists! y : B, R x y) -> - (exists f : A->B, forall x:A, R x (f x)). +Theorem unique_choice : + forall (A B:Type) (R:A -> B -> Prop), + (forall x:A, exists! y : B, R x y) -> + (exists f : A -> B, forall x:A, R x (f x)). Proof. intros A B. -apply (dependent_description A (fun _ => B)). +apply dependent_unique_choice with (B:=fun _:A => B). Qed. -(** Axiom of unique "choice" (functional reification of functional relations) *) +(** Compatibility lemmas *) -Set Implicit Arguments. - -Require Import Setoid. +Unset Implicit Arguments. -Theorem unique_choice : - forall (A B:Type) (R:A -> B -> Prop), - (forall x:A, exists! y : B, R x y) -> - (exists f : A -> B, forall x:A, R x (f x)). -Proof. -intros A B R H. -apply (description A B). -intro x. apply H. -Qed. +Definition dependent_description := dependent_unique_choice. +Definition description := unique_choice. diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v new file mode 100644 index 00000000..61e377ea --- /dev/null +++ b/theories/Logic/ConstructiveEpsilon.v @@ -0,0 +1,155 @@ +(************************************************************************) +(* 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:$ i*) + +(** This module proves the constructive description schema, which +infers the sigma-existence (i.e., [Set]-existence) of a witness to a +predicate from the regular existence (i.e., [Prop]-existence). One +requires that the underlying set is countable and that the predicate +is decidable. *) + +(** Coq does not allow case analysis on sort [Set] when the goal is in +[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to +show [{n : nat | P n}]. However, one can perform a recursion on an +inductive predicate in sort [Prop] so that the returning type of the +recursion is in [Set]. This trick is described in Coq'Art book, Sect. +14.2.3 and 15.4. In particular, this trick is used in the proof of +[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an +inductive predicate [Acc] and the resulting type is in [Type]. + +The predicate [Acc] delineates elements that are accessible via a +given relation [R]. An element is accessible if there are no infinite +[R]-descending chains starting from it. + +To use [Acc_iter], we define a relation R and prove that if [exists n, +P n] then 0 is accessible with respect to R. Then, by induction on the +definition of [Acc R 0], we show [{n : nat | P n}]. *) + +(** Contributed by Yevgeniy Makarov *) + +Require Import Arith. + +Section ConstructiveIndefiniteDescription. + +Variable P : nat -> Prop. + +Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}. + +(** To find a witness of [P] constructively, we define an algorithm +that tries P on all natural numbers starting from 0 and going up. The +relation [R] describes the connection between the two successive +numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after +[x], i.e., [y = S x] and [P x] is false. Then the absence of an +infinite [R]-descending chain from 0 is equivalent to the termination +of our searching algorithm. *) + +Let R (x y : nat) := (x = S y /\ ~ P y). +Notation Local "'acc' x" := (Acc R x) (at level 10). + +Lemma P_implies_acc : forall x : nat, P x -> acc x. +Proof. +intros x H. constructor. +intros y [_ not_Px]. absurd (P x); assumption. +Qed. + +Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x. +Proof. +intros x n; generalize x; clear x; induction n as [|n IH]; simpl. +apply P_implies_acc. +intros x H. constructor. intros y [fxy _]. +apply IH. rewrite fxy. +replace (n + S x) with (S (n + x)); auto with arith. +Defined. + +Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0. +Proof. +intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x). +replace (x + 0) with x; auto with arith. +Defined. + +(** In the following statement, we use the trick with recursion on +[Acc]. This is also where decidability of [P] is used. *) + +Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}. +Proof. +intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption]. +clear Acc_0; intros x IH. +destruct (P_decidable x) as [Px | not_Px]. +exists x; simpl; assumption. +set (y := S x). +assert (Ryx : R y x). unfold R; split; auto. +destruct (IH y Ryx) as [n Hn]. +exists n; assumption. +Defined. + +Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}. +Proof. +intros H; apply acc_implies_P_eventually. +apply P_eventually_implies_acc_ex; assumption. +Defined. + +End ConstructiveIndefiniteDescription. + +Section ConstructiveEpsilon. + +(** For the current purpose, we say that a set [A] is countable if +there are functions [f : A -> nat] and [g : nat -> A] such that [g] is +a left inverse of [f]. *) + +Variable A : Type. +Variable f : A -> nat. +Variable g : nat -> A. + +Hypothesis gof_eq_id : forall x : A, g (f x) = x. + +Variable P : A -> Prop. + +Hypothesis P_decidable : forall x : A, {P x} + {~ P x}. + +Definition P' (x : nat) : Prop := P (g x). + +Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}. +Proof. +intro n; unfold P'; destruct (P_decidable (g n)); auto. +Defined. + +Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}. +Proof. +intro H. assert (H1 : exists n : nat, P' n). +destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption. +apply (constructive_indefinite_description_nat P' P'_decidable) in H1. +destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption. +Defined. + +Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}. +Proof. + intros; apply constructive_indefinite_description; firstorder. +Defined. + +Definition epsilon (E : exists x : A, P x) : A + := proj1_sig (constructive_indefinite_description E). + +Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E) + := proj2_sig (constructive_indefinite_description E). + +End ConstructiveEpsilon. + +Theorem choice : + forall (A B : Type) (f : B -> nat) (g : nat -> B), + (forall x : B, g (f x) = x) -> + forall (R : A -> B -> Prop), + (forall (x : A) (y : B), {R x y} + {~ R x y}) -> + (forall x : A, exists y : B, R x y) -> + (exists f : A -> B, forall x : A, R x (f x)). +Proof. +intros A B f g gof_eq_id R R_dec H. +exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)). +intro x. +apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)). +Qed. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a257ef55..94a577ca 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*) (** This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives @@ -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 *) @@ -303,7 +293,7 @@ Lemma eq_rect_eq : Proof M.eq_rect_eq U. Lemma eq_rec_eq : - forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h. Proof (fun p Q => M.eq_rect_eq U p Q). (** Injectivity of Dependent Equality *) @@ -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 740fcfcf..103efd22 100644 --- a/theories/Logic/Eqdep_dec.v +++ b/theories/Logic/Eqdep_dec.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Eqdep_dec.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id: Eqdep_dec.v 9597 2007-02-06 19:44:05Z herbelin $ i*) (** We prove that there is only one proof of [x=x], i.e [refl_equal x]. This holds if the equality upon the set of [x] is decidable. @@ -235,7 +235,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. @@ -276,14 +276,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 : @@ -291,11 +283,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. |