diff options
Diffstat (limited to 'theories/Logic/ConstructiveEpsilon.v')
-rw-r--r-- | theories/Logic/ConstructiveEpsilon.v | 32 |
1 files changed, 11 insertions, 21 deletions
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 61e377ea..f1503d24 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id:$ i*) +(*i $Id: ConstructiveEpsilon.v 10739 2008-04-01 14:45:20Z herbelin $ i*) (** This module proves the constructive description schema, which infers the sigma-existence (i.e., [Set]-existence) of a witness to a @@ -20,17 +20,19 @@ 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 +[Fix_F] 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, +To use [Fix_F], 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}]. *) +(** Based on ideas from Benjamin Werner and Jean-François Monin *) + (** Contributed by Yevgeniy Makarov *) Require Import Arith. @@ -49,7 +51,8 @@ numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after 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). +Let R (x y : nat) : Prop := 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. @@ -78,7 +81,7 @@ Defined. Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}. Proof. -intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption]. +intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption]. clear Acc_0; intros x IH. destruct (P_decidable x) as [Px | not_Px]. exists x; simpl; assumption. @@ -102,7 +105,7 @@ Section ConstructiveEpsilon. there are functions [f : A -> nat] and [g : nat -> A] such that [g] is a left inverse of [f]. *) -Variable A : Type. +Variable A : Set. Variable f : A -> nat. Variable g : nat -> A. @@ -132,24 +135,11 @@ Proof. intros; apply constructive_indefinite_description; firstorder. Defined. -Definition epsilon (E : exists x : A, P x) : A +Definition constructive_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) +Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_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. |