From b9f47391f7f259c24119d1de0a87839e2cc5e80c Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 24 Jul 2010 20:01:08 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13323 --- theories/Logic/Berardi.v | 2 +- theories/Logic/ChoiceFacts.v | 2 +- theories/Logic/Classical.v | 2 +- theories/Logic/ClassicalChoice.v | 2 +- theories/Logic/ClassicalDescription.v | 2 +- theories/Logic/ClassicalEpsilon.v | 2 +- theories/Logic/ClassicalFacts.v | 2 +- theories/Logic/ClassicalUniqueChoice.v | 2 +- theories/Logic/Classical_Pred_Set.v | 2 +- theories/Logic/Classical_Pred_Type.v | 2 +- theories/Logic/Classical_Prop.v | 2 +- theories/Logic/Classical_Type.v | 2 +- theories/Logic/ConstructiveEpsilon.v | 112 +++++++++++++++++++++++++----- theories/Logic/Decidable.v | 2 +- theories/Logic/Description.v | 2 +- theories/Logic/Diaconescu.v | 2 +- theories/Logic/Epsilon.v | 2 +- theories/Logic/Eqdep.v | 2 +- theories/Logic/EqdepFacts.v | 2 +- theories/Logic/Eqdep_dec.v | 2 +- theories/Logic/FunctionalExtensionality.v | 2 +- theories/Logic/Hurkens.v | 2 +- theories/Logic/IndefiniteDescription.v | 2 +- theories/Logic/JMeq.v | 2 +- theories/Logic/ProofIrrelevance.v | 2 +- theories/Logic/ProofIrrelevanceFacts.v | 2 +- theories/Logic/RelationalChoice.v | 2 +- theories/Logic/SetIsType.v | 2 +- 28 files changed, 122 insertions(+), 44 deletions(-) (limited to 'theories/Logic') diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v index 5b2f5063..7d9fb802 100644 --- a/theories/Logic/Berardi.v +++ b/theories/Logic/Berardi.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Prop. + +Hypothesis P_dec : forall n, {P n}+{~(P n)}. + + +(** The termination argument is [before_witness n], which says that +any number before any witness (not necessarily the [x] of [exists x :A, P x]) +makes the search eventually stops. *) + +Inductive before_witness : nat -> Prop := + | stop : forall n, P n -> before_witness n + | next : forall n, before_witness (S n) -> before_witness n. + +(* Computation of the initial termination certificate *) +Fixpoint O_witness (n : nat) : before_witness n -> before_witness 0 := + match n return (before_witness n -> before_witness 0) with + | 0 => fun b => b + | S n => fun b => O_witness n (next n b) + end. + +(* Inversion of [inv_before_witness n] in a way such that the result +is structurally smaller even in the [stop] case. *) +Definition inv_before_witness : + forall n, before_witness n -> ~(P n) -> before_witness (S n) := + fun n b => + match b in before_witness n return ~ P n -> before_witness (S n) with + | stop n p => fun not_p => match (not_p p) with end + | next n b => fun _ => b + end. + +Fixpoint linear_search m (b : before_witness m) : {n : nat | P n} := + match P_dec m with + | left yes => exist (fun n => P n) m yes + | right no => linear_search (S m) (inv_before_witness m b no) + end. + +Definition constructive_indefinite_description_nat : + (exists n, P n) -> {n:nat | P n} := + fun e => linear_search O (let (n, p) := e in O_witness n (stop n p)). + +End ConstructiveIndefiniteDescription_Direct. + +(************************************************************************) + +(* Version using the predicate [Acc] *) Require Import Arith. -Section ConstructiveIndefiniteDescription. +Section ConstructiveIndefiniteDescription_Acc. Variable P : nat -> Prop. -Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}. +Hypothesis P_decidable : forall n : nat, {P n} + {~ P n}. + +(** 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 [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}]. -(** 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 +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 @@ -92,13 +151,32 @@ 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}. +Theorem constructive_indefinite_description_nat_Acc : + (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. +End ConstructiveIndefiniteDescription_Acc. + +(************************************************************************) + +Section ConstructiveEpsilon_nat. + +Variable P : nat -> Prop. + +Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}. + +Definition constructive_epsilon_nat (E : exists n : nat, P n) : nat + := proj1_sig (constructive_indefinite_description_nat P P_decidable E). + +Definition constructive_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_epsilon_nat E) + := proj2_sig (constructive_indefinite_description_nat P P_decidable E). + +End ConstructiveEpsilon_nat. + +(************************************************************************) Section ConstructiveEpsilon. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index c6d32d9b..df9acbcc 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*