Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ConstructiveEpsilon.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*)

(** This provides with a proof of the constructive form of definite
and indefinite descriptions for Sigma^0_1-formulas (hereafter called
"small" formulas), which infers the sigma-existence (i.e.,
[Type]-existence) of a witness to a decidable predicate over a
countable domain from the regular existence (i.e.,
[Prop]-existence). *)

(** Coq does not allow case analysis on sort [Prop] when the goal is in
not 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 [Type]. 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
[Fix_F] in the module Coq.Init.Wf. There, recursion is done on an
inductive predicate [Acc] and the resulting type is in [Type].

To find a witness of [P] constructively, we program the well-known
linear search algorithm that tries P on all natural numbers starting
from 0 and going up.  Such an algorithm needs a suitable termination
certificate.  We offer two ways for providing this termination
certificate: a direct one, based on an ad-hoc predicate called
[before_witness], and another one based on the predicate [Acc].
For the first one we provide explicit and short proof terms. *)

(** Based on ideas from Benjamin Werner and Jean-François Monin *)

(** Contributed by Yevgeniy Makarov and Jean-François Monin *)

(* -------------------------------------------------------------------- *)

(* Direct version *)

Require Import Arith.

Section ConstructiveIndefiniteGroundDescription_Direct.

Variable P : nat -> 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 (n:nat) : Prop :=
  | stop : P n -> before_witness n
  | next : 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 return ~ P n -> before_witness (S n) with
      | stop _ p => fun not_p => match (not_p p) with end
      | next _ 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_ground_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)).

Fixpoint linear_search_smallest (start : nat) (pr : before_witness start) :
  forall k : nat, start <= k < proj1_sig (linear_search start pr) -> ~P k.
Proof.
  (* Recursion on pr, which is the distance between start and linear_search *)
  intros. destruct (P_dec start) eqn:Pstart.
  - (* P start, k cannot exist *)
    intros. assert (proj1_sig (linear_search start pr) = start).
    { unfold linear_search. destruct pr; rewrite -> Pstart; reflexivity. }
    rewrite -> H0 in H. destruct H. apply (le_lt_trans start k) in H1.
    apply lt_irrefl in H1. contradiction. assumption.
  - (* ~P start, step once in the search and use induction hypothesis *)
    destruct pr. contradiction. destruct H. apply le_lt_or_eq in H. destruct H.
    apply (linear_search_smallest (S start) pr). split. assumption.
    simpl in H0. rewrite -> Pstart in H0. assumption. subst. assumption.
Defined.

Definition epsilon_smallest :
  (exists n : nat, P n)
  -> { n : nat | P n /\ forall k : nat, k < n -> ~P k }.
Proof.
  intros. pose (wit := (let (n, p) := H in O_witness n (stop n p))).
  destruct (linear_search 0 wit) as [n pr] eqn:ls. exists n. split. assumption. intros.
  apply (linear_search_smallest 0 wit). split. apply le_0_n.
  rewrite -> ls. assumption.
Qed.

End ConstructiveIndefiniteGroundDescription_Direct.

(************************************************************************)

(* Version using the predicate [Acc] *)

Section ConstructiveIndefiniteGroundDescription_Acc.

Variable P : nat -> Prop.

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}].

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) : Prop := x = S y /\ ~ P y.

Local Notation acc x := (Acc R x).

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 Fix_F 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_ground_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 ConstructiveIndefiniteGroundDescription_Acc.

(************************************************************************)

Section ConstructiveGroundEpsilon_nat.

Variable P : nat -> Prop.

Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.

Definition constructive_ground_epsilon_nat (E : exists n : nat, P n) : nat
  := proj1_sig (constructive_indefinite_ground_description_nat P P_decidable E).

Definition constructive_ground_epsilon_spec_nat (E : (exists n, P n)) : P (constructive_ground_epsilon_nat E)
  := proj2_sig (constructive_indefinite_ground_description_nat P P_decidable E).

End ConstructiveGroundEpsilon_nat.

(************************************************************************)

Section ConstructiveGroundEpsilon.

(** 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_ground_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_ground_description_nat P' P'_decidable)  in H1.
destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
Defined.

Lemma constructive_definite_ground_description : (exists! x : A, P x) -> {x : A | P x}.
Proof.
  intros; apply constructive_indefinite_ground_description; firstorder.
Defined.

Definition constructive_ground_epsilon (E : exists x : A, P x) : A
  := proj1_sig (constructive_indefinite_ground_description E).

Definition constructive_ground_epsilon_spec (E : (exists x, P x)) : P (constructive_ground_epsilon E)
  := proj2_sig (constructive_indefinite_ground_description E).

End ConstructiveGroundEpsilon.

(* begin hide *)
(* Compatibility: the qualificative "ground" was absent from the initial
names of the results in this file but this had introduced confusion
with the similarly named statement in Description.v *)
Notation constructive_indefinite_description_nat :=
  constructive_indefinite_ground_description_nat (only parsing).
Notation constructive_epsilon_spec_nat :=
  constructive_ground_epsilon_spec_nat (only parsing).
Notation constructive_epsilon_nat :=
  constructive_ground_epsilon_nat (only parsing).
Notation constructive_indefinite_description :=
  constructive_indefinite_ground_description (only parsing).
Notation constructive_definite_description :=
  constructive_definite_ground_description (only parsing).
Notation constructive_epsilon_spec :=
  constructive_ground_epsilon_spec (only parsing).
Notation constructive_epsilon :=
  constructive_ground_epsilon (only parsing).
(* end hide *)

¤ Dauer der Verarbeitung: 0.22 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.