← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Logic/ConstructiveEpsilon.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Logic/ConstructiveEpsilon.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)
 
10
 
 
11
(** This module proves the constructive description schema, which
 
12
infers the sigma-existence (i.e., [Set]-existence) of a witness to a
 
13
predicate from the regular existence (i.e., [Prop]-existence). One
 
14
requires that the underlying set is countable and that the predicate
 
15
is decidable. *)
 
16
 
 
17
(** Coq does not allow case analysis on sort [Prop] when the goal is in
 
18
[Set]. Therefore, one cannot eliminate [exists n, P n] in order to
 
19
show [{n : nat | P n}]. However, one can perform a recursion on an
 
20
inductive predicate in sort [Prop] so that the returning type of the
 
21
recursion is in [Set]. This trick is described in Coq'Art book, Sect.
 
22
14.2.3 and 15.4. In particular, this trick is used in the proof of
 
23
[Fix_F] in the module Coq.Init.Wf. There, recursion is done on an
 
24
inductive predicate [Acc] and the resulting type is in [Type].
 
25
 
 
26
The predicate [Acc] delineates elements that are accessible via a
 
27
given relation [R]. An element is accessible if there are no infinite
 
28
[R]-descending chains starting from it.
 
29
 
 
30
To use [Fix_F], we define a relation R and prove that if [exists n,
 
31
P n] then 0 is accessible with respect to R. Then, by induction on the
 
32
definition of [Acc R 0], we show [{n : nat | P n}]. *)
 
33
 
 
34
(** Based on ideas from Benjamin Werner and Jean-François Monin *)
 
35
 
 
36
(** Contributed by Yevgeniy Makarov *)
 
37
 
 
38
Require Import Arith.
 
39
 
 
40
Section ConstructiveIndefiniteDescription.
 
41
 
 
42
Variable P : nat -> Prop.
 
43
 
 
44
Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
 
45
 
 
46
(** To find a witness of [P] constructively, we define an algorithm
 
47
that tries P on all natural numbers starting from 0 and going up. The
 
48
relation [R] describes the connection between the two successive
 
49
numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after
 
50
[x], i.e., [y = S x] and [P x] is false. Then the absence of an
 
51
infinite [R]-descending chain from 0 is equivalent to the termination
 
52
of our searching algorithm. *)
 
53
 
 
54
Let R (x y : nat) : Prop := x = S y /\ ~ P y.
 
55
 
 
56
Notation Local acc x := (Acc R x).
 
57
 
 
58
Lemma P_implies_acc : forall x : nat, P x -> acc x.
 
59
Proof.
 
60
intros x H. constructor.
 
61
intros y [_ not_Px]. absurd (P x); assumption.
 
62
Qed.
 
63
 
 
64
Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
 
65
Proof.
 
66
intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
 
67
apply P_implies_acc.
 
68
intros x H. constructor. intros y [fxy _].
 
69
apply IH. rewrite fxy.
 
70
replace (n + S x) with (S (n + x)); auto with arith.
 
71
Defined.
 
72
 
 
73
Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.
 
74
Proof.
 
75
intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
 
76
replace (x + 0) with x; auto with arith.
 
77
Defined.
 
78
 
 
79
(** In the following statement, we use the trick with recursion on
 
80
[Acc]. This is also where decidability of [P] is used. *)
 
81
 
 
82
Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
 
83
Proof.
 
84
intros Acc_0. pattern 0. apply Fix_F with (R := R); [| assumption].
 
85
clear Acc_0; intros x IH.
 
86
destruct (P_decidable x) as [Px | not_Px].
 
87
exists x; simpl; assumption.
 
88
set (y := S x).
 
89
assert (Ryx : R y x). unfold R; split; auto.
 
90
destruct (IH y Ryx) as [n Hn].
 
91
exists n; assumption.
 
92
Defined.
 
93
 
 
94
Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}.
 
95
Proof.
 
96
intros H; apply acc_implies_P_eventually.
 
97
apply P_eventually_implies_acc_ex; assumption.
 
98
Defined.
 
99
 
 
100
End ConstructiveIndefiniteDescription.
 
101
 
 
102
Section ConstructiveEpsilon.
 
103
 
 
104
(** For the current purpose, we say that a set [A] is countable if
 
105
there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
 
106
a left inverse of [f]. *)
 
107
 
 
108
Variable A : Set.
 
109
Variable f : A -> nat.
 
110
Variable g : nat -> A.
 
111
 
 
112
Hypothesis gof_eq_id : forall x : A, g (f x) = x.
 
113
 
 
114
Variable P : A -> Prop.
 
115
 
 
116
Hypothesis P_decidable : forall x : A, {P x} + {~ P x}.
 
117
 
 
118
Definition P' (x : nat) : Prop := P (g x).
 
119
 
 
120
Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}.
 
121
Proof.
 
122
intro n; unfold P'; destruct (P_decidable (g n)); auto.
 
123
Defined.
 
124
 
 
125
Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
 
126
Proof.
 
127
intro H. assert (H1 : exists n : nat, P' n).
 
128
destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
 
129
apply (constructive_indefinite_description_nat P' P'_decidable)  in H1.
 
130
destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
 
131
Defined.
 
132
 
 
133
Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
 
134
Proof.
 
135
  intros; apply constructive_indefinite_description; firstorder.
 
136
Defined.
 
137
 
 
138
Definition constructive_epsilon (E : exists x : A, P x) : A
 
139
  := proj1_sig (constructive_indefinite_description E).
 
140
 
 
141
Definition constructive_epsilon_spec (E : (exists x, P x)) : P (constructive_epsilon E)
 
142
  := proj2_sig (constructive_indefinite_description E).
 
143
 
 
144
End ConstructiveEpsilon.
 
145