Library FinSet.Lib.CEExt
This file contains extensions of the ConstructiveEpsilon library
of Coq. Primarily, this is about supporting the DProp library
instead of explicit usage of sumbool. In addition this files
provides additional lemmas about ConstructiveEpsilon, in
particular the extensionality of the choice procedure.
Require Coq.Logic.ConstructiveEpsilon.
Require Import FinSet.Lib.DProp.
Import Coq.Classes.Morphisms.
A DProp interface
Section Choice.
Context {A:Type} (to_nat:A→nat) (of_nat:nat→A).
Context (retract:∀ x, of_nat(to_nat x) = x).
Context(P:A→DProp).
Indefinite description for inhabited countable types.
Definition choice : (∃ x, P x) → { x:A | P x } :=
ConstructiveEpsilon.constructive_indefinite_ground_description
A to_nat of_nat retract P (fun x⇒ dec_alt (P x))
.
ConstructiveEpsilon.constructive_indefinite_ground_description
A to_nat of_nat retract P (fun x⇒ dec_alt (P x))
.
choose is a choice operator on every inhabited countable
type. The main result in this file is that choose only depends
on the extension of P (and the encoding).
Definition choose (h:∃ x, P x) : A := proj1_sig (choice h).
Lemma choose_spec : ∀ h, P (choose h).
End Choice.
Lemma choose_spec : ∀ h, P (choose h).
End Choice.
choose is extensional
Lemma linear_search_ext : ∀ P P_dec Q Q_dec n w v, (∀ x, P x ↔ Q x) →
proj1_sig (ConstructiveEpsilon.linear_search P P_dec n w) =
proj1_sig (ConstructiveEpsilon.linear_search Q Q_dec n v).
Section ChoiceExt.
Context (A:Type).
Local Notation "´Π´ x y ´:´ R ´,´ S" := (respectful_hetero _ _ _ _ R%signature (fun x y ⇒ S)%signature) (at level 200, x ident, y ident).
Lemma choose_ext : Proper
(Π to_nat₁ to_nat₂ : eq==>eq,
Π of_nat₁ of_nat₂ : eq==>eq,
Π _ _ : (fun _ _ ⇒ True),
Π P P´ : eq==>eq_dprop,
Π _ _ : (fun _ _ ⇒ True),
@eq A) choose.
End ChoiceExt.