Library Subsets.Subset_dec
This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Decidability results about subsets.
This module may be used through the import of Subsets.Subsets,
Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or
Lebesgue.Bochner.Bochner_wDep, where it is exported.
Brief description
Description
Support for unit types
- unit_subset_dec is a decidability result stating that subsets of unit types are either empty or singletons;
- unit_subset_is_singleton states the condition for subsets of unit types to be singletons.
Used logic axioms
- classic_dec, an alias for excluded_middle_informative, the strong form of excluded middle.
Usage
From Logic Require Import logic_compl.
From Subsets Require Import Subset.
Section Subset_Facts.
Context {U : Type}.
Lemma empty_dec : ∀ (A : U → Prop), { empty A } + { nonempty A }.
Proof.
intros A; destruct (classic_dec (empty A)); intros;
[left | right; apply nonempty_is_not_empty]; easy.
Qed.
Lemma in_dec : ∀ A (x : U), { A x } + { compl A x }.
Proof. intros; apply classic_dec. Qed.
Lemma unit_subset_dec :
∀ (A : U → Prop) {x : U} (HU : unit_type x),
{ empty A } + { A = singleton x }.
Proof.
intros A x HU; destruct (empty_dec A) as [HA | HA]; [left; easy |].
right; apply is_singleton_equiv; split; [easy | intros; apply HU].
Qed.
Lemma unit_subset_is_singleton :
∀ (A : U → Prop) {x : U} (HU : unit_type x), nonempty A → A = singleton x.
Proof.
intros A x HU HA; destruct (unit_subset_dec A HU) as [HA' |];
[contradict HA'; apply nonempty_is_not_empty |]; easy.
Qed.
End Subset_Facts.